From 2d260bd4a4a5c07d3c585f6b64e7b59f619558be Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Tue, 27 Oct 2026 22:07:16 -0700 Subject: [PATCH 1/2] Prove helper469 endpoint receiver recoding impossible on selected word --- .../p104-helper469-receiver-recoding/PROOF.md | 104 +++++++++++ .../README.md | 69 ++++++++ .../RESULT.json | 164 ++++++++++++++++++ .../SOURCES.json | 24 +++ .../TASK.json | 75 ++++++++ .../VERIFY.json | 20 +++ .../verify.py | 127 ++++++++++++++ 7 files changed, 583 insertions(+) create mode 100644 research/p104-helper469-receiver-recoding/PROOF.md create mode 100644 research/p104-helper469-receiver-recoding/README.md create mode 100644 research/p104-helper469-receiver-recoding/RESULT.json create mode 100644 research/p104-helper469-receiver-recoding/SOURCES.json create mode 100644 research/p104-helper469-receiver-recoding/TASK.json create mode 100644 research/p104-helper469-receiver-recoding/VERIFY.json create mode 100644 research/p104-helper469-receiver-recoding/verify.py diff --git a/research/p104-helper469-receiver-recoding/PROOF.md b/research/p104-helper469-receiver-recoding/PROOF.md new file mode 100644 index 0000000000..ee08932356 --- /dev/null +++ b/research/p104-helper469-receiver-recoding/PROOF.md @@ -0,0 +1,104 @@ +# Helper469: receiver recoding still cannot remove the frame593 rung + +This is a one-interval exact rational exclusion, not a new multiplication +construction, native implementation, cost improvement, or universal barrier. +All indices below are zero-based and a slot is the state before an event. + +## Source and changed hypothesis + +The sole computational input is the selected PR6030 word at main +`721c03822c421b7f7fcbb2598993b947c4d88419`, SHA256 +`7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f`. +Its inherited helper468 and helper470 removals are retained. +Jonathan Capalbo's [PR6069](https://github.com/CrocSwap/integer-mult-bounds/pull/6069), +head `b3f5aabddbae2d65f80bb8356e6993e0a65cd245`, excludes donor-only +endpoint resynthesis but explicitly excludes receiver scaling/recoding from +its claim. Its `ENDPOINT-PROOF.md` SHA256 is +`2e7a08c289cfd7761a02d4fcdf0be804a8882a66c532e84058c91ed41134148c`. +That pending proof is contextual attribution, not an imported code dependency +or an assumption of this certificate; the elementary argument is given below. +No foreign source-history ancestry is fabricated or required. + +We allow any finite rational receiver-only ADD/SCALE program in the two +maximal contact-free endpoint windows, with every SCALE nonzero. Other roles' +programs, public inputs, owned lifetimes and charts are fixed. Replace only +469's MOVE 3->593 at14357, its ADD469+=2*703 at14380, and its +MOVE593->713 at14417 by a direct MOVE3->713 and the endpoint programs. +The receiver must regain its entire original scalar row at chart713 before +its next contact at14850. No new MOVE, owned storage or altered donor is allowed. + +## Exact rows and legal windows + +The previous receiver contact is a read at7895. Its next contact after the +second MOVE is the incoming ADD at14850. Thus endpoint slots are +[7896,14357] at chart3 and [14418,14850] at chart713, inclusively. +No original operation reads or changes469 within either window. + +Start all770 public roles as independent coordinate rows e_0,...,e_769; +owned roles enter with zero rows on INIT. ADD/SCALE/COPY have literal rational +semantics; MOVE changes the chart and leaves the decoded scalar row unchanged. +This is the selected word's scalar contract, not a new native-map assertion. + +Exact prefix replay gives receiver entry + + f = e_469 + (1/2)e_537. + +Write Delta = 2 row_703(14380), the one removed interior contribution. +The verifier records every coefficient of Delta in RESULT.json and checks +that the full original receiver row at14418 and14850 equals f+Delta. +In particular Delta has coefficient1/2 at public-input coordinate1. + +Collect every other live row at the beginning of each window, then every +other role's row immediately after a MOVE arrival at its endpoint chart +through the last slot. These569 timestamped generators comprise568 at the +first endpoint and1 at the second. Every collected value is available at its +recorded slot: the receiver can read it then, without retaining a donor after +its departure. Exact replay proves every generator has coordinate1 zero. +The receiver f also has coordinate1 zero. + +Every other donor version available later in a window lies in the span of +these generators: same-chart ADD, SCALE and COPY preserve the accumulated +span; INIT contributes zero; CLEAR and departure cannot enlarge it; each MOVE +arrival is included. No original read of469 occurs within either window, +so modifications to469 do not affect donor rows. This is PR6069's credited +accumulated-span argument, specialized here and independently checked. + +## Normal form and complete decision + +Any finite receiver-only endpoint program has scalar form + + r_out = lambda f + sum_j c_j g_j, lambda != 0, + +because every ADD adds a fixed donor row and every SCALE multiplies all +existing coefficients. A direct MOVE preserves this row; combining both +endpoint programs multiplies their nonzero receiver coefficients. The desired +restoration is r_out=f+Delta, equivalently + + (lambda-1) f + sum_j c_j g_j = Delta. (1) + +This is an exact rational affine system with the invertibility side condition. +For completeness, any formal coefficients of timestamped generators can be +realized in chronological order with arbitrary rational ADDs: scale at the +first slot by lambda, then add each generator at its recorded slot, taking the +direct MOVE after the first window. Donors are unchanged and never read469; +no new storage or free retention is needed. This scalar realization does not +establish the physical scalar alphabet or its cost. Those gates would follow +only if a solution existed. + +Apply the linear functional L(v)=v[1] to(1). The left side is0 for every +rational lambda and c_j, while the right side is1/2. Contradiction. +The feasible lambda set is therefore empty, even if zero multipliers were +granted. This separates the entire affine span, not a finite coefficient +search or a first-order screen. It decides the prescribed invertible model. + +The obstruction explicitly concerns an arbitrary input column; replacing703 +by a label or checking only an ideal fixture would not establish it. The +original receiver row must be restored before14850; postponing repair or +changing another role is outside the model. The precise scientific review +obligations are the scalar interpretation, the complete window boundary, +the accumulated-span induction and its normal-form applicability. + +No candidate survives to be priced. No favorable direct-transition native +rank, paid profile, productive-target histogram, ordinary cost or kappa is +claimed. This exclusion does not decide changed donor routes, new storage, +new receiver contacts, a different word or coupled receiver/donor recoding. diff --git a/research/p104-helper469-receiver-recoding/README.md b/research/p104-helper469-receiver-recoding/README.md new file mode 100644 index 0000000000..985ee532bb --- /dev/null +++ b/research/p104-helper469-receiver-recoding/README.md @@ -0,0 +1,69 @@ +# One coordinate excludes helper469's invertible endpoint recoding + +On the selected PR6030 word, helper469 cannot replace its chart3->593->713 +interval with a direct MOVE3->713 using any finite rational receiver-only +ADD/SCALE programs in its two maximal endpoint windows. Every available donor +and the receiver's entry row have zero coefficient on public input1; the +required restored row has coefficient1/2. The feasible receiver multiplier set +is empty, including all nonzero rational multipliers. See [PROOF.md](PROOF.md) +and the exact [certificate](RESULT.json). + +This answers the receiver-recoding case explicitly excluded by +[PR6069](https://github.com/CrocSwap/integer-mult-bounds/pull/6069), only for +helper469 events14357..14417. It does not repeat the predecessor's764-interval +census. The initial unchanged-receiver holder proposal was withdrawn because +PR6069 already covers it. Canonical investigation: +[discussion6078](https://github.com/CrocSwap/integer-mult-bounds/discussions/6078). + +The verifier independently reconstructs the source rows with standard-library +rational arithmetic. It authenticates the selected word, verifies maximal +contact-free windows and source chart/lifetime semantics, gathers569 legal +timestamped generators, checks the complete receiver row, and compares the +committed deterministic certificate. No pending-source code is imported. +Only the prefix through the restoration boundary is replayed; no full native, +physical caller, selected invoice, Lean or Docker replay is performed. + +## Reproduction + +From the repository root, with Python3.12 or later and no dependencies: + +```sh +python3 -B scripts/research_package.py --package research/p104-helper469-receiver-recoding +python3 -B scripts/check_research_commit.py --package research/p104-helper469-receiver-recoding --check-source-history +``` + +The direct verifier also works in a Git-free export containing the package +and its one declared word input. It writes no files: + +```sh +python3 -B research/p104-helper469-receiver-recoding/verify.py +``` + +SOURCES.json pins the selected word, catalogue card and selected-result record +at main721c03822c421b7f7fcbb2598993b947c4d88419, priority8. The pending +PR6069 head and exact proof hash are contextual provenance in PROOF.md; +there is no hidden dependency on its local Git object. The parent investigation +checked live overlap before claiming this changed hypothesis; this does not +claim novelty against unpublished work or every historical closed PR. + +## Open next questions + +A further construction would have to change a donor program or another stated +boundary. Before opening a new search, identify a route delivering nonzero +input1 coefficient and a favorable complete cost allowance, including native, +productive-target, ordinary and restoration costs. No such route is supplied. +The structured question, relevance, first step and blocker are in TASK.json. +This is a stopping point for receiver-only recoding of this interval. + +## Credit and limitations + +Prepared for JoyboyBrian with substantial OpenAI Codex assistance; Apache-2.0. +Credit Jonathan Capalbo/PR6069 for the accumulated endpoint-span argument and +its explicit receiver-recoding boundary; Nick Petalas/PR6033 for the carrier +cost context; DreamingOfClouds/PR6030 for the selected word and inherited rung +removals; Ali Romman/PR5827 and all retained P104 authors for the scalar/native +construction. Sparse rational replay here is independently implemented. + +This is an author-checked finite scalar exclusion and a mathematical argument +for its stated endpoint program class. It is not independent human scientific +acceptance, supplier admission, a new kappa, or the full multiplication theorem. diff --git a/research/p104-helper469-receiver-recoding/RESULT.json b/research/p104-helper469-receiver-recoding/RESULT.json new file mode 100644 index 0000000000..8f2eb1f879 --- /dev/null +++ b/research/p104-helper469-receiver-recoding/RESULT.json @@ -0,0 +1,164 @@ +{ + "status": "EXCLUDED_ALL_RATIONAL_RECEIVER_MULTIPLIERS", + "receiver": 469, + "moves": [ + 14357, + 14417 + ], + "interior_add": 14380, + "windows": [ + { + "side": "before", + "slots_inclusive": [ + 7896, + 14357 + ], + "chart": 3 + }, + { + "side": "after", + "slots_inclusive": [ + 14418, + 14850 + ], + "chart": 713 + } + ], + "receiver_entry": { + "469": "1", + "537": "1/2" + }, + "required_interior_increment": { + "1": "1/2", + "4": "1/2", + "5": "1/2", + "7": "-1/2", + "10": "-1/2", + "11": "-1/2", + "12": "-1/2", + "13": "-1/2", + "18": "-1/2", + "19": "-1/2", + "24": "-1/2", + "26": "1/2", + "29": "1/2", + "30": "1/2", + "32": "-1/2", + "36": "-1/2", + "37": "-1/2", + "38": "-1/2", + "43": "-1/2", + "45": "-1/2", + "49": "-1/2", + "50": "-1/2", + "51": "1/2", + "56": "-1/2", + "57": "-1/2", + "58": "1/2", + "62": "-1/2", + "63": "-1/2", + "64": "1/2", + "65": "1/2", + "67": "1/2", + "72": "-1/2", + "73": "1/2", + "74": "1/2", + "79": "-1/2", + "81": "-1/2", + "82": "1/2", + "86": "1/2", + "88": "1/2", + "89": "1/2", + "92": "-1/2", + "94": "-1/2", + "95": "1/2", + "98": "-1/2", + "101": "-1/2", + "102": "-1/2", + "103": "-1/2", + "104": "1/2", + "108": "-1/2", + "109": "-1/2", + "110": "1/2", + "111": "1/2", + "173": "1", + "224": "1/2", + "226": "1/2", + "227": "-1/2", + "233": "-1/2", + "235": "-1/2", + "237": "-1/2", + "239": "-1/2", + "241": "-1/2", + "243": "-1/2", + "249": "-1/2", + "251": "-1/2", + "253": "-1/2", + "255": "-1/2", + "256": "-1", + "257": "-1/2", + "262": "1/2", + "265": "-1", + "266": "-1/2", + "269": "-1/2", + "276": "-1/2", + "283": "-1/2", + "286": "-1/2", + "287": "1", + "292": "-1/2", + "299": "-1/2", + "302": "-1/2", + "303": "1", + "308": "-1/2", + "315": "-1/2", + "318": "-1/2", + "319": "1", + "324": "-1/2", + "331": "-1/2", + "334": "-1/2", + "335": "1", + "336": "1/2", + "347": "1/2", + "351": "1/2", + "352": "1/2", + "363": "1/2", + "367": "1/2", + "368": "1/2", + "379": "1/2", + "383": "1/2", + "384": "1/2", + "395": "1/2", + "399": "1/2", + "416": "-1/2", + "418": "1/2", + "419": "-1/2", + "422": "1/2", + "425": "-1/2", + "426": "-1/2", + "427": "1/2", + "431": "1/2", + "434": "1/2", + "435": "-1/2", + "438": "1/2", + "441": "-1/2", + "442": "-1/2", + "443": "1/2", + "447": "1/2", + "703": "2" + }, + "donor_generators": { + "before": 568, + "after": 1, + "timestamped_rows_sha256": "afbfd8ab585100cc059c63d76a32232e866c2bf9be2a23a1e6f3300eaa5f6c4f" + }, + "separator": { + "public_input": 1, + "receiver_value": "0", + "every_donor_value": "0", + "required_increment_value": "1/2", + "feasible_lambda_set": "empty" + }, + "full_receiver_target_checked": true, + "word_sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f", + "scope": "Only receiver469 interval14357..14417, unchanged donor programs and two maximal endpoint windows; no supplier or kappa claim." +} diff --git a/research/p104-helper469-receiver-recoding/SOURCES.json b/research/p104-helper469-receiver-recoding/SOURCES.json new file mode 100644 index 0000000000..c46dd7611f --- /dev/null +++ b/research/p104-helper469-receiver-recoding/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "usage": "input", + "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760", + "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" + } + ] +} diff --git a/research/p104-helper469-receiver-recoding/TASK.json b/research/p104-helper469-receiver-recoding/TASK.json new file mode 100644 index 0000000000..ca9d65be66 --- /dev/null +++ b/research/p104-helper469-receiver-recoding/TASK.json @@ -0,0 +1,75 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Exact all-rational receiver-only endpoint ADD/SCALE recoding for helper469 interval14357..14417 on selected PR6030.", + "scope_change_reason": "PR6069 excludes donor-only relocation but explicitly leaves receiver scaling/recoding open. Add the entry receiver row to its span model, only for this interval.", + "bottleneck_link": "Reject this itinerary removal before spending native/invoice work; receiver recoding is a changed hypothesis, not another donor-holder search.", + "budget_minutes": 60, + "stop_rule": "Stop after the one-interval exact affine decision; no interval census or new donor routes.", + "outcome": "scoped-exclusion", + "evidence": "PROOF.md, RESULT.json and verify.py", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance", + "open_questions": [ + { + "question": "Can a changed other-role program deliver a nonzero input1 coefficient to an endpoint without repaying the removed transport?", + "why_it_matters": "Every unchanged donor and the receiver lack this coordinate, so receiver-only recoding cannot remove the rung.", + "first_step": "Before construction, name one changed donor route and bound its complete paid, productive-target, ordinary and restoration costs.", + "blocked_by": "No favorable complete-cost changed-donor route is supplied; do not expand this exclusion into an automatic search." + } + ] +} diff --git a/research/p104-helper469-receiver-recoding/VERIFY.json b/research/p104-helper469-receiver-recoding/VERIFY.json new file mode 100644 index 0000000000..4e0b286605 --- /dev/null +++ b/research/p104-helper469-receiver-recoding/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper470-twin-rung-removal/WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact source hash, arbitrary-input receiver row, legal donor versions and separating coordinate" + } + ] +} diff --git a/research/p104-helper469-receiver-recoding/verify.py b/research/p104-helper469-receiver-recoding/verify.py new file mode 100644 index 0000000000..0de3113ee9 --- /dev/null +++ b/research/p104-helper469-receiver-recoding/verify.py @@ -0,0 +1,127 @@ +"""One-interval exact scalar exclusion. JoyboyBrian, OpenAI Codex assistance. +Apache-2.0; PR6069's accumulated-span argument is credited in PROOF.md. +""" +from fractions import Fraction as Q +from hashlib import sha256 +from pathlib import Path +import gzip +import json + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +WORD = 'research/p104-helper470-twin-rung-removal/WORD.json.gz' +WORD_HASH = '7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f' +WINDOWS = [('before', 7896, 14357, 3), ('after', 14418, 14850, 713)] + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def encode(row): + return {str(k): str(v) for k, v in sorted(row.items()) if v} + + +def digest(value): + return sha256(json.dumps(value, sort_keys=True, separators=(',', ':')).encode()).hexdigest() + + +def add(row, donor, c): + for k, v in tuple(donor.items()): + row[k] = row.get(k, 0) + c * v + if not row[k]: + del row[k] + + +def load_word(): + payload = (ROOT / WORD).read_bytes() + require(sha256(payload).hexdigest() == WORD_HASH, 'Selected word source hash') + return json.loads(gzip.decompress(payload)) + + +def extract(word): + """Reconstruct arbitrary-input rows and actual start/arrival donor versions.""" + program, public = word['program'], word['public'] + require(public == 770 and word['owned_fields'] == 29, 'Source dimensions') + require(program[14357] == ['MOVE', 469, 3, 593, False], 'First MOVE') + require(program[14380] == ['ADD', 469, 703, '2', 593], 'Interior ADD') + require(program[14417] == ['MOVE', 469, 593, 713, False], 'Second MOVE') + contacts = [i for i, e in enumerate(program) if e[1] == 469 or + (e[0] in ('ADD', 'COPY') and e[2] == 469)] + require([i for i in contacts if 7895 <= i <= 14850] == + [7895, 14357, 14380, 14417, 14850], 'Maximal contact-free windows') + rows = [{r: Q(1)} for r in range(public)] + [{} for _ in range(word['owned_fields'])] + charts = word['initial'][:] + [None] * word['owned_fields'] + generators, f, delta, target = [], None, None, None + for slot, event in enumerate(program[:14850]): + for side, lo, hi, frame in WINDOWS: + if slot == lo: + require(charts[469] == frame, 'Endpoint receiver chart') + generators.extend((side, slot, r, dict(rows[r])) for r, chart in + enumerate(charts) if chart == frame and r != 469) + if (lo <= slot < hi and event[0] == 'MOVE' and event[3] == frame + and event[1] != 469): + generators.append((side, slot + 1, event[1], dict(rows[event[1]]))) + if slot == 14357: + f = dict(rows[469]) + if slot == 14380: + delta = {k: 2 * v for k, v in rows[703].items()} + op, r = event[:2] + if op == 'MOVE': + require(charts[r] == event[2] and event[4] == (r >= public), 'MOVE chart/ownership') + charts[r] = event[3] + elif op == 'INIT': + require(r >= public and charts[r] is None, 'INIT lifetime') + charts[r], rows[r] = event[2], {} + elif op == 'CLEAR': + require(r >= public and charts[r] == event[2], 'CLEAR lifetime') + charts[r], rows[r] = None, {} + else: + c, chart = Q(event[-2]), event[-1] + require(c and charts[r] == chart and chart is not None, 'Scalar destination') + if op == 'SCALE': + rows[r] = {k: c * v for k, v in rows[r].items()} + else: + require(op in ('ADD', 'COPY') and event[2] != r and + charts[event[2]] == chart, 'Scalar donor chart') + require(op != 'COPY' or (r >= public and not rows[r]), 'COPY zero lifetime') + add(rows[r], rows[event[2]], c) + if slot == 14417: + target = dict(rows[469]) + expected = dict(f) + add(expected, delta, Q(1)) + require(expected == target == rows[469] and charts[469] == 713, 'Full receiver restoration target') + require(f == {469: Q(1), 537: Q(1, 2)}, 'Receiver entry arbitrary-input row') + return f, delta, generators + + +def certificate(word): + f, delta, generators = extract(word) + require(len(generators) == 569, 'Generator inventory') + require(f.get(1, 0) == 0 and all(row.get(1, 0) == 0 for *_, row in generators), + 'Separator annihilates receiver and every donor generator') + require(delta.get(1) == Q(1, 2), 'Separator detects required restoration') + return { + 'status': 'EXCLUDED_ALL_RATIONAL_RECEIVER_MULTIPLIERS', + 'receiver': 469, 'moves': [14357, 14417], 'interior_add': 14380, + 'windows': [{'side': s, 'slots_inclusive': [a, b], 'chart': c} for s, a, b, c in WINDOWS], + 'receiver_entry': encode(f), 'required_interior_increment': encode(delta), + 'donor_generators': {'before': sum(s == 'before' for s, *_ in generators), + 'after': sum(s == 'after' for s, *_ in generators), + 'timestamped_rows_sha256': digest([[s, t, r, encode(v)] for s, t, r, v in generators])}, + 'separator': {'public_input': 1, 'receiver_value': '0', 'every_donor_value': '0', + 'required_increment_value': '1/2', 'feasible_lambda_set': 'empty'}, + 'full_receiver_target_checked': True, + 'word_sha256': WORD_HASH, + 'scope': 'Only receiver469 interval14357..14417, unchanged donor programs and two maximal endpoint windows; no supplier or kappa claim.'} + + +def main(): + result = certificate(load_word()) + require(result == json.loads((PACKAGE / 'RESULT.json').read_text()), 'Committed exact certificate') + print(json.dumps(result, sort_keys=True)) + + +if __name__ == '__main__': + main() From 06d9cd06aa769514304b1ec461117a793addb9f9 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Tue, 27 Oct 2026 22:08:35 -0700 Subject: [PATCH 2/2] Independently replay legal donor slots and reject invalid endpoint recodings --- .../README.md | 7 +- .../TASK.json | 4 +- .../VERIFY.json | 31 ++++- .../controls.py | 112 ++++++++++++++++++ 4 files changed, 149 insertions(+), 5 deletions(-) create mode 100644 research/p104-helper469-receiver-recoding/controls.py diff --git a/research/p104-helper469-receiver-recoding/README.md b/research/p104-helper469-receiver-recoding/README.md index 985ee532bb..38169d3b8c 100644 --- a/research/p104-helper469-receiver-recoding/README.md +++ b/research/p104-helper469-receiver-recoding/README.md @@ -20,7 +20,10 @@ rational arithmetic. It authenticates the selected word, verifies maximal contact-free windows and source chart/lifetime semantics, gathers569 legal timestamped generators, checks the complete receiver row, and compares the committed deterministic certificate. No pending-source code is imported. -Only the prefix through the restoration boundary is replayed; no full native, +Independent controls replay input1 literally at every legal donor slot and exercise +a synthetic recoding positive plus zero-multiplier, wrong-version, wrong-chart, +changed-input-column and omitted-restoration negatives. Both scripts are +registered in normal and optimized Python. Only the prefix through the restoration boundary is replayed; no full native, physical caller, selected invoice, Lean or Docker replay is performed. ## Reproduction @@ -28,7 +31,7 @@ physical caller, selected invoice, Lean or Docker replay is performed. From the repository root, with Python3.12 or later and no dependencies: ```sh -python3 -B scripts/research_package.py --package research/p104-helper469-receiver-recoding +python3.12 -B scripts/research_package.py --package research/p104-helper469-receiver-recoding python3 -B scripts/check_research_commit.py --package research/p104-helper469-receiver-recoding --check-source-history ``` diff --git a/research/p104-helper469-receiver-recoding/TASK.json b/research/p104-helper469-receiver-recoding/TASK.json index ca9d65be66..1fa424acb6 100644 --- a/research/p104-helper469-receiver-recoding/TASK.json +++ b/research/p104-helper469-receiver-recoding/TASK.json @@ -60,8 +60,8 @@ "bottleneck_link": "Reject this itinerary removal before spending native/invoice work; receiver recoding is a changed hypothesis, not another donor-holder search.", "budget_minutes": 60, "stop_rule": "Stop after the one-interval exact affine decision; no interval census or new donor routes.", - "outcome": "scoped-exclusion", - "evidence": "PROOF.md, RESULT.json and verify.py", + "outcome": "negative-result", + "evidence": "PROOF.md, RESULT.json, verify.py and independent controls.py", "author": "JoyboyBrian", "ai_assistance": "Substantial OpenAI Codex assistance", "open_questions": [ diff --git a/research/p104-helper469-receiver-recoding/VERIFY.json b/research/p104-helper469-receiver-recoding/VERIFY.json index 4e0b286605..86bb84d6f3 100644 --- a/research/p104-helper469-receiver-recoding/VERIFY.json +++ b/research/p104-helper469-receiver-recoding/VERIFY.json @@ -14,7 +14,36 @@ "{package}/verify.py" ], "timeout_seconds": 30, - "checks": "Exact source hash, arbitrary-input receiver row, legal donor versions and separating coordinate" + "checks": "Exact source and all-rational separating certificate" + }, + { + "argv": [ + "{python}", + "-B", + "{package}/controls.py" + ], + "timeout_seconds": 30, + "checks": "Independent literal input1 replay; recoding positive; zero, chart, version, arbitrary-column and restoration negatives" + }, + { + "argv": [ + "{python}", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact source and all-rational separating certificate under optimized Python" + }, + { + "argv": [ + "{python}", + "-B", + "-O", + "{package}/controls.py" + ], + "timeout_seconds": 30, + "checks": "Independent literal input1 replay; recoding positive; zero, chart, version, arbitrary-column and restoration negatives under optimized Python" } ] } diff --git a/research/p104-helper469-receiver-recoding/controls.py b/research/p104-helper469-receiver-recoding/controls.py new file mode 100644 index 0000000000..0dc2a6ab39 --- /dev/null +++ b/research/p104-helper469-receiver-recoding/controls.py @@ -0,0 +1,112 @@ +"""Independent one-column replay and literal endpoint controls; standard library. +Prepared for JoyboyBrian with substantial OpenAI Codex assistance; Apache-2.0. +""" +from fractions import Fraction as F +import json +import verify as primary + + +def check(condition, message): + if not condition: + raise ValueError(message) + + +def independent_column(word): + # A scalar input evaluation, with no sparse-row replay or span code reused. + values = [F(int(r == 1)) for r in range(799)] + charts = word['initial'][:] + [None] * 29 + checked = 0 + for slot in range(14851): + frame = 3 if 7896 <= slot <= 14357 else 713 if 14418 <= slot <= 14850 else None + if frame is not None: + for role, chart in enumerate(charts): + if chart == frame and role != 469: + check(values[role] == 0, 'Independent legal donor coordinate') + checked += 1 + if slot == 14357: + check(values[469] == 0, 'Independent entry coordinate') + if slot == 14418 or slot == 14850: + check(values[469] == F(1, 2), 'Independent restored coordinate') + if slot == 14850: + break + event = word['program'][slot] + op, r = event[:2] + if op == 'MOVE': + check(charts[r] == event[2], 'Independent MOVE source') + charts[r] = event[3] + elif op == 'INIT': + check(charts[r] is None, 'Independent INIT') + values[r], charts[r] = F(0), event[2] + elif op == 'CLEAR': + check(charts[r] == event[2], 'Independent CLEAR') + values[r], charts[r] = F(0), None + elif op == 'SCALE': + check(charts[r] == event[3], 'Independent SCALE chart') + values[r] *= F(event[2]) + elif op in ('ADD', 'COPY'): + check(charts[r] == charts[event[2]] == event[4], 'Independent ADD chart') + if op == 'COPY': + check(values[r] == 0, 'Independent COPY zero') + values[r] += F(event[3]) * values[event[2]] + else: + raise ValueError('Unknown source operation') + return checked + + +def literal_endpoint(operations, expected, donor=(0, 1), donor_chart=0): + """Dense two-column receiver interpreter; ADD carries its donor version.""" + receiver, source, chart = [F(1), F(0)], list(map(F, donor)), 0 + for event in operations: + if event[0] == 'SCALE': + c = F(event[1]) + check(c != 0, 'Nonzero receiver multiplier') + receiver = [c * x for x in receiver] + elif event[0] == 'ADD': + check(chart == donor_chart, 'Live donor chart') + check(source == list(map(F, event[2])), 'Exact donor version') + receiver = [x + F(event[1]) * y for x, y in zip(receiver, source)] + elif event[0] == 'MOVE': + check(chart == event[1], 'Receiver MOVE source') + chart = event[2] + else: + raise ValueError('Unknown endpoint operation') + check(chart == 1, 'Restored endpoint chart') + check(receiver == list(map(F, expected)), 'Complete arbitrary-input restoration') + return receiver + + +def rejected(callback, expected_error): + try: + callback() + except ValueError as error: + check(str(error) == expected_error, 'Expected rejection reason: ' + str(error)) + else: + raise ValueError('Negative control was accepted') + + +def main(): + word = primary.load_word() + visits = independent_column(word) + good = [('SCALE', 2), ('ADD', 3, [0, 1]), ('MOVE', 0, 1)] + check(literal_endpoint(good, [2, 3]) == [2, 3], 'Receiver recoding positive') + # Delta=(1,3) is outside span{(0,1)}, but lambda=2 solves the affine problem. + delta, donor = [F(1), F(3)], [F(0), F(1)] + check(delta[0] != 0 and donor[0] == 0, 'Coordinate separates donor-only target') + rejected(lambda: literal_endpoint([('SCALE', 0), ('MOVE', 0, 1)], [0, 0]), + 'Nonzero receiver multiplier') + rejected(lambda: literal_endpoint(good, [2, 3], donor=(0, 2)), 'Exact donor version') + rejected(lambda: literal_endpoint(good, [2, 3], donor_chart=1), 'Live donor chart') + rejected(lambda: literal_endpoint(good, [2, 4]), 'Complete arbitrary-input restoration') + rejected(lambda: literal_endpoint([('SCALE', 2), ('MOVE', 0, 1)], [2, 3]), + 'Complete arbitrary-input restoration') + # Omitting the entry receiver from a generic span test loses valid recodings. + check([2 * F(1), 3 * F(1)] == literal_endpoint(good, [2, 3]), 'Literal affine substitution') + print(json.dumps({'status': 'PASS_INDEPENDENT_CONTROLS', 'legal_donor_slot_visits': visits, + 'actual_input1_literal_replay': True, 'invertible_recoding_positive': True, + 'zero_multiplier_rejected': True, 'wrong_donor_version_rejected': True, + 'wrong_chart_rejected': True, 'changed_input_column_rejected': True, + 'omitted_restoration_rejected': True}, sort_keys=True)) + + +if __name__ == '__main__': + main()