Prove the six-ADD bank-exchange floor with one clean helper

research/clean-helper-bank-exchange/PROOF.md

@@ -0,0 +1,148 @@
+# One clean helper does not lower the bank-exchange floor
+
+This result was produced by Nick Petalas. It is an exact finite certificate
+with a written reduction to a scalar circuit problem. Independent human and
+formal proof-kernel review are unclaimed.
+
+## Statement and changed premise
+
+Let `a0,a1,b0,b1` be independent inputs over F2 and let `z=0` initially.
+A paid ADD replaces one of these five wires by its XOR with a distinct wire.
+Every one of the twenty ordered directions is allowed. A word is finite,
+straight-line and independent of the input values. No other operation is
+allowed, including reset, overwrite, free permutation or intermediate basis
+change. The final helper must be zero for every data input.
+
+For any `A,B in GL(2,F2)`, the requested data endpoint is
+
+```text
+(a', b') = (A b, B a),       z' = 0.
+```
+
+Every such word needs at least six ADDs. Two endpoint choices attain six,
+so the minimum over the allowed endpoint bases is exactly six.
+This does not determine every endpoint's exact length above that floor.
+
+Charan .'s [PR #5851](https://github.com/CrocSwap/integer-mult-bounds/pull/5851)
+proves the corresponding no-scratch floor. Its exact source head is
+`c698080add27ea02f62da393f27f05c537558ff8`. That package explicitly excludes
+added scratch. The new claim grants one zero helper and all incident ADDs.
+The predecessor result and its complete distance census are cited, not
+replayed or used to prove this stronger finite statement.
+
+## Exact state reduction
+
+Represent each live wire by its four coefficients on the independent data
+inputs. The initial five rows are `(1,2,4,8,0)`, with bit `i` denoting input
+`i`. The matrix is five by four, rather than a five-by-five identity: its last
+input is fixed to zero, and must not be treated as independent dirt.
+An ADD XORs the source row into the destination row. This description is
+exact by induction on the word, including every use of the helper.
+
+The two nonzero rows of an invertible binary two-by-two matrix are any
+ordered pair of distinct elements of `{1,2,3}`. There are six choices per
+bank, hence exactly 36 target coefficient states
+
+```text
+(4u, 4v, w, x, 0),
+u,v,w,x in {1,2,3}, u != v, w != x.
+```
+
+Here `4u` means an ordinary integer left shift by two in the row encoding.
+Independent invertible entrance and exit bases within the two banks give
+exactly this endpoint class. All instructions realizing the endpoint remain
+paid. A choice of endpoint does not grant free basis changes during the word.
+
+## Complete exclusion of length at most five
+
+Let `Ball_r(q)` be the set of coefficient states obtained from `q` by at
+most `r` ADDs. Every ADD is its own inverse. Therefore a word of length at
+most five from the initial state `s` to a target `t` exists if and only if
+
+```text
+Ball_2(s) intersects Ball_3(t).
+```
+
+For the forward implication, split after at most two instructions. The
+remaining suffix has length at most three, and its reverse reaches the split
+state from `t`. The reverse implication concatenates the prefix and reversed
+suffix. Shorter words are included throughout.
+
+The generated certificate and independent checker establish the following
+finite facts. Forward distance layers are `1,16,166`, totaling 183 states.
+For each of the 36 targets, backward distance layers are `1,16,166,1302`,
+totaling 1,485 states. Every one of the 36 intersections is empty. The
+53,460 backward states counted over targets need not be distinct across
+targets; no union cardinality is claimed.
+
+`generate.py` builds the coefficient-state balls by breadth-first layers.
+It emits their sorted-state SHA256 digests, counts and two attaining words.
+`verify.py` imports no generator code. It evaluates wires on every one of
+the sixteen data assignments, stores five literal sixteen-bit truth tables,
+and enumerates all padded words of lengths two and three directly. The
+padding symbol does nothing and only includes shorter paid words. It is
+not a free data operation. There are `21^2=441` padded prefix words and
+`36*21^3=333396` padded backward words for the main exclusion.
+The checker reconstructs every digested state set and checks disjointness.
+Hashes bind the certificate; exact enumeration supplies the exclusion.
+
+This is a complete exclusion in the finite stated circuit model, rather
+than a heuristic search failure. It remains a computational certificate,
+not a proof-assistant theorem.
+
+## Attainment and vector inputs
+
+For each pair of distinct wires `(i,j)`, the three ADDs
+
+```text
+i += j;  j += i;  i += j
+```
+
+swap their arbitrary initial values. Swapping `(0,2)` and `(1,3)` attains
+`A=B=I`. Swapping `(0,3)` and `(1,2)` attains the crossed orientation in
+both banks. Both words have six instructions and leave the helper untouched.
+The verifier checks both complete truth tables and helper restoration.
+The swap identity is standard and is not claimed as new.
+
+The same identities apply coordinatewise to arbitrary equal-length vectors
+over F2, with one full vector ADD as the unit operation. A universal shorter
+word would in particular work on one-bit inputs, contradicting the finite
+exclusion. The same floor also holds for an arbitrarily dirty restored
+helper: specialize its initial contents to zero. The attaining words already
+leave every possible helper value untouched.
+
+## Source relevance and limitations
+
+Ali Romman's [PR #5840](https://github.com/CrocSwap/integer-mult-bounds/pull/5840),
+head `6a043d0fc0199ee5b24c61f883f1943eaf6424be`, supplies the G20 bank-boundary
+construction and general-basis question. Under #5851's retained decomposition
+into fixed chain instructions and isolated four-wire exchange components,
+granting one private clean helper to a component cannot reduce its six-ADD
+floor. That conditional application uses the cited source decomposition;
+the actual controller is not imported or independently replayed here.
+
+Two or more helpers, cross-component gates, sharing with the chain, changed
+tariffs, nonlinear operations, data-dependent control, and a nonrestored helper
+are outside this certificate. There is no global boundary minimum, native
+implementation, physical supplier admission or new kappa. Initialization,
+ownership, movement and all other physical helper costs are unpriced here;
+granting the clean helper at no extra charge favors a proposed improvement.
+Any complete implementation must pay those costs as well as every ADD.
+The five selected framework assumptions and selected frontier are unchanged.
+
+## Verifier bounds
+
+All enumeration loops have fixed finite bounds. The largest direct word set
+has at most 9,261 entries and each state uses at most eighty bits. Only one
+target's balls are live during the main exclusion. Certificate input is capped
+at 64 KiB, the endpoint inventory at 36 and each attainment at six ADDs.
+Functions stay below sixty lines. Explicit exceptions preserve checks under
+optimization. There is no recursion, subprocess, network, runtime code
+generation or mutable external state in the direct verifier.
+
+Python integers, sets and JSON require managed allocation. The fixed domains
+bound it; no allocation-free execution is claimed. Seven explicit mutations
+exercise certificate rejection, without callbacks or input-selected code.
+Warning-strict normal and optimized
+replays provide the available interpreted-language diagnostics. No global
+lint configuration or unrelated source is changed.

research/clean-helper-bank-exchange/README.md

@@ -0,0 +1,96 @@
+# Sharp bank-exchange floor with one clean helper
+
+This finite certificate was produced by Nick Petalas. Exchanging two arbitrary
+two-wire binary banks needs at least **six paid ADDs**, even with one initially
+zero helper restored to zero and arbitrary invertible endpoint bases within
+the banks. All 36 endpoint choices are excluded at length at most five.
+Two ordinary matching exchanges attain six. Exact lengths above the floor
+for the other endpoint choices are unclaimed.
+
+This extends the no-scratch model of Charan .'s
+[PR #5851](https://github.com/CrocSwap/integer-mult-bounds/pull/5851).
+Ali Romman's [PR #5840](https://github.com/CrocSwap/integer-mult-bounds/pull/5840)
+supplies the G20 bank-boundary construction and general-basis question.
+Neither predecessor's verifier is imported or replayed. The new contribution
+is the added-helper exclusion, not their no-scratch census or standard swap
+construction. Exact heads and roles are recorded in [SOURCES.json](SOURCES.json).
+
+Every ADD among the five wires costs one. No reset, free basis change,
+overwrite or other data operation is granted. The proof also gives the same
+floor for arbitrary vector width and for a restored dirty helper by restriction
+to zero initial dirt. See [PROOF.md](PROOF.md) for the exact model and reduction.
+
+## Evidence
+
+The forward radius-two ball has 183 injection states. Each of the 36 backward
+radius-three balls has 1,485 states. All 36 intersections are empty. A generator
+using coefficient rows emits [CERTIFICATE.json](CERTIFICATE.json); a separate
+checker enumerates literal truth tables on all sixteen data assignments.
+It checks 441 padded prefix words and 333,396 padded suffix words for the main
+exclusion, both six-ADD attainments, seven rejection controls, twenty one-ADD
+positive controls and a helper-touching five-ADD positive meet.
+
+This is a complete finite exclusion with a scoped mathematical reduction.
+Independent human and formal proof-kernel review are unclaimed.
+The direct verifier prints a generated receipt binding every package file's
+SHA256 to the actual counts and interpreter version. Receipts and replay logs
+are outputs, not handwritten package evidence.
+
+## Reproduce
+
+From the repository root, use CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/clean-helper-bank-exchange/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/clean-helper-bank-exchange/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/clean-helper-bank-exchange
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/clean-helper-bank-exchange --check-source-history
+```
+
+Both direct commands must end with `PASS_CLEAN_HELPER_BANK_EXCHANGE`.
+Use another CPython 3.12 path when reproducing on another machine. Direct
+verification needs only this package and works without Git or network.
+The source-history preflight needs the committed package and full Git ancestry.
+
+To regenerate the certificate, redirect `generate.py` stdout to an external
+scratch file, then compare that file byte for byte with `CERTIFICATE.json`.
+The generator never writes the package. Both registered verification commands
+have a 120-second timeout. Their measured local runtimes belong in the PR body.
+
+## Scope and research record
+
+Base is canonical main `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority
+revision 8. [TASK.json](TASK.json) records the changed connector card premise,
+stop rule, source attribution and
+[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216124).
+The first working example was the five-by-four identity injection with one
+zero row. The original card's old connector census was read for its interface;
+replaying another result was excluded by the research assignment.
+
+This is a local obstruction to an added-workspace route. Two or more helpers,
+cross-component gates, shared chain operations and the complete physical bill
+remain outside its scope. No global CNOT minimum, new supplier, kappa or
+complete multiplication theorem is claimed. The selected frontier is unchanged.
+No full native/caller replay, Lean, Docker or historical suite was run.
+
+## Open next questions
+
+Can two clean helpers reduce the floor? A first step is the same length-five
+meet with two zero rows, with every ADD counted. That is a new finite domain
+and is not decided here. It matters only if ownership, initialization and
+movement can also fit the complete caller bill.
+
+Can cross-component synthesis or sharing with the fixed chain shorten the
+whole boundary? A strictly shorter exact source-bound boundary and inverse
+would be the first useful witness. Complete native and caller costs remain
+the blocker to supplier use.
+
+## Credit and license
+
+The added-helper result, certificate and independent checker were produced by
+Nick Petalas. Credit Charan . for #5851, Ali Romman for #5840, and the retained
+#5834, #5807/#5828, #5708/#5671, ai-nanachi #5512, Dugongue, ToikY and native,
+controller, compiler and BIT source lineage credited there. No predecessor
+source is copied or modified. Breadth-first enumeration, meet in the middle,
+elementary transvections and the three-ADD swap are standard techniques.
+New work is Apache-2.0 under the repository license.

research/clean-helper-bank-exchange/SOURCES.json

@@ -0,0 +1,35 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ],
+  "mathematical_references": [
+    {
+      "pr": 5851,
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5851",
+      "head": "c698080add27ea02f62da393f27f05c537558ff8",
+      "path": "research/g20-isolated-exchange-floor/PROOF.md",
+      "author": "Charan .",
+      "use": "Question source and no-scratch predecessor. Cited, not an executable or a mathematical dependency of the finite five-wire enumeration."
+    },
+    {
+      "pr": 5840,
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5840",
+      "head": "6a043d0fc0199ee5b24c61f883f1943eaf6424be",
+      "author": "Ali Romman",
+      "use": "G20 bank-boundary construction and general-basis question, used only as motivation."
+    }
+  ]
+}

research/clean-helper-bank-exchange/TASK.json

@@ -0,0 +1,75 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "connector-alphabet-change",
+    "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/universal-connector-boundary/README.md",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Construct and charge a legal extra operation on a minimal instance.",
+      "Prove a target-specific bound after adding one specified operation family."
+    ],
+    "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. 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",
+        "research/universal-connector-boundary/verify.py"
+      ],
+      "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY",
+      "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.",
+    "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.",
+    "allowed_variations": [
+      "Choose one additional operation and a small source count for its first counterexample."
+    ],
+    "scope_change_triggers": [
+      "Keeping the alphabet and only increasing the source count; record this as a changed assignment.",
+      "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions."
+    ],
+    "overlap_terms": [
+      "universal connector",
+      "source-toggle",
+      "connector alphabet"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exclude at most five directed binary ADDs for all 36 two-bank exchange endpoints with one initially zero helper restored to zero; attain six on the straight and crossed matching exchanges.",
+  "scope_change_reason": "The card asks for a new connector operation. This side result instead changes the workspace premise of PR5851 by adding one clean helper and all eight incident ADD directions. Its first working example is the five-wire identity injection, rather than a replay of the predecessor connector census.",
+  "bottleneck_link": "Rules out a proposed local route to cheaper G20 bank boundaries. Under isolated exchange components and fixed chain instructions, one private clean helper per component cannot beat the cited six-ADD component floor. No global supplier claim.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first certified extension or shorter exact witness. Do not enlarge helper count or synthesize the complete boundary.",
+  "outcome": "negative-result",
+  "evidence": "CERTIFICATE.json plus independent literal truth-table short-word enumeration in verify.py; written reduction in PROOF.md.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can two or more clean helpers lower the six-ADD minimum for a general two-bank endpoint?",
+      "why_it_matters": "Determines whether the remaining scratch route is worth considering before a complete caller rewrite.",
+      "first_step": "Add a second zero row to the injection model and test the same length-five meet.",
+      "blocked_by": "Not covered by the present five-wire enumeration; every ADD and helper ownership must still be paid."
+    },
+    {
+      "question": "Can cross-component synthesis or sharing with the fixed chain beat the complete boundary?",
+      "why_it_matters": "These interactions escape the component floor even with one helper.",
+      "first_step": "Construct one strictly shorter source-bound full boundary and its inverse, retaining target pairs.",
+      "blocked_by": "Requires actual source endpoint and full native/caller invoice; no claim follows from the local result."
+    }
+  ],
+  "predecessor": {
+    "pr": 5851,
+    "head": "c698080add27ea02f62da393f27f05c537558ff8",
+    "author": "Charan .",
+    "relationship": "The new result changes its explicitly excluded added-scratch premise; no predecessor executable is imported or replayed."
+  },
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216124"
+}

research/clean-helper-bank-exchange/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "All 36 clean-helper exchange endpoints, full radius-two/radius-three meet, literal attainments and semantic controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same exact exclusion and controls with assertions disabled."
+    }
+  ]
+}