[petalas]

Summary

A finite exact certificate proves that one initially zero, restored helper cannot lower the six-ADD minimum for exchanging two arbitrary two-wire binary banks, even with arbitrary invertible endpoint bases. All twenty directed ADDs on the five wires are paid. All 36 endpoints need at least six; two ordinary matching exchanges attain six. Exact lengths above that floor are unclaimed.

- Four data wires, no scratch: minimum over bank bases is six ADDs.
+ Four data wires and one clean restored helper: the minimum is still six.

The added-helper exclusion was produced by Nick Petalas. Credit Charan . #5851 for the no-scratch result and explicitly excluded scratch premise, and Ali Romman #5840 for the G20 boundary construction and general-basis question. Their exact heads are recorded in SOURCES.json. No predecessor executable or census is imported or replayed. Standard meet-in-the-middle enumeration and the three-ADD swap are not claimed as new.

Claim type: finite certificate with a scoped written reduction to arbitrary vector inputs, not a search failure, new kappa or complete multiplication theorem. Independent human and formal proof-kernel review are unclaimed. The selected frontier is unchanged.

Evidence

Before, #5851 excluded added scratch. After, the five-by-four input injection includes a zero helper, rather than an independent fifth dirty input. Its radius-two ball has 183 states. Each of the 36 target radius-three balls has 1,485 states, and all 36 intersections are empty. A coefficient-row generator and separate literal truth-table checker agree on every set digest and count.

The checker enumerates 441 padded prefix words and 333,396 padded suffix words for the main exclusion. It checks both six-ADD attainments, seven rejected certificate mutations, twenty one-ADD positive controls and a helper-touching five-ADD positive meet. Generated stdout receipts bind all eight package files and CPython 3.12.15 to the actual result.

From the repository root, exact local reproduction commands are:

/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 print PASS_CLEAN_HELPER_BANK_EXCHANGE. The registered runner prints PASS_REGISTERED_RESEARCH_PACKAGE; committed-byte/source-history checking prints PASS_RESEARCH_COMMIT_BYTES. Each registered command was also timed directly at about 0.45 seconds locally, well below its 120-second timeout. This is timeout evidence, not a performance comparison.

Certificate regeneration is byte-identical. Official committed-package export and integrity checks pass. Separate normal and optimized read-only Git-free export replays pass with empty PATH, and all nine exported files including the manifest retain their hashes. The standalone verifier uses only the package and Python's standard library. Metadata/pins and staged whitespace checks pass. All touched functions are below sixty lines; the bounded managed-allocation deviation is recorded in PROOF.md.

Limitations

The result covers one clean helper restored to zero, straight-line binary ADDs and unit gate tariffs. It also implies the same floor for a restored dirty helper by specializing its initial value to zero. It does not cover multiple helpers, cross-component synthesis, sharing with the chain, unreturned scratch, nonlinear operations or data-dependent control.

The conditional G20 relevance retains the source's isolated-component decomposition. No actual controller, native operator, physical caller, compiler, stock, precision/tape or analytic obligation was replayed or discharged. No global boundary minimum is claimed. Helper initialization and physical costs must be charged by a complete caller. No Lean, Docker or historical suite was run.

Open next questions

• Can two clean helpers reduce the floor? Start with the same length-five meet on six wires; charge all helper ownership and ADDs before drawing a supplier conclusion.
• Can a complete boundary share gates across components or with the chain? The first useful witness is a strictly shorter exact source-bound boundary and inverse, followed by its full native/caller bill.

Related open work

• Prove a six-ADD floor for isolated G20 bank exchanges under general binary bases #5851 proves the isolated no-scratch floor and supplies this question's source. The new added-helper floor is also six; its full endpoint-distance histogram is not recounted here.
• [negative result] Certify the GL2 floor for three G20 boundary exchanges #5850 certifies no-scratch GL2 choices for selected G20 tail components. Its stated six-ADD component floor agrees with this result, which changes the helper premise.
• Halve G20 boundary work with equal-target bases and a complete physical caller #5840 constructs the complete target-pair boundary. This local exclusion grants extra workspace inside an isolated component; it does not re-optimize that complete boundary.
• Construct a shorter G20 word: 245 fewer ADDs per call with exact endpoints #5807 shortens local G20 core words through exact small-window synthesis. This result concerns bank exchange with a clean helper, not its emitted core word.
• Remove 1350 G20 ADDs through exact dependency-trace resynthesis #5828 resynthesizes dependency traces across commuting operations. Such cross-component sharing remains outside this certificate.
• Install the shorter G20 word in all 18 physical calls with fresh source records #5834 installs shorter local cores throughout the physical caller. This package does not rebuild or recheck those source records.
• Audit the complete G20 caller and exact port interfaces #5798 studies complete G20 caller and port bindings. Those physical obligations remain separate from this scalar obstruction.

Related work was refreshed against this account's seven other open PRs created since the advance CLAIM: #5897, #5899, #5900, #5901, #5902, #5903 and #5904. None computes this bank-exchange ADD minimum or supplies a conflicting same-instance number. No extra computations were run to validate those contributions.

CI notes

At head eab71a61c7465a2b5c33726174433d9dfd3e07ca, run 40500670034 has plan failed; replay skipped. The only failed step is Onboarding helper tests. All ten failure/error entries are in unchanged tests/test_research_current_assignment.py, ending FAILED (failures=8, errors=2, skipped=22). The two errors are KeyError: 'follow_up_steps' and KeyError: 'catalog_first_step'; the eight failed assertions concern current/historical commands, missing-reference validation and sparse path expectations.

The ten failure/error headers and final summary match the inspected PR #5897 run. This confirms the reported shared main de5ec2e7a onboarding failure. Maintainers will handle that repair. No shared tests or implementation files were changed.

Hosted replay has not certified this package. Only the local scientific checks above have run.

Advance claim: #1166 (comment)

Merge Danger

Door: two-way. This adds one isolated research package.

Blast Radius: package. No selected record, shared verifier, predecessor package or pinned source changes.