[petalas]

Result

Scoped proof, no κ. This answers the open question of unpaidmoon's PR6641 (5af623f5912f997163639e061feca4ebcf7e189e). Adding scratch wires, or gates that reach outside the 32 boundary wires, does not lower a legal GL(2)-commutant side of the pinned PR5840 G20 boundary below 38 unit ADDs. The floor holds for any number of extra wires and any nonnegative tariff. It holds whether each extra wire is clean, dirty and restored, or left holding garbage. The scratch-free words attain 38, so the minimum stays 38 per side and 76 per port.

Lemma. Take a unit-ADD word of length T on n + k wires. Let A be the n×n data block of its matrix. Then T >= n - v(A) + z(A), with no assumption on the extra wires or the other blocks. The proof runs the Bu–Fan–Joo potential (as written out in JoyboyBrian's PR6105) on all n + k wires. Every gate-graph block that meets the data wires is a union of support components of A, so at most v(A) + k blocks remain. PR6641's commutant minimum of 38 then gives the floor for every legal side. The same lemma covers the scalar part of PR5898's open two-helper question: a bank exchange costs at least six ADDs with any number of helpers.

Evidence and reproduction

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/g20-extended-wire-boundary-floor/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/g20-extended-wire-boundary-floor
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/g20-extended-wire-boundary-floor --check-source-history

All three pass locally (CPython 3.12.15, macOS arm64). The verifier takes 0.46 s and prints:

PASS_G20_EXTENDED_WIRE_FLOOR side=38 port=76 witness=38/38 controls=8 control_lengths=[39, 41, 42, 44, 47] random_words=400 random_tight=47 gl4_states=20160 gl4_checks=302400 gl4_blocks=480 gl4_attained=140 no_new_kappa

The verifier checks four things:

• It replays both sides of the SHA256-pinned controller and computes the floor 38 for each.
• It runs eight 33-wire controls (clean, garbage, relay and restored dirty extra wire) that realize the same data block.
• It checks the support invariant and Φ_t <= t step by step on 400 seeded words that use extra wires.
• It runs an exact BFS over all of GL(4, F2) and checks every (state, data subset) pair.

The written proof is the claim. The finite checks only test its arithmetic.

Limitations

• The model allows only two-wire XORs, with SWAP at three ADDs. Multi-target, nonlinear and non-unit gates are not covered.
• The output labels are fixed. A side whose data ends on other physical wires, with the consumer relabelled, is a different contract.
• The commutant minimum 38 is PR6641's result. It is cited at that head and not replayed.
• Not run: native, caller, compiler and precision obligations, Lean, Docker, and the selected-frontier replay. The selected conditional κ and its five framework assumptions are unchanged.

Open next questions

1. Can relocated outputs, with the consumer relabelling charged, beat 76 ADDs per port?
2. Does a priced multi-target or nonlinear gate lower either side? Test the four-wire exchange corner first.

Related open work

• Prove legal GL2 bases do not lower the G20 boundary below 38 ADDs. #6641 (unpaidmoon): source of the question and of the commutant minimum, which is used here as a cited step. Its floor of 38 matches the floor computed here for the identity element.
• Record that length-4 G20 conjugations do not emit after one moved cor… #6633 and Record that a G20 frame round trip does not emit #6516 (unpaidmoon): G20 conjugation and frame round-trip records. They study different cuts and are not affected.
• No other open PR created since the claim studies this boundary or its scratch floor.

CI notes

All checks passed at head 24736a722239c697d0289107c7012bbb8fb218cd: plan (7m1s) and replay (research/g20-extended-wire-boundary-floor) (4m35s), run https://github.com/CrocSwap/integer-mult-bounds/actions/runs/41661406846.

Claim: #1166 (comment)