Prove sharp commuting repair for Hermitian qubit triples (no new κ)

research/qubit-commuting-repair/README.md

@@ -0,0 +1,195 @@
+# Sharp commuting repair for a Hermitian qubit triple
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written mathematical proof with exact finite corroboration.
+It answers the dimension-two case of David Ganz's explicitly unproved
+[atlas B099](../pure-math-atlas-400/volumes/02-geometry.md#b099),
+[PR #2849](https://github.com/CrocSwap/integer-mult-bounds/pull/2849).
+The new result is an exact repair formula, every minimizer, and the sharp
+square-root constant for this case. Global literature priority and independent
+human and formal proof-kernel review are unclaimed.
+
+## Result
+
+Let A_1,A_2,A_3 be arbitrary two-by-two Hermitian contractions. Use the atlas
+normalization ||M||_(2,2)^2 = Tr(M* M)/2, and put
+
+$$
+\delta^2=\sum_{i<j}\|[A_i,A_j]\|_{2,2}^2,\qquad
+E^2=\min_{\substack{B_i=B_i^*,\ \|B_i\|\le1\\[B_i,B_j]=0}}
+           \sum_{i=1}^3\|A_i-B_i\|_{2,2}^2.
+$$
+
+Write A_i = a_i I + v_i dot sigma, with a_i real, v_i in R^3 and
+sigma = (X,Y,Z) the usual Pauli matrices. Let
+S = sum_i v_i v_i^T have eigenvalues lambda_1 >= lambda_2 >= lambda_3 >= 0.
+Then
+
+$$
+E^2=\lambda_2+\lambda_3,\qquad
+\delta^2=4(\lambda_1\lambda_2+\lambda_1\lambda_3+\lambda_2\lambda_3),
+\qquad E\le 3^{-1/4}\sqrt\delta.
+$$
+
+Every minimizing triple is
+
+$$
+B_i=a_i I+(v_i\cdot n)(n\cdot\sigma),
+$$
+
+where n is a unit vector in the top eigenspace of S. The formulas include
+S=0. For a noncommuting triple equality in the bound holds exactly when
+S=r^2 I for some r>0, equivalently when the three v_i are mutually orthogonal
+and have equal length r. The constant 3^(-1/4) is best possible even for
+arbitrarily small positive delta. No exponent greater than one-half can
+replace one-half with a constant uniform over these qubit triples near delta=0.
+
+## Proof
+
+The Pauli matrices are orthonormal for normalized Hilbert-Schmidt inner product.
+Their multiplication identity gives
+
+$$
+\|aI+v\cdot\sigma\|_{2,2}^2=a^2+|v|^2,\qquad
+[v\cdot\sigma,w\cdot\sigma]=2i(v\times w)\cdot\sigma.
+$$
+
+The eigenvalues of A_i are a_i +/- |v_i|. Thus the contraction condition is
+|a_i|+|v_i| <= 1, and two Hermitian qubit matrices commute exactly when their
+Pauli vectors are collinear. This elementary representation is classical.
+
+Any commuting Hermitian triple has the form b_i I + t_i n dot sigma for one
+unit vector n. The all-scalar case allows any n. Orthogonal projection gives
+
+$$
+\sum_i\|A_i-B_i\|_{2,2}^2
+=\sum_i(a_i-b_i)^2+\sum_i|v_i-t_i n|^2
+\ge\operatorname{tr}S-n^TSn
+\ge\operatorname{tr}S-\lambda_1.
+$$
+
+For any top unit eigenvector n, choose b_i=a_i and t_i=v_i dot n. Both
+inequalities are then equalities. These choices are contractions because
+|a_i|+|v_i dot n| <= |a_i|+|v_i| <= 1. This proves the exact minimum without
+relaxing the feasible contraction set. Conversely, equality in the displayed
+sum forces b_i=a_i and t_i=v_i dot n. Equality in the Rayleigh bound forces n
+to belong to the top eigenspace. This proves the minimizer classification.
+The rank-one approximation step is classical; the contribution applies it to
+the precise atlas repair contract and determines the sharp constant below.
+
+The cross-product identity yields delta^2 = 4 sum_(i<j) |v_i cross v_j|^2.
+Expanding the trace of S^2 shows that twice this latter sum is
+(tr S)^2 - tr(S^2), so the claimed eigenvalue formula follows. Finally,
+
+$$
+\begin{aligned}
+\delta^2-3E^4
+&=4(\lambda_1-\lambda_2)(\lambda_2+\lambda_3)
+ +(\lambda_2-\lambda_3)(\lambda_2+3\lambda_3)\ge0.
+\end{aligned}
+$$
+
+All factors are nonnegative. If the triple does not commute, lambda_2>0.
+Both terms vanish exactly when lambda_1=lambda_2=lambda_3. If lambda_2=0,
+all vectors are collinear and E=delta=0. With three vectors, positive
+S=r^2 I also implies V V^T=r^2 I for the matrix V with rows v_i, proving
+the stated orthogonality characterization.
+
+For sharpness take (A_1,A_2,A_3)=(rX,rY,rZ), 0<r<=1. The matrices are
+contractions, E^2=2r^2 and delta^2=12r^4. Hence E^4/delta^2=1/3 at every r.
+For any alpha>1/2 the ratio E/delta^alpha is a positive constant times
+r^(1-2alpha), which tends to infinity as r decreases to zero. This proves
+both sharpness claims. It completes the written proof; finite checks below
+corroborate its identities rather than establish its real universal quantifiers.
+
+## Evidence and reproduction
+
+From the repository root, use CPython 3.12 and only the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -Werror -B research/qubit-commuting-repair/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -Werror -B research/qubit-commuting-repair/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/qubit-commuting-repair
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/qubit-commuting-repair --check-source-history
+```
+
+The interpreter path is specific to the contribution environment. Elsewhere
+substitute a CPython 3.12 executable. The standalone verifier emits
+PASS_QUBIT_COMMUTING_REPAIR and a receipt bound to the five package-file hashes.
+It writes no files. No receipt is hand-written or committed.
+
+The checker uses exact rational realifications of literal complex matrices.
+It checks 729 ordered matrix pairs, all 19,683 triples of integer vectors in
+{-1,0,1}^3 for the covariance identity, and 1,000 explicit spectral repairs.
+The latter include zero, rank-one, rank-two, repeated-eigenvalue and distinct
+positive spectra, noncoordinate rational frames, and nonzero scalar parts.
+The two-by-two observable pair fixtures scale the integer vectors by 1/4.
+There are 150 noncommuting equality fixtures among the spectral repairs.
+It also checks 32 scaled Pauli attainers and eleven rejection controls.
+The controls reject invalid contractions, wrong eigendirections, wrong norms,
+noncommuting repairs, shifted scalar parts, suboptimal scalar repairs and a
+false stronger constant. These are finite counts, not a census of all inputs.
+
+## Scope and sources
+
+B099's all-dimension universal constant is still unresolved here. This is a
+fixed-dimensional side result. It does not give a paid native decoder, an
+integer-multiplication supplier, new kappa or a selected-frontier change.
+Physical routing, dirty restoration, compiler, stock, precision/tape and the
+complete supplier bill remain outside scope. No selected cold replay, Lean
+build, Docker replay or predecessor scientific suite was run.
+
+Credit David Ganz for atlas B099, its exact normalization and the simultaneous
+repair question. Classical Pauli coordinates and best rank-one approximation
+retain their standard credit. Islam Faisal, Anand Natarajan and Alexander
+Poremba's [qubit rounding work](https://arxiv.org/abs/2605.26096), sections 3.1
+and 3.2, supplies related pinching and scalar-rounding context. It is not used
+as a proof premise or claimed as this result. Their two-local Hamiltonian
+problem and operator-norm bill differ from the exact normalized-HS triple
+minimum computed here. Lev Glebsky's [normalized-HS work](https://arxiv.org/abs/1002.3082)
+is background on dimension-uniform qualitative repair. No claim that this
+short qubit calculation is new to the literature is made.
+
+The base, selected record, original card and exact atlas bytes are recorded in
+SOURCES.json and TASK.json. Existing source and contributor credit are unchanged.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19147024)
+records the bounded target and overlap coverage. Search coverage includes live
+open/account PRs, active Discussions, latest handoffs, targeted main-package
+and merged-PR searches, and the cached card scan. It excludes unpublished work
+and a complete historical code-diff or literature audit.
+
+## Implementation bounds
+
+The verifier has no recursion, network, subprocesses or external dependencies.
+All loops run over the fixed grids above, matrices have dimensions at most four,
+and no function exceeds 60 lines. Explicit require checks remain active under
+optimized Python. Warnings are errors in both registered commands. The package
+runner checks the declared source hash; the standalone theorem checker imports
+no predecessor executable.
+
+Power-of-ten rule 3 has a bounded managed-runtime deviation in verify.py.
+CPython integers, Fractions and tuples allocate during checking, so fixed
+allocation after initialization cannot be met. At most one triple and its
+matrices are processed at a time; grids hold 27 vectors and five frames, and
+integer/rational inputs and all iteration counts are fixed in the source.
+No candidate history accumulates. The normal and optimized full replays verify
+these bounded paths. Revisit this choice if externally supplied dimensions or
+grids are added. The standard-library dataclass only defines the eight-field
+immutable witness record; all verification branches and calls remain explicit.
+No external static analyzer was installed. Warning-strict execution and AST
+syntax/function-size inspection passed; the longest function has 28 lines.
+
+## Open next questions
+
+1. Does this sharp constant extend to triples with a known common invariant
+   decomposition into blocks of dimension at most two? Such a result would
+   give a dimension-uniform structured case of B099. Start by combining the
+   proved qubit repairs with the normalized-HS block weights. A proof must
+   account for global normalization and distinguish a constructive upper bound
+   from the globally optimal repair, which could mix blocks.
+2. What bound holds for general three-by-three Hermitian contractions? This
+   is the next fixed dimension beyond the Pauli collinearity argument. Start
+   with a specific spectral clustering rule and the complete summed repair
+   error. The current exact reduction relies on dimension two and does not
+   supply a qutrit formula.

research/qubit-commuting-repair/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/pure-math-atlas-400/volumes/02-geometry.md",
+      "usage": "input",
+      "git_blob": "baef1e69c08c7cbd4dfd020862870fa5161afc86",
+      "sha256": "39fc97bdfa29337b79d1308e35df41e867ce2102d44755fd407aa09ff8352b39"
+    }
+  ]
+}

research/qubit-commuting-repair/TASK.json

@@ -0,0 +1,109 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove the exact optimal simultaneous commuting repair of three Hermitian qubit contractions and the sharp square-root constant 3^(-1/4), resolving the dimension-two case of atlas B099.",
+  "scope_change_reason": "The formal-interface card is changed to an explicit quantitative operator repair question from another contributor. This is a fixed-dimensional mathematical side result, not a formal kernel proof or paid supplier interface.",
+  "bottleneck_link": "Side result: supplies a sharp normalized-Hilbert-Schmidt repair contract for the repository atlas. No supplier or multiplication-exponent improvement follows.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified dimension-two theorem; leave higher dimensions and structured-block extensions as open questions.",
+  "outcome": "completed",
+  "evidence": "Written Pauli-covariance proof with exact rational literal matrix and spectral repair checks, scaled sharp attainers and rejection controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Extend the qubit bound to a known common invariant decomposition into blocks of dimension at most two.",
+      "why_it_matters": "Would give a dimension-uniform structured case of B099.",
+      "first_step": "Combine block repairs with exact normalized-HS weights.",
+      "blocked_by": "Global normalization and possible block-mixing optimizers need separate analysis."
+    },
+    {
+      "question": "Find a square-root repair bound for general three-by-three Hermitian contractions.",
+      "why_it_matters": "The next fixed dimension tests which parts survive beyond Pauli collinearity.",
+      "first_step": "Analyze a named spectral clustering rule and its complete summed error.",
+      "blocked_by": "The dimension-two covariance formula does not extend directly."
+    }
+  ],
+  "environment": {
+    "python": "3.12.15",
+    "platform": "macOS-27.0.1-arm64-arm-64bit"
+  },
+  "overlap": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19147024",
+    "coverage": "Live open/account PR lists, latest handoffs, active Discussions, targeted main-tree and merged searches, atlas predecessor and related PR bodies. Completed cache covers 310 open PRs and 4,482 Discussion records; sparse local search covers 153 notes and leaves 6,940 HEAD notes unsearched. Distinctive README search used the full origin/main tree. Unpublished work and complete historical code/literature coverage excluded."
+  }
+}

research/qubit-commuting-repair/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/pure-math-atlas-400/volumes/02-geometry.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-Werror",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "Exact literal qubit identities, covariance triples, optimal spectral repairs, equality attainers, rejection controls and hash-bound stdout receipt."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-Werror",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "All checks and rejection controls remain active with optimization."
+    }
+  ]
+}