[petalas]

Summary

Prove the sharp approximation floor for replacing a real two-coordinate orthogonal gate U by an exactly unitary matrix over D=Z[i,1/2]:

m = max |U_ij|
minimum squared operator error = 2(1-m)

A real signed permutation attains the bound. Any finite number of arbitrary independently dirty helpers, returned exactly for every input, leaves the minimum unchanged. The rational butterfly [[3/5,4/5],[4/5,-3/5]] has exact squared error 2/5; the worst floor over real O(2) is 2-sqrt(2).

Claim type: scoped written mathematical proof with exact finite corroboration. No new kappa. Only research/dyadic-two-wire-approximation/ is added.

Evidence

• Before: Jose Manuel's PR4205 supplies exactly unitary rational FFT coefficient gates, with dyadic data rounding handled separately. Replacing their coefficients by exact Gaussian-dyadic unitaries would change that arithmetic boundary.
• After: PROOF.md gives the exact distance for every real target and a block-matrix proof covering arbitrarily many exactly restored helpers. A positive precision-independent floor excludes an arbitrarily accurate replacement of a nontrivial real butterfly in that model.
• The standalone checker joins all possible columns by two constructions and compares all 96 resulting unitaries against 368 rational rotations/reflections: 35,328 exact operator comparisons. Exact Hermitian principal minors avoid floating eigenvalues. It also checks 2,304 forbidden one-helper leakage blocks, 96 restored-helper positives and six threshold/domain/semantics rejections. A closer nonunitary dyadic control has squared error 1/320 and norm square 61/64, exposing the exact-unitarity premise.
• Warning-strict normal and optimized commands passed locally in 0.169 and 0.130 seconds. Their complete generated receipts agree byte for byte. Registered replay passed in 0.522 seconds. These are check durations, not a speedup claim.
• All six committed files, executable modes and canonical-base source history pass preflight. Official export integrity and both read-only, Git-free, empty-PATH direct replays pass with unchanged complete receipts. Receipts are generated and bind all package files plus the per-target transcript.

Exact reproduction from the repository root, CPython 3.12 standard library:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/dyadic-two-wire-approximation/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/dyadic-two-wire-approximation/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/dyadic-two-wire-approximation
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/dyadic-two-wire-approximation --check-source-history --check-modes

Any CPython 3.12 path can replace the absolute interpreter path. Local environment: CPython 3.12.15, macOS arm64. Expected direct status: PASS_DYADIC_TWO_WIRE_APPROXIMATION.

Limitations and credit

The claim concerns linear, exactly unitary Gaussian-dyadic maps at a restored two-active-coordinate boundary. It supplies no global FFT lower bound, physical coefficient-delivery tariff, favorable complete supplier bill or exclusion of nonunitary dyadic lifting, rounded maps, larger active boundaries or cancellation among changed gates. Physical tapes, precision, stock, compilation and complete multiplication remain open. The selected result and all five framework assumptions are unchanged. Selected cold replay, Lean, Docker, independent human and formal proof-kernel acceptance are unrun or unclaimed.

The 96-element dyadic-unitary group is classical, including De Vos, Van Laer and Vandenbrande's 2012 paper. That classification is credited, not claimed as new. The contribution is the sharp distance formula and its exact-restored-helper interface consequence. Credit Jose Manuel/jmbarrancoml's PR4205 rational child, Vlado Vojdanovski, Chafik Boukhalfa, Mason Hale, Jeremy Kothe/IdeaOuter, Cinna Davis and their retained lineage. MatShep's merged PR5549 studies tensor faithfulness of the same group, a different quantity. No predecessor scientific replay is presented as new evidence. No worldwide literature-priority claim is made.

Scientific base: canonical main 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8, selected PR6030; unchanged at prepublication fetch. Exact source-document pins are provenance. The overlap helper covered 555 open PR bodies and 6,598 Discussion records with complete pagination at its recorded refresh; sparse local coverage was 135 of 8,917 note records. Distinctive all-main README and merged-PR searches supplemented that incomplete local coverage. Bounded searches do not establish absence of unpublished overlap.

Advance CLAIM.

Related open work

• PR6619 classifies injective norm-nonincreasing rounding of rational orthogonal maps on one fixed lattice, permitting nonlinear maps. This result optimizes continuous linear Gaussian-dyadic coefficient maps under exact unitarity. These contracts do not report the same numerical minimum.
• PR6605 proves correction-rank bounds for separating higher-dimensional Gaussian coordinate banks. This result concerns two-coordinate approximation error; no correction-rank comparison is made.
• PR6610 implements the complete two-qubit Clifford replay. This result concerns two-dimensional Gaussian-dyadic approximation, with no claim about that larger finite-group replay or its tensor thresholds.

The completion refresh inspected all returned account open PRs, including the fifteen other contributions created since the advance CLAIM. None reports a competing value for this exact two-wire approximation quantity. The related lines compare published contracts only; no additional scientific computation audited another result. PR4205 and PR5549 are merged predecessors. Sparse notes, arbitrary historical diffs, unpublished work and later changes remain overlap limits.

Open next questions

Can a nonunitary dyadic lifting replacement of one rational butterfly meet its full composed error/restoration budget with cheaper complete coefficient delivery? Start with the pinned PR4205 butterfly, an exact dyadic shear factorization, explicit rounding sites and inverse, and bound its intermediate norms. Stability, fixed-grid restoration and a favorable physical invoice are missing. No follow-up is reserved.

CI notes

Both hosted checks, plan and replay (research/dyadic-two-wire-approximation), passed at exact head 6341bc34e9ca9b24e962ac12064fe56979984dd6 in run 41634572504. The completed checks were read once with gh pr checks 6614 --repo CrocSwap/integer-mult-bounds; separate run metadata confirms completed success and the matching head.

All registered normal/optimized checks, direct checks, committed-byte/mode/source-history preflight and read-only exported replay also passed locally. No local executable obligation was deferred to CI. Hosted execution replays the finite checker and metadata; the written universal proof remains separate, with independent human and formal proof-kernel review unclaimed.

Merge Danger

Door: two-way. Blast radius: isolated. The six-file package changes no shared implementation, pinned evidence, upstream archive, selected certificate or other contributor's credit.