From ebb536fff17e28a6fd1edcac308f7d90b518ebe4 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Tue, 27 Oct 2026 22:10:42 -0700 Subject: [PATCH 1/2] Prove the two-ADD non-carrier seam fails outside restoration --- .../p104-noncarrier-two-add-seam/PROOF.md | 132 ++++++++ .../p104-noncarrier-two-add-seam/README.md | 80 +++++ .../p104-noncarrier-two-add-seam/RESULT.json | 40 +++ .../p104-noncarrier-two-add-seam/SOURCES.json | 24 ++ .../p104-noncarrier-two-add-seam/TASK.json | 118 +++++++ .../p104-noncarrier-two-add-seam/VERIFY.json | 32 ++ .../p104-noncarrier-two-add-seam/verify.py | 305 ++++++++++++++++++ 7 files changed, 731 insertions(+) create mode 100644 research/p104-noncarrier-two-add-seam/PROOF.md create mode 100644 research/p104-noncarrier-two-add-seam/README.md create mode 100644 research/p104-noncarrier-two-add-seam/RESULT.json create mode 100644 research/p104-noncarrier-two-add-seam/SOURCES.json create mode 100644 research/p104-noncarrier-two-add-seam/TASK.json create mode 100644 research/p104-noncarrier-two-add-seam/VERIFY.json create mode 100644 research/p104-noncarrier-two-add-seam/verify.py diff --git a/research/p104-noncarrier-two-add-seam/PROOF.md b/research/p104-noncarrier-two-add-seam/PROOF.md new file mode 100644 index 0000000000..6a6dff4ffd --- /dev/null +++ b/research/p104-noncarrier-two-add-seam/PROOF.md @@ -0,0 +1,132 @@ +# Two ADDs across the 572 seam cannot restore the outside outputs + +This is an exact finite exclusion in the rational scalar model of the selected +PR6030 word. It is not a new supplier or a universal P104 obstruction. +All event indices are zero based, and a window is immediately **after** its event. + +## Domain + +Keep the complete prefix, original event schedule, charts, fields and owned +lifetimes. Immediately after event 13637 (`COPY 778 <- 572` at chart 595), +replace field 572 by a new independent input `z`. The displaced original row is +`ell X`, where `X` consists of all 770 arbitrary original public inputs. + +Insert precisely these two ADD opportunities (a zero coefficient is allowed, +so the exclusion also covers using fewer than two): + +1. After any event `i` in 13637..13651, add `a * field_u` to `field_v`, with + distinct `u,v` in chart 595. Its six roles are + `[127,572,581,582,731,778]` throughout these windows. +2. After event `j` in `{13652,13654,13655}`, add `b * field_s` to `field_r`, + with distinct `s,r` then at chart 603. The banks are respectively + `[572,740]`, `[572,740]`, `[572,709,740]`. + +Both coefficients may be arbitrary rationals. Sources need not be carriers: +these operations may temporarily change original `X` rows. Event 13652 is the +unchanged MOVE of 572 from 595 to 603; event 13654 adds `-572` into 740; +event 13655 brings 709 to 603. CLEAR 778 at 13656 also stays unchanged. + +Let `V=127`, the original final chart of 572, and let `O` be the 186 public +roles whose final chart differs from V. The required necessary condition is +that **every O output equal its original unsplit output for every X and z**. + +**Result.** None of the `15 * 30 * (2 + 2 + 6) = 4,500` location pairs can +meet that condition. This holds even if erasing z completely were permitted. +Consequently none can supply a legal split with a nonzero V-final z target. + +## Exact endpoint polynomial + +Use row vectors for input functionals and column vectors for final public +outputs. Let `R_i` be the original prefix at window i and `S_i` the original +public suffix. Let `beta_i` be the propagation, through original events, of +the unit vector placed at 572 at the overwrite. Set + +``` +e = z - ell X +D = S_cut e_572 +A = S_i e_v +B = S_j e_r +b1 = (beta_i)_u +b2 = (beta_j)_s +g = (T_{j<-i})_{s,v} +f = (R_i X)_u + b1 e +h = (R_j X)_s + b2 e +``` + +Here `e_572,e_v,e_r` are state-coordinate unit vectors; `e` without a +subscript is the scalar functional `z-ell X`. `T_{j<-i}` is the unchanged +intervening linear program. The first source's value is f. Its update changes +the second source's value from h to `h + a*g*f`. Linearity of the retained +suffix gives the complete final public difference: + +``` +D e + a A f + b B h + a b g B f. (1) +``` + +This includes original-input defects as well as the z coefficient. It does +not assume that either correction has zero original value. Neither does it +linearize around zero coefficients or discard the interaction term. + +Introduce independent rational unknowns `(a,b,c)` in place of `(a,b,a*b)`. +For each outside output and each input column (including z), setting (1) to +zero is a linear equation in these three unknowns. Every actual two-ADD +solution would solve this **more permissive** system with `c=a*b`. +The verifier proves all 4,500 relaxed systems inconsistent. No bounded +coefficient search, root-finding or unproved quadratic-solving step is used. + +## Certificates and coverage + +The checker authenticates the selected compressed word against SOURCES.json, +replays its exact rational rows and live charts, and constructs reverse public +suffix columns. The complete forward endpoint and reverse transpose agree; +all original owned rows restore and their lifetimes end. This authenticates +the scalar data used here, not the selected native implementation. + +For each of all 4,500 location pairs, sparse elimination records a rational +linear combination of original protected-output equations whose left side is +zero and right side is one. A separate checker recomputes the selected original +equations and verifies those dot products directly, without row reduction. +There are 4,262 one-equation and 238 two-equation contradictions. The canonical +certificate transcript SHA-256 is retained in RESULT.json; every replay +recomputes and checks every certificate, not merely its digest. + +For example, the first pair is +`(i,u,v,j,s,r)=(13637,127,572,13652,572,740)`. A contradiction uses output 120's +original input-column equations 0 and 34 with multipliers `-2` and `1`. +The exact right-side sum is 1 and all three unknown coefficients sum to zero. +The literal coordinates and multipliers are in RESULT.json. + +Independent literal whole-word execution checks four parameterized production +cases against (1) on **all original input columns and the new z column**. +These include a nonzero interaction term, a correction using 778, a first +update before the ADD into 582, and a changed original row. The literal engine +has its own event loop and row arithmetic, separate from the prefix/suffix +engine. This is implementation cross-checking by an AI-assisted contributor, +not independent human or formal-kernel acceptance. + +A particularly relevant false positive is `127 -> 572` with coefficient 1 +after 13651, followed by `740 -> 572` with coefficient 1 after 13654. Its +outside z-leak is zero and z survives publicly, but its outside original-X +rows are wrong. The full equations reject it. This demonstrates why a z-only +check would not settle the claimed question. + +## Scope boundary + +PR6067 and PR6069 cover corrections that preserve the original scalar rows at +each completed atomic carrier update. Their results do not imply this one: +we allow non-carrier sources and change original rows between two different +charts. Conversely, this package covers only the stated two-ADD locations. +It says nothing about three or more ADDs, different later windows, changed +prefixes, non-unit injection, new routes/storage or changed scheduled events. +It does not audit either predecessor's complete proof or census. + +The necessary scalar condition already fails. Therefore no candidate reaches +pairing, productive targets, owned-restoration after a successful edit, native +realization or full paid/ordinary/compiler/outer pricing. Those checks are not +silently counted as passed. The selected word, its five framework assumptions +and kappa remain unchanged. + +Prepared for **JoyboyBrian**, with substantial OpenAI Codex assistance. +Apache-2.0. Credit apoursh (PR6067), Jonathan Capalbo (PR6069), JosieElliston +(PR6045), Nick Petalas (PR6040), Matarener (PR5994), flyingviper (PR5718), +Ali Romman and DreamingOfClouds (selected P104 word), and their retained lineage. diff --git a/research/p104-noncarrier-two-add-seam/README.md b/research/p104-noncarrier-two-add-seam/README.md new file mode 100644 index 0000000000..907c4e10b7 --- /dev/null +++ b/research/p104-noncarrier-two-add-seam/README.md @@ -0,0 +1,80 @@ +# P104: two non-carrier ADDs across the helper572 seam fail + +**Scoped exact exclusion; no new kappa.** On the selected PR6030 word, +none of 4,500 declared two-ADD location pairs restores every outside-V output +following the unit overwrite of helper572 after event13637. The corrections +may temporarily change original input rows, so this is outside the carrier-only +models of [PR6067](https://github.com/CrocSwap/integer-mult-bounds/pull/6067) +and [PR6069](https://github.com/CrocSwap/integer-mult-bounds/pull/6069). + +The first ADD is at chart595 after any event13637..13651. The second is at +chart603 after13652,13654 or13655. All original events, fields, charts and +lifetimes stay fixed. Coefficients are arbitrary rationals, including zero. +Every original input and the new independent z are symbolic. [PROOF.md](PROOF.md) +specifies the complete domain and endpoint polynomial. + +All cases fail even after relaxing the product `a*b` to an independent third +unknown. Each has an exact independently checked linear contradiction: +4,262 use one equation and238 use two. Four separate literal whole-word checks +validate the polynomial on all input columns, including a nonzero interaction +term. A retained false positive clears the z-leak but corrupts original inputs. +[RESULT.json](RESULT.json) retains the deterministic certificate digest and counts. + +The scientific base is canonical main `721c03822c421b7f7fcbb2598993b947c4d88419`, +priority8, selected conditional kappa0.003125804. The canonical investigation is +[Discussion6074](https://github.com/CrocSwap/integer-mult-bounds/discussions/6074). + +## Reproduce + +Python3.12 and its standard library, from the repository root: + +```sh +python3.12 -I -B research/p104-noncarrier-two-add-seam/verify.py +python3.12 -I -O -B research/p104-noncarrier-two-add-seam/verify.py +python3.12 -B scripts/research_package.py --package research/p104-noncarrier-two-add-seam +``` + +Direct normal replay took about8.6seconds on macOS arm64. Both registered +modes have30-second limits. Every guard remains active under `-O`. +`--write` regenerates only this package's RESULT.json; default replay is read-only. +There are no executable pending-PR dependencies: the sole external live input +is the selected WORD.json.gz, source-pinned in SOURCES.json and declared in VERIFY.json. + +## Coverage and overlap + +This follows the original-row-changing correction question in PR6067 at +`4d629cf0d20a06d65b3ba0cf3a34e105128725e3` and PR6069 at +`b3f5aabddbae2d65f80bb8356e6993e0a65cd245`. Their carrier-only exclusions are +credited rather than replayed. The package derives its boundary data directly +from the selected word; neither pending proof is an executable dependency. + +Preclaim overlap read341open PRs,5,722discussion records and8,348local notes. +That metadata coverage is not a novelty guarantee or a search of historical +diffs/unpublished work. The companion receiver-recoding task concerns helper469 +and is separate. No fixed-invoice repacking or selected-word application audit +is repeated here. + +The full necessary endpoint condition fails, so there is no edited supplier to +price. No native/compiler/caller/precision/outer replay, selected cold replay, +Lean, Docker or full multiplication proof is supplied. No universal bound or +claim about more edits follows. The five selected assumptions remain. + +## Open next questions + +A longer source-bound correction or a different chronological window remains +outside this exclusion. Before a new search, supply a concrete candidate word +that changes the failed original-input equations, then check its full symbolic +endpoint, pairing, lifetime and complete bill. No broader search is proposed +merely because this bounded model failed. Structured first steps and blockers +are in TASK.json. + +## Credit + +Prepared for **JoyboyBrian**, with substantial OpenAI Codex assistance in +triage, derivation, implementation and verification. This is AI-assisted +research, not independent human or proof-kernel approval. Apache-2.0. + +Credit apoursh (PR6067), Jonathan Capalbo (PR6069), JosieElliston (PR6045), +Nick Petalas (PR6040), Matarener (PR5994), flyingviper (PR5718), Ali Romman, +DreamingOfClouds (PR6030/5907) and the retained P104/native/compiler lineage. +Frozen predecessor packages and the selected construction are unchanged. diff --git a/research/p104-noncarrier-two-add-seam/RESULT.json b/research/p104-noncarrier-two-add-seam/RESULT.json new file mode 100644 index 0000000000..f2e870a9d1 --- /dev/null +++ b/research/p104-noncarrier-two-add-seam/RESULT.json @@ -0,0 +1,40 @@ +{ + "V_chart": 127, + "cases": 4500, + "claim": "Every declared two-ADD seam fails exact outside-V restoration, even with ab independent.", + "controls": { + "bilinear_case": true, + "consistent_system": true, + "forged_dual_rejected": true, + "literal_full_column_cases": 4, + "z_only_false_positive": true + }, + "dual_sha256": "324b646386e6776953c9d3ad52e03ad9d76738c0ca2fc061e20c106e21f73846", + "dual_size_counts": { + "1": 4262, + "2": 238 + }, + "first_dual": { + "case": [ + 13637, + 127, + 572, + 13652, + 572, + 740 + ], + "dual": [ + [ + 120, + 0, + "-2" + ], + [ + 120, + 34, + "1" + ] + ] + }, + "outside_public_roles": 186 +} diff --git a/research/p104-noncarrier-two-add-seam/SOURCES.json b/research/p104-noncarrier-two-add-seam/SOURCES.json new file mode 100644 index 0000000000..c46dd7611f --- /dev/null +++ b/research/p104-noncarrier-two-add-seam/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-noncarrier-two-add-seam/TASK.json b/research/p104-noncarrier-two-add-seam/TASK.json new file mode 100644 index 0000000000..ab1ca22974 --- /dev/null +++ b/research/p104-noncarrier-two-add-seam/TASK.json @@ -0,0 +1,118 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "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", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.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": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "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": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "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": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "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": "changed", + "actual_scope": "Exact all-rational exclusion of two original-row-changing ADDs across helper572 chart595-to603 after unit overwrite at13637 on selectedPR6030.", + "scope_change_reason": "The releasedPR6067/6069 non-carrier question replaces the stalePR5599 construction scope; one explicit seam and two correction opportunities are fixed.", + "bottleneck_link": "This is a scoped necessary-condition side result for a proposed productive helper split, not a completed supplier or priced gain.", + "budget_minutes": 60, + "stop_rule": "Stop after an exact witness or exclusion of the4500 declared location pairs; do not widen to longer words or rerun the4033-class census.", + "outcome": "negative-result", + "evidence": "PROOF.md, RESULT.json and source-bound verify.py with exact checked duals and separate literal whole-word controls.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance; no independent human or proof-kernel review claimed.", + "open_questions": [ + { + "question": "Can a concrete longer correction or different second window restore the original inputs while retaining the new helper?", + "why_it_matters": "The claimed two-event seam fails on original-input equations; a useful successor must change that obstruction.", + "first_step": "Provide one explicit changed chronological word, derive its entire X,z endpoint, then test pairing and charge the complete bill.", + "blocked_by": "No candidate is supplied; this finite exclusion alone does not justify a wider search. Native, lifetime and full-cost obligations remain." + } + ], + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/6074" +} diff --git a/research/p104-noncarrier-two-add-seam/VERIFY.json b/research/p104-noncarrier-two-add-seam/VERIFY.json new file mode 100644 index 0000000000..2a33428d33 --- /dev/null +++ b/research/p104-noncarrier-two-add-seam/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper470-twin-rung-removal/WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Authenticate source; all4500 exact relaxed systems and duals; forward/reverse equality; four independent literal all-column executions; z-only false positive and solver controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Authenticate source; all4500 exact relaxed systems and duals; forward/reverse equality; four independent literal all-column executions; z-only false positive and solver controls." + } + ] +} diff --git a/research/p104-noncarrier-two-add-seam/verify.py b/research/p104-noncarrier-two-add-seam/verify.py new file mode 100644 index 0000000000..3f6b708d5c --- /dev/null +++ b/research/p104-noncarrier-two-add-seam/verify.py @@ -0,0 +1,305 @@ +"""Exact two-ADD seam exclusion. JoyboyBrian with OpenAI Codex, Apache-2.0.""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +from pathlib import Path +import gzip +import json +import sys + +HERE = Path(__file__).resolve().parent +WORD = 'research/p104-helper470-twin-rung-removal/WORD.json.gz' +CUT = 13637 +FIRST = range(CUT, 13652) +SECOND = (13652, 13654, 13655) +PIVOT = 572 + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def add(a, b, scale=Q(1)): + result = a.copy() + for k, v in b.items(): + value = result.get(k, 0) + scale * v + if value: + result[k] = value + else: + result.pop(k, None) + return result + + +def forward(rows, event): + op, r = event[:2] + if op == 'ADD': + rows[r] = add(rows[r], rows[event[2]], Q(event[3])) + elif op == 'COPY': + rows[r] = {k: Q(event[3]) * v for k, v in rows[event[2]].items() if Q(event[3]) * v} + elif op == 'SCALE': + rows[r] = {k: Q(event[2]) * v for k, v in rows[r].items() if Q(event[2]) * v} + elif op in ('INIT', 'CLEAR'): + rows[r] = {} + else: + need(op == 'MOVE', 'known scalar opcode') + + +def initial(word): + return [{i: Q(1)} for i in range(word['public'])] + [{} for _ in range(word['owned_fields'])] + + +def boundaries(word): + n = word['public'] + rows = initial(word) + charts = word['initial'] + [None] * word['owned_fields'] + prefix, banks, beta = {}, {}, {} + signal = [{} for _ in rows] + for i, event in enumerate(word['program']): + op, r = event[:2] + if op == 'INIT': + need(charts[r] is None, 'INIT is dead') + charts[r] = event[2] + elif op == 'MOVE': + need(charts[r] == event[2], 'MOVE source chart') + charts[r] = event[3] + elif op == 'CLEAR': + need(charts[r] == event[2], 'CLEAR chart') + charts[r] = None + else: + need(charts[r] == event[-1], 'target chart') + if op in ('ADD', 'COPY'): + need(charts[event[2]] == event[-1], 'source chart') + forward(rows, event) + if i == CUT: + signal[PIVOT] = {0: Q(1)} + elif i > CUT: + forward(signal, event) + if i in FIRST or i in SECOND: + banks[i] = {c: tuple(r for r, f in enumerate(charts) if f == c) for c in (595, 603)} + prefix[i] = {r: rows[r].copy() for bank in banks[i].values() for r in bank} + beta[i] = {r: signal[r].get(0, Q(0)) for bank in banks[i].values() for r in bank} + need(charts[:n] == word['final'] and all(f is None for f in charts[n:]), 'final charts/lifetimes') + need(all(not row for row in rows[n:]), 'original owned rows restored') + baseline = rows + columns = initial(word) + suffix = {} + for i in range(len(word['program']) - 1, -1, -1): + if i in banks: + suffix[i] = {r: columns[r].copy() for bank in banks[i].values() for r in bank} + event = word['program'][i] + op, r = event[:2] + if op in ('ADD', 'COPY'): + s, q = event[2], Q(event[3]) + columns[s] = add(columns[s], columns[r], q) + if op == 'COPY': + columns[r] = {} + elif op == 'SCALE': + columns[r] = {k: Q(event[2]) * v for k, v in columns[r].items() if Q(event[2]) * v} + elif op in ('INIT', 'CLEAR'): + columns[r] = {} + else: + need(op == 'MOVE', 'reverse opcode') + transpose = [{} for _ in columns] + for out, row in enumerate(baseline[:n]): + for inp, value in row.items(): + transpose[inp][out] = value + need(columns == transpose, 'full forward/reverse adjoint equality') + need(banks[CUT][595] == (127, 572, 581, 582, 731, 778), 'first chart inventory') + need(word['program'][13652] == ['MOVE', 572, 595, 603, False], 'fixed seam') + return prefix, suffix, banks, beta, baseline + + +def transfer(word, i, target, j): + state = [{} for _ in range(word['public'] + word['owned_fields'])] + state[target] = {0: Q(1)} + for event in word['program'][i + 1:j + 1]: + forward(state, event) + return state + + +def coefficients(case, data, word): + i, u, v, j, s, r = case + prefix, suffix, banks, beta, baseline = data + ell = prefix[CUT][PIVOT] + b1, b2 = beta[i][u], beta[j][s] + g = transfer(word, i, v, j)[s].get(0, Q(0)) + f = add(prefix[i][u], ell, -b1) + h = add(prefix[j][s], ell, -b2) + f[word['public']] = b1 + h[word['public']] = b2 + f = {k: q for k, q in f.items() if q} + h = {k: q for k, q in h.items() if q} + e = {k: -q for k, q in ell.items()} + e[word['public']] = Q(1) + return suffix[CUT][PIVOT], suffix[i][v], suffix[j][r], e, f, h, g + + +def equations(parts, outside): + d, A, B, e, f, h, g = parts + for out in sorted(outside.intersection(set(d) | set(A) | set(B))): + for inp in sorted(set(e) | set(f) | set(h)): + yield (out, inp), [A.get(out, 0) * f.get(inp, 0), + B.get(out, 0) * h.get(inp, 0), + B.get(out, 0) * g * f.get(inp, 0)], -d.get(out, 0) * e.get(inp, 0) + + +def contradiction(eqs): + pivots = {} + for label, values, rhs in eqs: + row = {j: q for j, q in enumerate(values) if q} + weights = {label: Q(1)} + for j, (pivot, value, origin) in pivots.items(): + if j in row: + q = row[j] + row = add(row, pivot, -q) + rhs -= q * value + weights = add(weights, origin, -q) + if not row: + if rhs: + return {label: q / rhs for label, q in weights.items() if q} + else: + j = min(row) + q = row[j] + pivots[j] = ({k: v / q for k, v in row.items()}, rhs / q, + {label: v / q for label, v in weights.items()}) + return None + + +def check_dual(eqs, weights): + """Direct dot products, independent of the elimination/row-add engine.""" + rows = {label: (values, rhs) for label, values, rhs in eqs} + need(weights is not None and all(label in rows for label in weights), 'dual labels') + lhs = [sum((q * rows[label][0][j] for label, q in weights.items()), Q(0)) for j in range(3)] + rhs = sum((q * rows[label][1] for label, q in weights.items()), Q(0)) + need(lhs == [0, 0, 0] and rhs == 1, 'dual proves zero equals one') + + +def literal(word, case, a, b): + """Separate whole-word row interpreter; does not call forward/add.""" + rows = initial(word) + i, u, v, j, s, r = case + for k, event in enumerate(word['program']): + op, target = event[:2] + if op in ('ADD', 'COPY'): + source, q = event[2], Q(event[3]) + old = rows[target] if op == 'ADD' else {} + rows[target] = {c: value + for c in old.keys() | rows[source].keys() + if (value := old.get(c, Q(0)) + q * rows[source].get(c, Q(0)))} + elif op == 'SCALE': + rows[target] = {c: Q(event[2]) * q for c, q in rows[target].items() if Q(event[2]) * q} + elif op in ('INIT', 'CLEAR'): + rows[target] = {} + else: + need(op == 'MOVE', 'literal opcode') + if k == CUT: + rows[PIVOT] = {word['public']: Q(1)} + for when, source, target, q in ((i, u, v, a), (j, s, r, b)): + if k == when: + old = rows[target] + rows[target] = {c: value + for c in old.keys() | rows[source].keys() + if (value := old.get(c, Q(0)) + q * rows[source].get(c, Q(0)))} + return rows + + +def controls(word, data, outside): + eqs = [((0, 0), [Q(1), Q(0), Q(0)], Q(0)), + ((0, 1), [Q(1), Q(0), Q(0)], Q(1))] + witness = contradiction(eqs) + check_dual(eqs, witness) + need(contradiction(eqs[:1]) is None, 'consistent system accepted') + try: + check_dual(eqs, {k: 2 * v for k, v in witness.items()}) + except ValueError: + pass + else: + raise ValueError('forged dual accepted') + cases = [((13637, 127, 572, 13654, 572, 740), Q(2), Q(-3)), + ((13639, 572, 778, 13655, 709, 572), Q(1, 2), Q(3, 2)), + ((13637, 731, 582, 13652, 740, 572), Q(-1), Q(2)), + ((13651, 127, 572, 13654, 740, 572), Q(1), Q(1))] + saw_bilinear = False + for case, a, b in cases: + d, A, B, e, f, h, g = coefficients(case, data, word) + predicted = [row.copy() for row in data[4]] + for out in range(word['public']): + for vector, scale in ((e, d.get(out, 0)), (f, a * A.get(out, 0)), + (h, b * B.get(out, 0)), (f, a * b * g * B.get(out, 0))): + predicted[out] = add(predicted[out], vector, scale) + actual = literal(word, case, a, b) + need(actual == predicted, 'full all-column literal endpoint polynomial') + saw_bilinear |= bool(g) + need(saw_bilinear, 'nonzero bilinear production control') + # The last literal control is also the z-only false positive. + z = word['public'] + need(all(actual[o].get(z, 0) == 0 for o in outside), 'z-only false positive clears leak') + need(any(actual[o] != data[4][o] for o in outside), 'arbitrary-X rejects z-only false positive') + need(any(row.get(z, 0) for row in actual[:z]), 'false positive retains public z') + return {'literal_full_column_cases': len(cases), 'z_only_false_positive': True, + 'consistent_system': True, 'forged_dual_rejected': True, 'bilinear_case': saw_bilinear} + + +def run(word): + data = boundaries(word) + prefix, suffix, banks, beta, baseline = data + outside = {r for r, chart in enumerate(word['final']) if chart != word['final'][PIVOT]} + digest = sha256() + count = 0 + sizes = Counter() + first = None + for i in FIRST: + for u in banks[i][595]: + for v in banks[i][595]: + if u == v: + continue + for j in SECOND: + for s in banks[j][603]: + for r in banks[j][603]: + if s == r: + continue + case = (i, u, v, j, s, r) + parts = coefficients(case, data, word) + witness = contradiction(equations(parts, outside)) + need(witness is not None, 'every declared case has an inconsistent linear relaxation') + d, A, B, e, f, h, g = parts + selected = [] + for out, inp in witness: + need(out in outside and inp in set(e) | set(f) | set(h), 'protected equation label') + selected.append(((out, inp), [A.get(out, 0) * f.get(inp, 0), + B.get(out, 0) * h.get(inp, 0), + B.get(out, 0) * g * f.get(inp, 0)], + -d.get(out, 0) * e.get(inp, 0))) + check_dual(selected, witness) + record = {'case': list(case), 'dual': [[*label, str(q)] for label, q in sorted(witness.items())]} + digest.update((json.dumps(record, sort_keys=True, separators=(',', ':')) + '\n').encode()) + if first is None: + first = record + count += 1 + sizes[len(witness)] += 1 + need(count == 4500, 'complete 15*30*(2+2+6) location-pair domain') + return {'claim': 'Every declared two-ADD seam fails exact outside-V restoration, even with ab independent.', + 'cases': count, 'outside_public_roles': len(outside), 'V_chart': word['final'][PIVOT], + 'dual_size_counts': dict(sorted(sizes.items())), 'dual_sha256': digest.hexdigest(), + 'first_dual': first, 'controls': controls(word, data, outside)} + + +def main(): + manifest = json.loads((HERE / 'SOURCES.json').read_text()) + pin = next(p for p in manifest['files'] if p['path'] == WORD) + raw = (HERE.parents[1] / WORD).read_bytes() + need(sha256(raw).hexdigest() == pin['sha256'], 'authenticated selected word') + word = json.loads(gzip.decompress(raw)) + result = run(word) + encoded = json.dumps(result, indent=2, sort_keys=True) + '\n' + if '--write' in sys.argv: + (HERE / 'RESULT.json').write_text(encoded) + else: + need(json.loads((HERE / 'RESULT.json').read_text()) == json.loads(encoded), 'exact result receipt') + print(encoded, end='') + print('PASS_P104_NONCARRIER_TWO_ADD_SEAM') + + +if __name__ == '__main__': + main() From 6e6236ec763d2aa3eac40201c9634051c583320c Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Tue, 27 Oct 2026 22:12:22 -0700 Subject: [PATCH 2/2] Validate changed-boundary repairs and reject an illegal seam --- .../p104-noncarrier-two-add-seam/PROOF.md | 4 +++ .../p104-noncarrier-two-add-seam/README.md | 27 ++++++++++--------- .../p104-noncarrier-two-add-seam/RESULT.json | 2 ++ .../p104-noncarrier-two-add-seam/verify.py | 18 ++++++++++++- 4 files changed, 37 insertions(+), 14 deletions(-) diff --git a/research/p104-noncarrier-two-add-seam/PROOF.md b/research/p104-noncarrier-two-add-seam/PROOF.md index 6a6dff4ffd..089d6b55e1 100644 --- a/research/p104-noncarrier-two-add-seam/PROOF.md +++ b/research/p104-noncarrier-two-add-seam/PROOF.md @@ -104,6 +104,10 @@ has its own event loop and row arithmetic, separate from the prefix/suffix engine. This is implementation cross-checking by an AI-assisted contributor, not independent human or formal-kernel acceptance. +A synthetic changed-boundary fixture admits a two-ADD non-carrier repair; the +checker does not reject every model by construction. Moving 572 to the wrong +chart is rejected at its actual consumer, and a forged dual is rejected. + A particularly relevant false positive is `127 -> 572` with coefficient 1 after 13651, followed by `740 -> 572` with coefficient 1 after 13654. Its outside z-leak is zero and z survives publicly, but its outside original-X diff --git a/research/p104-noncarrier-two-add-seam/README.md b/research/p104-noncarrier-two-add-seam/README.md index 907c4e10b7..b6bec92f3d 100644 --- a/research/p104-noncarrier-two-add-seam/README.md +++ b/research/p104-noncarrier-two-add-seam/README.md @@ -1,32 +1,33 @@ -# P104: two non-carrier ADDs across the helper572 seam fail +# P104: two non-carrier ADDs across the helper 572 seam fail **Scoped exact exclusion; no new kappa.** On the selected PR6030 word, none of 4,500 declared two-ADD location pairs restores every outside-V output -following the unit overwrite of helper572 after event13637. The corrections +following the unit overwrite of helper 572 after event 13637. The corrections may temporarily change original input rows, so this is outside the carrier-only models of [PR6067](https://github.com/CrocSwap/integer-mult-bounds/pull/6067) and [PR6069](https://github.com/CrocSwap/integer-mult-bounds/pull/6069). -The first ADD is at chart595 after any event13637..13651. The second is at -chart603 after13652,13654 or13655. All original events, fields, charts and +The first ADD is at chart 595 after any event 13637..13651. The second is at +chart 603 after 13652,13654 or13655. All original events, fields, charts and lifetimes stay fixed. Coefficients are arbitrary rationals, including zero. Every original input and the new independent z are symbolic. [PROOF.md](PROOF.md) specifies the complete domain and endpoint polynomial. All cases fail even after relaxing the product `a*b` to an independent third unknown. Each has an exact independently checked linear contradiction: -4,262 use one equation and238 use two. Four separate literal whole-word checks +4,262 use one equation and 238 use two. Four separate literal whole-word checks validate the polynomial on all input columns, including a nonzero interaction -term. A retained false positive clears the z-leak but corrupts original inputs. +term. A synthetic changed-boundary two-ADD repair is accepted, while a wrong +seam chart and a forged contradiction certificate are rejected. A retained false positive clears the z-leak but corrupts original inputs. [RESULT.json](RESULT.json) retains the deterministic certificate digest and counts. The scientific base is canonical main `721c03822c421b7f7fcbb2598993b947c4d88419`, -priority8, selected conditional kappa0.003125804. The canonical investigation is -[Discussion6074](https://github.com/CrocSwap/integer-mult-bounds/discussions/6074). +priority 8, selected conditional kappa 0.003125804. The canonical investigation is +[Discussion 6074](https://github.com/CrocSwap/integer-mult-bounds/discussions/6074). ## Reproduce -Python3.12 and its standard library, from the repository root: +Python 3.12 and its standard library, from the repository root: ```sh python3.12 -I -B research/p104-noncarrier-two-add-seam/verify.py @@ -34,8 +35,8 @@ python3.12 -I -O -B research/p104-noncarrier-two-add-seam/verify.py python3.12 -B scripts/research_package.py --package research/p104-noncarrier-two-add-seam ``` -Direct normal replay took about8.6seconds on macOS arm64. Both registered -modes have30-second limits. Every guard remains active under `-O`. +Direct normal replay took about 8.6 seconds on macOS arm64. Both registered +modes have 30-second limits. Every guard remains active under `-O`. `--write` regenerates only this package's RESULT.json; default replay is read-only. There are no executable pending-PR dependencies: the sole external live input is the selected WORD.json.gz, source-pinned in SOURCES.json and declared in VERIFY.json. @@ -48,9 +49,9 @@ This follows the original-row-changing correction question in PR6067 at credited rather than replayed. The package derives its boundary data directly from the selected word; neither pending proof is an executable dependency. -Preclaim overlap read341open PRs,5,722discussion records and8,348local notes. +Preclaim overlap read 341 open PRs,5,722 discussion records and 8,348 local notes. That metadata coverage is not a novelty guarantee or a search of historical -diffs/unpublished work. The companion receiver-recoding task concerns helper469 +diffs/unpublished work. The companion receiver-recoding task concerns helper 469 and is separate. No fixed-invoice repacking or selected-word application audit is repeated here. diff --git a/research/p104-noncarrier-two-add-seam/RESULT.json b/research/p104-noncarrier-two-add-seam/RESULT.json index f2e870a9d1..00d07b9b67 100644 --- a/research/p104-noncarrier-two-add-seam/RESULT.json +++ b/research/p104-noncarrier-two-add-seam/RESULT.json @@ -7,6 +7,8 @@ "consistent_system": true, "forged_dual_rejected": true, "literal_full_column_cases": 4, + "synthetic_noncarrier_repair": true, + "wrong_seam_rejected": true, "z_only_false_positive": true }, "dual_sha256": "324b646386e6776953c9d3ad52e03ad9d76738c0ca2fc061e20c106e21f73846", diff --git a/research/p104-noncarrier-two-add-seam/verify.py b/research/p104-noncarrier-two-add-seam/verify.py index 3f6b708d5c..7138ef725a 100644 --- a/research/p104-noncarrier-two-add-seam/verify.py +++ b/research/p104-noncarrier-two-add-seam/verify.py @@ -216,6 +216,21 @@ def controls(word, data, outside): pass else: raise ValueError('forged dual accepted') + # A non-carrier two-ADD repair exists in a synthetic changed boundary. + positive = ({0: Q(1), 1: Q(1)}, {0: Q(1)}, {0: Q(1)}, + {0: Q(-1), 1: Q(1)}, {0: Q(1)}, {1: Q(1)}, Q(0)) + need(contradiction(equations(positive, {0})) is None, 'changed-boundary positive admitted') + for _, values, rhs in equations(positive, {0}): + need(values[0] - values[1] - values[2] == rhs, 'positive a=1,b=-1,c=-1') + damaged = dict(word) + damaged['program'] = [event.copy() for event in word['program']] + damaged['program'][13652][3] = 597 + try: + boundaries(damaged) + except ValueError as error: + need(str(error) == 'source chart', 'wrong seam rejected at an actual consumer') + else: + raise ValueError('wrong chart accepted') cases = [((13637, 127, 572, 13654, 572, 740), Q(2), Q(-3)), ((13639, 572, 778, 13655, 709, 572), Q(1, 2), Q(3, 2)), ((13637, 731, 582, 13652, 740, 572), Q(-1), Q(2)), @@ -238,7 +253,8 @@ def controls(word, data, outside): need(any(actual[o] != data[4][o] for o in outside), 'arbitrary-X rejects z-only false positive') need(any(row.get(z, 0) for row in actual[:z]), 'false positive retains public z') return {'literal_full_column_cases': len(cases), 'z_only_false_positive': True, - 'consistent_system': True, 'forged_dual_rejected': True, 'bilinear_case': saw_bilinear} + 'consistent_system': True, 'forged_dual_rejected': True, 'bilinear_case': saw_bilinear, + 'synthetic_noncarrier_repair': True, 'wrong_seam_rejected': True} def run(word):