[petalas]

Summary

Scoped constructive proof and an explicit compiler improvement. One arbitrary common-chart spare realizes the dyadic dual-pair exchange

ab = 1
S = [[I-ba,b],[a,0]], S^2 = I
S; G_on_spare; S: (x,z) -> (x+b(G-I)ax,z)

The compiler uses three block shears and one sign SCALE, with only signed input coefficients. It emits no Euclidean quotient or odd division. Three block shears are necessary for this particular exchange even with free invertible block-diagonal maps; unrestricted scalar-circuit optimality is not claimed.

For a=(3,5), b=(2,-1), the unmodified PR5611 compiler on the same three roles emits 20 gates with real scalar allowance 134. This compiler emits 7 gates with allowance 64. The new result is the coefficient-preserving compiler application, its exact tariff and scoped dirty-spare consumer guarantee. Elementary block factorization and stabilized completion are classical. No new kappa or selected-frontier change.

Only research/division-free-dual-exchange/ is added. This contribution was produced by Nick Petalas. Credit Ali Romman / PR5611 for the complete dual-pair specification and Euclidean compiler, PR5602 for the scalar tariff and helper interface, PR5599 and the retained P104/native/controller/compiler lineage. PR5115 is a different earlier source-only borrowing contract. Advance claim.

Evidence

• Before: named padded nonunit pair, 20 emitted gates and allowance 134.
• After: seven explicit gates and allowance 64, satisfying the same row/column boundary equations on the same three roles. The complementary action may differ. The predecessor's emitted program is the comparison, not a globally optimal completion.
• Exact dense replay covers 116 integer pairs, 64 dyadic pairs through dimension eight, three valid compiler-limit cases, nine full two-coordinate-field consumers and nineteen rejecting controls. Every scalar prefix is bounded; normal and optimized runs agree.
• Warning-strict direct checks took 0.110 and 0.108 seconds on macOS arm64 / CPython 3.12.15. The complete registered launcher took 0.522 seconds. These are check durations, not a runtime-improvement claim.
• Committed-byte/mode and declared source-history checks pass at 4d6e4374d6fdda7df72ddeb19dd6756353383346 for all eleven package/input files. Official export and input-coverage checks pass. Both read-only Git-free replays with an empty PATH pass; all twelve exported files, including the export inventory, remain byte-identical. An actual retained-source byte mutation rejects normally and under optimized Python.
• RESULT.json is generated and bound to the package files and live inputs. The scientific predecessor suite was not replayed; its compiler is called only on the named pair to compare emitted work.

Reproduce from the repository root with CPython 3.12, standard library only:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/division-free-dual-exchange/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/division-free-dual-exchange/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/division-free-dual-exchange
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/division-free-dual-exchange --check-source-history --check-modes

Expected markers: PASS_DIVISION_FREE_DUAL_EXCHANGE, PASS_REGISTERED_RESEARCH_PACKAGE, PASS_RESEARCH_COMMIT_BYTES. Another CPython 3.12 path can replace the one shown.

Limitations

The spare must be physically available at the required chart. During the basis map alone it contains ax; return is proved only for the stated complete S/G/S consumer. No actual P104 cut, new productive target, native realization, rounded precision allocation, favorable complete signed invoice or supplier admission is supplied. G, routing, allocation/lifetimes, chart changes and restoration outside the stated algebra remain payable. All five selected framework assumptions remain. No selected scientific cold replay, Lean proof or independent human/formal-kernel review was run.

The exact scalar price is the cheaper of two displayed factorizations. It is not a global optimum. Compiler input bounds do not widen the source caller's coefficient-magnitude cap. The block identities are all-dimension statements; finite replay alone does not prove them.

Related open work

• Conditional κ 0.00309871 from a prepared P104 split helper #5606 changes a physical prepared P104 helper and its complete invoice; this package supplies an optional scalar-basis module and finds no physical split.

• Construct an exact dyadic rank-seven P104 projector (no new kappa) #6247 constructs a dyadic rank-seven P104 projector; it does not supply this spare-role completion, and its approximation objective is not compared here.

• Prove an exact integer dirty-fanout shortening gap (no κ) #6277 proves an integer dirty-fanout tariff with a preserved source; this has a different dual-pair basis contract, a spare coordinate and coefficient-dependent dyadic pricing. Neither result is audited or extended by the other here.

• Reduce complete dirty-certificate replay time by 22.57% (no new κ) #6279 accelerates the general dirty-linear certificate checker by reusing path prefixes; this package supplies an explicit dual-pair circuit and uses its own dense interpreter. There is no shared numerical optimum to compare.

The account's open PRs created since the advance claim were refreshed through #6283. No additional PR specifically providing this division-free spare-role dual-pair completion was found. Search coverage remains bounded.

Open next questions

1. Pin one current word/cut with a compatible arbitrary spare at every required chart. Price all transports and target debits before installing this compiler.
2. Match one actual G to the complete S/G/S consumer and charge its native, routing, precision and storage obligations. The one-call algebra alone gives no supplier saving.

CI notes

Both hosted checks, plan and replay (research/division-free-dual-exchange), passed at 4d6e4374d6fdda7df72ddeb19dd6756353383346 in run 41068426684. The completed checks were read once, and run metadata confirms success at the matching head. Hosted CI certifies the registered replay and planning checks; it is not independent scientific or formal-kernel acceptance. All local registered and publication/export checks above also pass.

Merge danger

Two-way door. Blast radius is the isolated research package. Shared code, predecessor sources, pinned evidence and the selected frontier are unchanged.