[petalas]

Summary

The remaining 18-register chain/exchange component of the PR5840 G20 boundary (wires 0-15, 30, 31: fourteen chain ADDs plus the bank 7/15 exchange) needs exactly 20 unit ADDs per side. This holds even when gates mix chain and exchange operations, or the even and odd chains, anywhere on those 18 wires. The source attains 20, so joint resynthesis inside this component saves nothing.

- #5850/#5851: isolated four-wire exchanges need 6 each; the 18-register chain/exchange component is open.
+ The 18-register component needs exactly 20 (each of its two closed 9-wire parts needs exactly 10).

With the cited component-local exchange floor, 20 + 3 x 6 = 38 per side and 76 per port stay optimal for synthesis that keeps gates inside each component.

Claim type: finite exhaustive certificate (computer proof) with a written model and a hand proof of the even 9-wire bound. It is not a global 32-wire minimum, a search failure, a new kappa or a complete multiplication theorem. Independent human and formal proof-kernel review are unclaimed. The selected frontier (kappa 0.00310045) is unchanged.

Evidence

• The verifier replays both PR5840 programs against the stored rows, checks that the 18 wires are closed, checks that the right boundary is the exact inverse of the left, and splits the component into the two 9-wire parts.
• For each budget from 0 up to the source cost, an exhaustive depth-first search tries every ADD on the wire set at every node. It prunes only with two admissible bounds: rows still differing from the target, and non-unit columns of the remaining map (the reversed transposed word has the same length). Failed states are memoized by their largest failed budget. A node limit fails the check rather than reporting a bound.
• Budget 19 on 18 wires is excluded after 2,016,480 nodes. A 20-ADD witness is found and replayed on all 2^18 Boolean inputs. Both 9-wire parts are exactly 10.
• Controls: the chain alone needs exactly 14 (13 excluded), a weakened even target fits in nine, and a two-wire exchange needs exactly three.

Reproduction from the repository root (the interpreter used locally was /Users/nick/git/integer-mult-bounds/.venv/bin/python3.12, CPython 3.12):

python3.12 -I -W error -B research/g20-chain-exchange-floor/verify.py
python3.12 -B scripts/research_package.py --package research/g20-chain-exchange-floor
python3.12 -B scripts/check_research_commit.py --package research/g20-chain-exchange-floor --check-source-history

Local results: the direct run prints PASS_G20_CHAIN_EXCHANGE_FLOOR component18=20 even9=10 odd9=10 controls=4 in about 34 s with about 400 MB peak memory. The registered runner runs both commands (normal and -O) and prints PASS_REGISTERED_RESEARCH_PACKAGE in 68 s total. The commit check prints PASS_RESEARCH_COMMIT_BYTES. Each registered command has a 300 s timeout.

The only live input is the PR5840 controller already vendored by #5851 (research/g20-isolated-exchange-floor/inputs/CONTROLLER.json). It is pinned in SOURCES.json and its SHA256 is checked by the verifier.

Limitations

Not covered: gates linking the component to the other 14 boundary wires, GL2 bases inside the equal-target pairs (2k, 2k+1) (they mix the two parts and change the target), scratch or helpers, a changed controller, nonunit tariffs, and all recursive, physical, compiler, precision and analytic obligations. The paid recursive profile is unchanged. The 38/76 totals rely on #5850/#5851's component-local exchange floor, which is cited and not replayed here.

Open next questions

1. Does any scratch-free word on all 32 boundary wires implement one side in fewer than 38 ADDs? First step: the same search on the chain component plus one four-wire exchange (22 wires, budget 25). A stronger bound or written argument is probably needed.
2. Do GL2 bases inside the equal-target pairs lower the 20-ADD component cost? First step: enumerate the pair-basis orbit of the 18-wire target up to cost-preserving symmetries and search the cheapest representatives, then price the caller.

Related open work

No open PR studies the PR5840 boundary words or this component; this account's other open PRs opened since the claim (#5930-#5941, #5943) study different objects. Merged predecessors: #5840 (construction), #5850 and #5851 (four-wire exchange floors; this PR answers their open 18-register / joint chain-exchange question inside the component), and #5898 (one clean helper on an isolated exchange; a different object).

Credit

Ali Romman (#5840) supplied the G20 boundary and controller. Charan . (#5850, #5851) posed the question, proved the exchange floor cited above and vendored the controller used as input. The component decomposition, exact 20-ADD minimum and verifier were produced by Nick Petalas.

CI notes

All checks passed at head 1f1c37ba713d027fb0c568f0dcfa41c42feaa884: plan and replay (research/g20-chain-exchange-floor) in run https://github.com/CrocSwap/integer-mult-bounds/actions/runs/40524983592 (replay job 3m45s).