Prove sharp dyadic two-wire approximation floors (no κ)

research/dyadic-two-wire-approximation/PROOF.md

@@ -0,0 +1,141 @@
+# Sharp approximation by exact Gaussian-dyadic two-wire gates
+
+This scoped proof and its application were produced by Nick Petalas.
+New material is Apache-2.0.
+
+Put D = Z[i,1/2]. Norms below are Euclidean operator norms on complex
+coordinate vectors. The target U is any real 2 by 2 orthogonal matrix;
+in particular it can be a real rotation or a normalized real butterfly.
+Write m = max over i,j of |U_ij|.
+
+## The approximation theorem
+
+For every such U,
+
+    min { ||V-U||_op^2 : V* V = I_2, V in D^(2 by 2) } = 2(1-m).       (1)
+
+A real signed permutation attains the minimum. Complex coefficients and
+arbitrarily large dyadic denominators cannot improve it. Consequently the
+worst minimum over real O(2) is 2-sqrt(2), attained by balanced butterflies.
+
+### Classical dyadic unit-vector lemma
+
+A unit vector in D^2, regarded as a real four-coordinate vector, is either
+a signed coordinate vector or has all four coordinates equal to +/-1/2.
+
+Choose its least common denominator 2^k. Its integer numerators satisfy
+
+    x_1^2 + x_2^2 + x_3^2 + x_4^2 = 4^k.
+
+If k>=1, the number of odd numerators is divisible by four, by reduction
+modulo four. Minimality excludes zero odd numerators, so all four are odd.
+For k>=2 their squares sum to 4 modulo eight, whereas 4^k is 0 modulo
+eight, a contradiction. For k=1 the four odd squares sum to four, forcing
+each numerator to be +/-1. For k=0 only a signed coordinate vector is
+possible. This is the classical small-dimensional dyadic-unitary argument,
+not a new group-classification claim.
+
+### Lower bound
+
+Let u=(a,c) be the first column of U, and v the first column of V.
+Real two-dimensional orthogonality gives
+
+    a^2+c^2=1,     max(|a|,|c|)=m.
+
+If v is a signed coordinate vector in its four real components, then
+Re(u* v) <= m. If its four real components are all +/-1/2, then
+
+    Re(u* v) <= (|a|+|c|)/2 <= m.
+
+Both vectors have norm one. Thus
+
+    ||V-U||_op^2 >= ||v-u||_2^2 = 2-2 Re(u* v) >= 2(1-m).
+
+This lower bound concerns the full complex operator norm, even though the
+target is real. It does not discard imaginary leakage into either output.
+
+### Attainment
+
+Let delta=det U, which is +/-1. Choose p to be the signed coordinate
+vector with u dot p = m. Set
+
+    J = [[0,-1],[1,0]],      P = [p, delta Jp].
+
+Then P is a real signed permutation and has the same determinant as U.
+The matrix P^T U is a real rotation with both diagonal entries equal to m.
+Therefore
+
+    (P-U)* (P-U) = 2I - P^T U - U^T P = 2(1-m) I.
+
+This proves (1), including the endpoints m=1 and m=1/sqrt(2). The latter
+endpoint gives the worst-case statement because m>=1/sqrt(2).
+
+## Arbitrarily many exactly restored dirty helpers do not help
+
+Allow any finite h and any finite circuit of exactly unitary linear gates
+over D on two active coordinates and h additional complex coordinates.
+Every helper input is arbitrary and independent. Require the completed
+linear map W to return every helper exactly to its initial value for every
+input. There is no measurement, postselection, data-dependent control or
+unobserved output outside this declared space.
+
+Closure under multiplication gives W in U_(2+h)(D). Exact helper return
+gives the block form
+
+    W = [[A,B],[0,I_h]].
+
+The bottom-right block of W*W is B*B+I_h, so unitarity forces B*B=0
+and hence B=0. The top-left block gives A*A=I_2. Thus W=A direct-sum I_h
+with A in U_2(D), and (1) applies without change. Its attaining P can simply
+leave all helpers untouched. This is an all-size block-matrix argument;
+the finite one-helper checks only corroborate it.
+
+## Consequence for the rational-unitary FFT interface
+
+Jose Manuel's PR4205 uses exactly unitary rational coefficient gates with
+stored adjoint inverses. PROOF.md sections 2 and 3 specify rational phases
+and butterflies [[a,bw],[b,-aw]], with a^2+b^2=|w|^2=1. Its dyadic data
+rounding is a separate operation. Taking w=1 yields the real family covered
+by (1). This is a self-posed denominator-elimination question about that
+boundary, not a defect in the predecessor's rational construction.
+
+For the explicit rational member of this algebraic family
+
+    U = [[3/5,4/5],[4/5,-3/5]],
+
+the optimum squared operator error is exactly 2/5. For any unit-scale real
+butterfly with m<=4/5, the same model cannot meet error below sqrt(2/5),
+regardless of the precision parameter, circuit length or count of exactly
+restored helpers. At input radius R the corresponding worst-case absolute
+error is R sqrt(2(1-m)). The operator-norm extremizer proves that statement;
+it is not an assertion about every input.
+
+Rational butterflies approaching a balanced Hadamard gate have optimum
+squared error approaching 2-sqrt(2), rather than zero. Hence exact
+Gaussian-dyadic unitarity at this restored two-coordinate boundary cannot
+replace the rational coefficient approximation as its requested error
+tends to zero.
+
+Removing exact unitarity changes the question. For example the dyadic real
+rotation-shaped matrix (5I+6J)/8 has norm square 61/64, while its squared
+operator distance to (3I+4J)/5 is only 1/320. Nonunitary dyadic lifting or
+rounded gates need their own stability and restoration budget. Joint gates
+with additional non-restored active coordinates, global cancellation among
+changed gates, Gaussian natives on large address spaces and other endpoint
+contracts are outside this obstruction. No physical cost, recursive saving,
+supplier admission or selected framework assumption is proved here.
+
+## Classical credit and proof status
+
+Alexis De Vos, Raphael Van Laer and Steven Vandenbrande,
+[The Group of Dyadic Unitary Matrices, 2012, section 5](https://backoffice.biblio.ugent.be/download/2069554/2069555),
+already describe the finite group U_2(D) of order 96. This package supplies
+an elementary proof of the unit-vector fact needed for the approximation
+formula. The new contribution claimed here is (1), its sharp gate-interface
+consequence and the exact-restored-helper extension, in this repository's
+arithmetic setting. No worldwide literature priority is claimed.
+
+The all-real and arbitrary-helper quantifiers rest on this written proof.
+The exact finite checker is corroboration and checks of the formula's
+implementation. Independent human and formal proof-kernel review are
+unclaimed.

research/dyadic-two-wire-approximation/README.md

@@ -0,0 +1,135 @@
+# Sharp exact-dyadic approximation floor for two-wire butterflies
+
+This contribution was produced by Nick Petalas. New material is Apache-2.0.
+Claim type: scoped written mathematical proof with exact finite corroboration.
+No new kappa or supplier admission is claimed.
+
+For every real 2 by 2 orthogonal matrix U, let m=max |U_ij|. The exact best
+Gaussian-dyadic unitary approximation satisfies
+
+    min_{V in U_2(Z[i,1/2])} ||V-U||_op^2 = 2(1-m).
+
+A real signed permutation attains it. Any finite number of arbitrary dirty
+helpers, returned exactly for every input, leaves this minimum unchanged.
+The worst floor over real orthogonal targets is 2-sqrt(2), at a balanced
+butterfly. The rational butterfly [[3/5,4/5],[4/5,-3/5]] already has sharp
+squared error 2/5, regardless of requested precision or circuit length.
+[PROOF.md](PROOF.md) supplies the all-real and arbitrary-helper arguments.
+
+## The changed arithmetic interface
+
+Jose Manuel's [PR4205](https://github.com/CrocSwap/integer-mult-bounds/pull/4205),
+retained head `78c72e563173f3822fcb4efed9ceeccf05630258`, supplies exactly
+unitary rational FFT coefficient gates and stored adjoint inverses. Its
+real-phase butterfly family is the motivation for a self-posed question:
+can exact Gaussian-dyadic unitaries remove those rational denominators at
+the same restored two-coordinate boundary? The formula excludes an
+arbitrarily accurate replacement of a nontrivial real butterfly in that
+model. The predecessor's rational construction is a cited premise, not an
+audit target, and is unchanged.
+
+This is an arithmetic-interface side result under a changed
+`joint-query-controller` card. It does not give a complete supplier invoice
+or resolve the selected compiler/precision obligations. Nonunitary lifting,
+rounded arithmetic and larger active joint boundaries remain possible.
+The nonunitary dyadic matrix (5I+6J)/8, J=[[0,-1],[1,0]], is at squared
+distance only 1/320 from (3I+4J)/5, but has norm square 61/64. Thus exact
+unitarity is a substantive premise.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/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
+```
+
+Any CPython 3.12 path can replace the absolute interpreter path. Direct
+replay prints `PASS_DYADIC_TWO_WIRE_APPROXIMATION` in a JSON receipt whose
+hashes bind all six package files and the complete mathematical transcript.
+It writes no files and imports no predecessor implementation. Both
+warning-strict normal and optimized commands are registered in VERIFY.json.
+
+The checker independently joins all possible first and second columns and
+compares that join with the perpendicular-column construction. It then
+compares every resulting unitary with every declared rational rotation and
+reflection using exact integer Hermitian principal minors. There are no
+floating-point eigenvalues. The target family uses p=-12..12, q=1..12 in
+the rational circle parametrization, with repetitions removed, plus the
+missing limiting point. The resulting 368 targets give 35,328 exact
+target/unitary comparisons. The emitted receipt also reports the control
+counts and a hash of the full sorted transcript.
+
+One-helper controls exhaust the 96 unitary active blocks paired with each
+of 24 nonzero possible unit-vector leakage columns. Every such leakage
+fails exact unitarity, while each direct-sum identity helper passes. Six
+other rejection controls cover a changed sharp threshold in both
+directions, an empty candidate list, a nonpositive denominator, a
+rectangular matrix and a nonunitary imaginary perturbation. The closer
+nonunitary dyadic control verifies the importance of the hypothesis.
+
+## Scope and credit
+
+The finite group of 96 two-dimensional Gaussian-dyadic unitaries is
+classical. Credit Alexis De Vos, Raphael Van Laer and Steven Vandenbrande,
+[The Group of Dyadic Unitary Matrices, 2012, section 5](https://backoffice.biblio.ugent.be/download/2069554/2069555).
+The new claim is the sharp distance formula and its restored-helper
+interface consequence, with no worldwide literature-priority claim.
+
+Credit Jose Manuel / jmbarrancoml for PR4205's rational-unitary child;
+Vlado Vojdanovski for the retained FFT and Toeplitz schedules; Chafik
+Boukhalfa for rational unit-phase construction; Mason Hale for the retained
+interval arithmetic; Jeremy Kothe / IdeaOuter and Cinna Davis for the
+credited Gaussian/caller lineage. Predecessor files and credit are unchanged.
+MatShep's PR5549 studies tensor faithfulness of the same 96-element group;
+this package does not repeat its tensor-rank result or scientific replay.
+
+The scientific base is canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, selected
+PR6030. SOURCES.json pins the motivating source documents as provenance.
+No source scientific checker is run. Live open/account PRs, active
+Discussions, local reservations and main/merged searches for the object,
+general dyadic-unitary form and formula preceded the
+[advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19373396).
+The overlap helper was also run; its coverage and freshness are recorded
+in the PR body. Sparse notes and bounded searches do not establish absence
+of unpublished overlap. The selected result and all five framework assumptions remain.
+
+This excludes only a linear, exactly unitary, Gaussian-dyadic replacement
+at a restored two-active-coordinate boundary. It excludes no global FFT
+approximation, large native operator, nonunitary lifting method or changed
+helper-return contract. Exact coefficient unitarity and rounded data
+restoration are separate claims. Physical coefficient delivery, tapes,
+precision, stock, compilation and complete multiplication remain unproved.
+Selected cold replay, Lean, Docker, independent human and formal
+proof-kernel review are unrun or unclaimed.
+
+## Open next questions
+
+Can a nonunitary dyadic lifting replacement of one rational butterfly meet
+its full composed error/restoration budget with a cheaper complete
+coefficient-delivery bill? 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. This result does not reserve that follow-up.
+The structured question is in TASK.json.
+
+## Implementation bounds
+
+The fixed checker uses no recursion, external process, network access,
+dynamic import or mutable global state. The target generator has at most
+602 outputs; each has exactly 96 candidates. Matrix dimensions are at most
+three. Integer target denominators are at most 288. The transcript has at
+most 602 records. Package hashing reads six files, each capped at 1 MB.
+Every function is shorter than 60 lines and executable contracts remain
+enabled under optimized Python.
+
+Power of Ten rule 3 has a managed-runtime deviation: Python integers,
+tuples, sets and JSON allocate during execution inside the fixed finite
+bounds above. Interpreter/library allocation is not statically controlled
+or measured. Rule 9's rejection-test helper dispatches only to the two
+named local check functions; its finite targets and call sites are explicit.
+Warning-strict normal/optimized replay is the Python diagnostic check.

research/dyadic-two-wire-approximation/SOURCES.json

@@ -0,0 +1,41 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/rational-unitary-fft/README.md",
+      "usage": "provenance",
+      "git_blob": "33000ee73067f27e87a04953ed0ba3e356d96bc6",
+      "sha256": "b334df2d512f971626aa69a2b94dab4e51acee19bc0f9f6ee42ea709636b8d9f"
+    },
+    {
+      "path": "research/rational-unitary-fft/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "99a55596f67ae3b94ef02ebb159b313f33bf22af",
+      "sha256": "50e31e33e1275a133d10e87208ceb50dddce67d0678d2a89de9f7ba28d8380d9"
+    }
+  ],
+  "external_reference": {
+    "url": "https://backoffice.biblio.ugent.be/download/2069554/2069555",
+    "title": "The Group of Dyadic Unitary Matrices",
+    "authors": [
+      "Alexis De Vos",
+      "Raphael Van Laer",
+      "Steven Vandenbrande"
+    ],
+    "year": 2012,
+    "usage": "Classical credit only; no fetched bytes or external theorem are required by the self-contained proof/checker."
+  }
+}