From 895e3db4982ad4bba6af3fbfbc6caf7b5f97ae1f Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 14:55:48 +0100 Subject: [PATCH] feat(research): prove sharp commuting repair for qubit triples --- research/qubit-commuting-repair/README.md | 195 ++++++++++++++++ research/qubit-commuting-repair/SOURCES.json | 24 ++ research/qubit-commuting-repair/TASK.json | 109 +++++++++ research/qubit-commuting-repair/VERIFY.json | 34 +++ research/qubit-commuting-repair/verify.py | 224 +++++++++++++++++++ 5 files changed, 586 insertions(+) create mode 100644 research/qubit-commuting-repair/README.md create mode 100644 research/qubit-commuting-repair/SOURCES.json create mode 100644 research/qubit-commuting-repair/TASK.json create mode 100644 research/qubit-commuting-repair/VERIFY.json create mode 100644 research/qubit-commuting-repair/verify.py diff --git a/research/qubit-commuting-repair/README.md b/research/qubit-commuting-repair/README.md new file mode 100644 index 0000000000..bd4fd321ff --- /dev/null +++ b/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= 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_(i0. +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), 01/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. diff --git a/research/qubit-commuting-repair/SOURCES.json b/research/qubit-commuting-repair/SOURCES.json new file mode 100644 index 0000000000..821685421e --- /dev/null +++ b/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" + } + ] +} diff --git a/research/qubit-commuting-repair/TASK.json b/research/qubit-commuting-repair/TASK.json new file mode 100644 index 0000000000..fefcbd1041 --- /dev/null +++ b/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." + } +} diff --git a/research/qubit-commuting-repair/VERIFY.json b/research/qubit-commuting-repair/VERIFY.json new file mode 100644 index 0000000000..bcb5cbcb5f --- /dev/null +++ b/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." + } + ] +} diff --git a/research/qubit-commuting-repair/verify.py b/research/qubit-commuting-repair/verify.py new file mode 100644 index 0000000000..9b580006da --- /dev/null +++ b/research/qubit-commuting-repair/verify.py @@ -0,0 +1,224 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the written qubit repair theorem; no output files.""" +from dataclasses import dataclass, replace +from fractions import Fraction as F +from hashlib import sha256 +from itertools import combinations, combinations_with_replacement, product +import json +from pathlib import Path +import sys + + +Vector = tuple[F, F, F] +Matrix = tuple[tuple[F, ...], ...] +AXES = ((F(1), F(0), F(0)), (F(0), F(1), F(0)), (F(0), F(0), F(1))) +PAULI = ( + ((0, 1, 0, 0), (1, 0, 0, 0), (0, 0, 0, 1), (0, 0, 1, 0)), + ((0, 0, 0, 1), (0, 0, -1, 0), (0, -1, 0, 0), (1, 0, 0, 0)), + ((1, 0, 0, 0), (0, -1, 0, 0), (0, 0, 1, 0), (0, 0, 0, -1)), +) + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b, strict=True)) + + +def transpose(a: Matrix) -> Matrix: + return tuple(zip(*a, strict=True)) + + +def multiply(a: Matrix, b: Matrix) -> Matrix: + columns = transpose(b) + return tuple(tuple(dot(row, col) for col in columns) for row in a) + + +def subtract(a: Matrix, b: Matrix) -> Matrix: + return tuple(tuple(x - y for x, y in zip(r, s, strict=True)) + for r, s in zip(a, b, strict=True)) + + +def observable(v: Vector, scalar: F) -> Matrix: + # Realification R(A) = [[Re A, -Im A], [Im A, Re A]]. + return tuple(tuple(scalar * (r == c) + sum(v[k] * PAULI[k][r][c] + for k in range(3)) for c in range(4)) for r in range(4)) + + +def norm2(a: Matrix) -> F: + # ||A||_(2,2)^2 = ||R(A)||_F^2 / 4, for arbitrary complex A. + return sum(x * x for row in a for x in row) / 4 + + +def cross2(a, b): + return sum((a[i] * b[j] - a[j] * b[i]) ** 2 + for i, j in combinations(range(3), 2)) + + +def covariance(vectors) -> Matrix: + return tuple(tuple(sum(v[i] * v[j] for v in vectors) + for j in range(3)) for i in range(3)) + + +def identity(n: int) -> Matrix: + return tuple(tuple(F(i == j) for j in range(n)) for i in range(n)) + + +@dataclass(frozen=True) +class Witness: + vectors: tuple[Vector, Vector, Vector] + scalars: Vector + frame: tuple[Vector, Vector, Vector] + eigenvalues: Vector + repaired: tuple[Vector, Vector, Vector] + repaired_scalars: Vector + error2: F + delta2: F + + +def witness(vectors, scalars, frame, eigenvalues) -> Witness: + direction = frame[0] + repaired = tuple(tuple(dot(v, direction) * x for x in direction) for v in vectors) + return Witness(vectors, scalars, frame, eigenvalues, repaired, scalars, + sum(eigenvalues[1:]), 4 * sum(cross2(a, b) + for a, b in combinations(vectors, 2))) + + +def validate(case: Witness) -> None: + require(all(len(v) == 3 for v in (*case.vectors, *case.frame, *case.repaired)), + 'vector dimensions') + require(multiply(case.frame, transpose(case.frame)) == identity(3), 'frame') + l1, l2, l3 = case.eigenvalues + require(l1 >= l2 >= l3 >= 0, 'eigenvalue order') + s = covariance(case.vectors) + for n, eigenvalue in zip(case.frame, case.eigenvalues, strict=True): + require(tuple(dot(row, n) for row in s) == tuple(eigenvalue * x for x in n), + 'spectral certificate') + for v, a in zip(case.vectors, case.scalars, strict=True): + require(abs(a) <= 1 and dot(v, v) <= (1 - abs(a)) ** 2, 'input contraction') + for v, a in zip(case.repaired, case.repaired_scalars, strict=True): + require(abs(a) <= 1 and dot(v, v) <= (1 - abs(a)) ** 2, 'output contraction') + original = tuple(observable(v, a) for v, a in zip(case.vectors, case.scalars, strict=True)) + repaired = tuple(observable(v, a) for v, a in zip(case.repaired, case.repaired_scalars, strict=True)) + for a, b in combinations(repaired, 2): + require(multiply(a, b) == multiply(b, a), 'commuting repair') + error2 = sum(norm2(subtract(a, b)) for a, b in zip(original, repaired, strict=True)) + delta2 = sum(norm2(subtract(multiply(a, b), multiply(b, a))) + for a, b in combinations(original, 2)) + require(case.error2 == error2 == l2 + l3, 'optimal distance') + require(case.delta2 == delta2 == 4 * (l1*l2 + l1*l3 + l2*l3), 'commutator norm') + require(3 * error2 ** 2 <= delta2, 'sharp bound') + require(delta2 - 3 * error2 ** 2 == + 4 * (l1-l2) * (l2+l3) + (l2-l3) * (l2+3*l3), 'gap identity') + require((3 * error2 ** 2 == delta2) == (l2 == l3 == 0 or l1 == l2 == l3), + 'equality classification') + + +def check_grid() -> dict: + raw = tuple(product((-1, 0, 1), repeat=3)) + vectors = tuple(tuple(F(x, 4) for x in v) for v in raw) + pair_checks = 0 + for a, b in product(vectors, repeat=2): + left, right = observable(a, F(1, 4)), observable(b, F(-1, 4)) + commutator = subtract(multiply(left, right), multiply(right, left)) + require(norm2(commutator) == 4 * cross2(a, b), 'literal pair norm') + require((commutator == tuple((F(0),)*4 for _ in range(4))) == + (cross2(a, b) == 0), 'literal pair commutation') + pair_checks += 1 + triple_checks = 0 + for indices in product(range(27), repeat=3): + vs = tuple(raw[i] for i in indices) + s = covariance(vs) + trace = sum(s[i][i] for i in range(3)) + trace_square = sum(s[i][j] ** 2 for i in range(3) for j in range(3)) + require(trace ** 2 - trace_square == + 2 * sum(cross2(a, b) for a, b in combinations(vs, 2)), 'Gram identity') + triple_checks += 1 + return {'literal_matrix_pairs': pair_checks, 'covariance_triples': triple_checks} + + +def frames(): + rotation = ((F(3, 5), F(-4, 5), F(0)), + (F(4, 5), F(3, 5), F(0)), AXES[2]) + permutation = (AXES[1], AXES[2], AXES[0]) + return (AXES, rotation, permutation, multiply(rotation, permutation), + multiply(permutation, rotation)) + + +def check_spectra() -> tuple[dict, Witness]: + count = 0 + equality = 0 + first = None + for radii in combinations_with_replacement((F(0), F(1, 8), F(1, 4), F(3, 8)), 3): + radii = tuple(reversed(radii)) + eig = tuple(x*x for x in radii) + for q, r in product(frames(), repeat=2): + # V = R diag(radii) Q, hence V^T V = Q^T diag(eig) Q. + vectors = multiply(tuple(tuple(r[i][j] * radii[j] for j in range(3)) + for i in range(3)), q) + for scalars in ((F(0),)*3, (F(-1, 4), F(0), F(1, 4))): + case = witness(vectors, scalars, q, eig) + validate(case) + count += 1 + equality += int(case.delta2 > 0 and 3 * case.error2 ** 2 == case.delta2) + if eig[0] > eig[1] > eig[2] > 0: + first = case + require(first is not None, 'strict-spectrum fixture exists') + return {'spectral_repairs': count, 'noncommuting_equality_fixtures': equality}, first + + +def check_controls(case: Witness) -> int: + bad = ( + replace(case, eigenvalues=tuple(reversed(case.eigenvalues))), + replace(case, frame=(case.frame[1], case.frame[0], case.frame[2])), + replace(case, frame=(AXES[0], AXES[0], AXES[2])), + replace(case, error2=case.error2 + 1), + replace(case, delta2=case.delta2 / 2), + replace(case, repaired=case.vectors), + replace(case, scalars=(F(2), F(0), F(0))), + replace(case, repaired_scalars=(F(2), F(0), F(0))), + replace(case, repaired_scalars=tuple(a + F(1, 8) for a in case.scalars)), + replace(case, repaired=tuple((F(0),)*3 for _ in range(3))), + ) + for mutant in bad: + try: + validate(mutant) + except ValueError: + continue + raise ValueError('a rejection control passed') + # The tempting stronger constant 1/sqrt(2) fails on the Pauli triple. + require(F(2) ** 2 > F(12, 4), 'false stronger constant rejects') + return len(bad) + 1 + + +def main() -> None: + require(len(sys.argv) == 1, 'no command-line arguments accepted') + counts = check_grid() + spectra, case = check_spectra() + counts.update(spectra) + counts['rejection_controls'] = check_controls(case) + sharp = witness(AXES, (F(0),)*3, AXES, (F(1),)*3) + validate(sharp) + require((sharp.error2, sharp.delta2) == (F(2), F(12)), 'Pauli attainer') + counts['scaled_pauli_attainers'] = 0 + for denominator in range(1, 33): + t = F(1, denominator) + scaled = tuple(tuple(t * x for x in axis) for axis in AXES) + sample = witness(scaled, (F(0),)*3, AXES, (t*t,)*3) + validate(sample) + require(sample.error2 ** 2 / sample.delta2 == F(1, 3), 'scale invariant ratio') + counts['scaled_pauli_attainers'] += 1 + package = Path(__file__).resolve().parent + names = ('README.md', 'TASK.json', 'SOURCES.json', 'VERIFY.json', 'verify.py') + hashes = {name: sha256((package / name).read_bytes()).hexdigest() for name in names} + print(json.dumps({'status': 'PASS_QUBIT_COMMUTING_REPAIR', 'counts': counts, + 'sharp_constant_fourth_power': '1/3', 'package_sha256': hashes, + 'scope': 'Finite exact corroboration of the written dimension-two proof.'}, + sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main()