diff --git a/research/clifford-threshold-linear-lower/PROOF.md b/research/clifford-threshold-linear-lower/PROOF.md new file mode 100644 index 0000000000..bfc3886dfa --- /dev/null +++ b/research/clifford-threshold-linear-lower/PROOF.md @@ -0,0 +1,142 @@ +# The full Clifford tensor threshold is at least 2n+1 + +## Statement + +Let G_n be the group of n-qubit unitary Clifford matrices with entries in +Z[i,1/2]. Its scalars are the four units i^k. For one representative U_a of +each projective class and positive width f, put + + H_f(a,b) = (tr(U_a^* U_b) / 2^n)^f, + +the Gram matrix of the unit vectors U_a^{tensor f}/2^{nf}. Let T(n) be the least +width from which H_f is nonsingular at every larger width. (By the Schur +product step of MatShep's #5675, Section 4, nonsingularity at f persists to +f+1, so T(n) is also the least nonsingular width.) + +**Theorem.** For every n >= 2 and every width 1 <= f <= 2n, H_f is singular. +Hence + + 2n + 1 <= T(n) <= 4n + 4. + +The upper bound is Ali Romman's pointwise theorem (#5526). The lower bound is +new. It is sharp for neither n=2 (T=9, #5675) nor, presumably, larger n; it +proves that T(n) grows linearly, and it gives 7 <= T(3) <= 16. + +Two refinements follow from cited code lemmas without new work: for n = 1 +modulo four, n >= 5, H_f is singular through f = 2n+2 (#5635, Section 2), so +T(n) >= 2n+3; for n = 2 modulo four, through f = 2n+1 (#5902), so T(n) >= 2n+2. + +## 1. A monomial subgroup and a principal submatrix + +Let M_n be the input-phase monomial group of Ali Romman's native grammar +(#5369, #5529): + + U(g,q) e_x = i^{q(x)} e_{g(x)}, + q(x) = c + sum_j a_j x_j + 2 sum_{j= 2, let Psi be the sum of the +cuspidal characters chi_theta of GL(n,2) over Frobenius orbits of primitive +characters theta of F_{2^n}^*. By Green's theorem Psi is a genuine integer +character with Psi(1) > 0 and Psi(1) + (2^{n-1}-1) Psi(t) = 0 at a +transvection t. Every nonidentity element of the pointwise stabilizer H of a +hyperplane is a transvection, so the representation has no H-fixed vector and + + sum_{h in gH} Psi(h^{-1}) = 0 for every g. + +The element + + A_n = sum_{t in X} sum_{g in GL(n,2)} Psi(g^{-1}) [x -> g x + t] + +therefore satisfies rho_f(A_n) e_tuple = 0 for every f-tuple of points of X +whose affine span is proper (#5635, Section 3, eq. (2)). + +*Phase projector.* With D the diagonal subgroup and + + E_r = (1/|D|) sum_{c,a,b} i^{-r c} [D_q], P_r = A_n E_r, + +rho_f(E_r) is the projector onto tuples with zero nonconstant phase character +when f = r (mod 4), and is zero otherwise (#5635, Section 4). A tuple +x_1..x_f has zero nonconstant phase character exactly when + + sum_t x_tj = 0 (mod 4), sum_t x_tj x_tk = 0 (mod 2) for j < k. + +*Code step, every n.* Let x_1..x_f have zero phase and full affine span, with +f <= 2n. Append zero points to length N = 2n. This keeps both properties. +The n coordinate rows span a binary code C of length N. Every row weight is +divisible by four and distinct rows meet evenly, so C is self-orthogonal and, +by full linear span, has dimension n. Full affine span also means the all-one +word 1_N is not in C. Every word of C has even weight, so 1_N is orthogonal to +C, and 1_N . 1_N = N = 0 (mod 2). Thus C + <1_N> is self-orthogonal of +dimension n + 1 > N/2, which is impossible. Hence **no zero-phase tuple of +length at most 2n has full affine span**, and + + rho_f(P_r) = 0 for every f <= 2n with f = r (mod 4), + +and trivially at the other residues. + +*Nonzero residual.* The tuple of length 4n+1 consisting of the zero point and +four copies of each basis vector e_j has zero phase (each column sum is four, +each pair product is zero) and full affine span. Pad with zeros to the width +f* in {4n+1,...,4n+4} with f* = r (mod 4). Only the identity affine map fixes +every point of a full-span tuple, so the diagonal entry of rho_{f*}(P_r) at +this tuple is Psi(1) > 0. Thus P_r is not in the central ideal +I_r = (z - i^r) that every width of residue r annihilates. + +## 3. From the residual to a null vector of H_f + +Group the terms of P_r by projective class. If U = i^k U_a, then +U^{tensor f} = i^{kf} U_a^{tensor f}. For f = r (mod 4) this gives a class +vector v_r, depending only on r, with + + rho_f(P_r) = sum_a v_r(a) U_a^{tensor f}. + +The diagonal entry at width f* is a linear functional of v_r and is nonzero, +so v_r is nonzero. At a width f <= 2n of residue r, rho_f(P_r) = 0, so +sum_a v_r(a) U_a^{tensor f} = 0 and the monomial Gram annihilates v_r. By +Section 1, H_f is singular. This holds for every 1 <= f <= 2n, which proves +the theorem. + +## 4. Finite corroboration + +`verify.py` uses exact integer and Gaussian-integer arithmetic. It checks: + +- the code step exhaustively for n = 2, 3, 4: all 7, 34 and 458 zero-phase + multisets of size at most 2n lack full affine span; and the explicit + length-(4n+1) tuple for n = 2..64; +- the cuspidal coset identity on GL(2,2) and GL(3,2), at all 1,194 + (g, hyperplane) pairs, with the degree and transvection values; +- the two-qubit transfer literally. All 3,072 monomial matrices normalize the + two-qubit Pauli group and form 768 projective classes. For each f = 1..4, + the class vector of P_{f mod 4} is nonzero (full support, 768 classes) and + is annihilated by the exact class Gram matrix (tr(U_a^* U_b))^f. Its + diagonal entry at widths 9..12 is 128 = |D| Psi(1), as predicted; +- three rejection controls: the trivial character, the sign with its + order-three values negated, and one perturbed coefficient each leave a + nonzero entry of H_4 v. + +The two-qubit null vectors agree with MatShep's ranks at widths 1..4 in #5675 +(all below 11,520); that package was not rerun. + +## 5. Limits + +This is a scoped proof. Green's character theorem enters through #5635 and +is cited, not proof-kernel checked; the finite checks at n = 2, 3 corroborate +it. The theorem does not decide T(3); in particular it neither proves nor +refutes T(3) = 13. It says nothing about the spectral constants of #5594 or +#5675, or about any physical caller, invoice or κ. diff --git a/research/clifford-threshold-linear-lower/README.md b/research/clifford-threshold-linear-lower/README.md new file mode 100644 index 0000000000..5da48bc4ea --- /dev/null +++ b/research/clifford-threshold-linear-lower/README.md @@ -0,0 +1,105 @@ +# The full Clifford tensor threshold grows at least like 2n+1 + +For every n >= 2, the projective tensor Gram matrix of the full n-qubit +Gaussian-dyadic Clifford group is **singular at every width f <= 2n**. +Its pointwise tensor-independence threshold therefore satisfies + + 2n + 1 <= T(n) <= 4n + 4, + +where the upper bound is Ali Romman's +[PR #5526](https://github.com/CrocSwap/integer-mult-bounds/pull/5526). +In particular **7 <= T(3) <= 16**. Before this, the only exact values were +T(1)=5 (MatShep, #5549) and T(2)=9 (MatShep, +[#5675](https://github.com/CrocSwap/integer-mult-bounds/pull/5675)), and there +was no lower bound for general n. With cited code lemmas, T(n) >= 2n+3 for +n = 1 (mod 4), n >= 5 (#5635), and T(n) >= 2n+2 for n = 2 (mod 4) (#5902). + +This partially answers the Open next question of #5675 ("does 4n+1 continue +at three or more qubits?"). It proves linear growth and leaves the exact +three-qubit value open. It is a scoped proof with finite corroboration, not +a κ, supplier or selected-frontier change. + +## The argument + +[PROOF.md](PROOF.md) has the details. The Hadamard-free affine/quadratic +monomial native group of #5369/#5529 is a subgroup of the Clifford group with +the same scalars, so its Gram matrix is a principal submatrix of the Clifford +Gram, and any null vector of it is a null vector of the full Gram. Ali +Romman's cuspidal residual from +[PR #5635](https://github.com/CrocSwap/integer-mult-bounds/pull/5635), +projected to zero phase, is a fixed nonzero group-algebra element. A +self-orthogonal-code argument valid for every n shows that it vanishes at +every width f <= 2n. It is nonzero because an explicit full-span zero-phase +tuple of length 4n+1 sees it. + +The new parts are the principal-submatrix transfer from the monomial grammar +to the full Clifford Gram, and the all-n code step (#5635 states its code step +only for n = 1 mod 4). + +## Evidence and reproduction + +Use the repository CPython 3.12 interpreter from the worktree root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/research_package.py --package research/clifford-threshold-linear-lower +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/check_research_commit.py --package research/clifford-threshold-linear-lower --check-source-history +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/clifford-threshold-linear-lower/verify.py +``` + +On another machine, substitute any CPython 3.12. Only the standard library is +used. The direct verifier prints `PASS_CLIFFORD_THRESHOLD_LINEAR_LOWER` in +about three seconds, in normal and `-O` modes. It checks, exactly: + +- the code step exhaustively at n = 2, 3, 4 (7, 34 and 458 zero-phase + multisets of size at most 2n, none with full affine span), plus the explicit + length-(4n+1) full-span tuple for n = 2..64; +- the cuspidal coset identity on GL(2,2) and GL(3,2) at 1,194 + (g, hyperplane) pairs; +- at two qubits, literally: all 3,072 monomial matrices normalize the Pauli + group and form 768 projective classes. At each width f = 1..4 the residual's + class vector is nonzero and the exact class Gram (tr(U_a^* U_b))^f + annihilates it. The same residual has diagonal entry 128 at widths 9..12; +- three rejection controls (trivial character, sign with its order-three + values negated, one perturbed coefficient), each of which fails H_4 v = 0. + +No predecessor executable is run. The cited proofs are pinned in +[SOURCES.json](SOURCES.json). + +## Limits + +Green's character theorem enters through #5635's cuspidal lemma and is cited, +not proof-kernel checked; the n = 2, 3 coset checks only corroborate it. The +bound 2n+1 is not sharp at n = 2 (T = 9), and the theorem does not decide +T(3) = 13. Spectral constants, physical callers, invoices, compiler, +precision, tape, stock and κ are outside this result. Independent human and +formal proof-kernel review are unclaimed. All five framework assumptions keep +their status. + +The formal-interface card is explicitly narrowed to this written +native-interface side result (see [TASK.json](TASK.json)). Base main is +`19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8. +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19221825). +Overlap was checked against open PRs, Discussion claims, merged PR titles +(`cuspidal`, `axis cutoff`, Clifford threshold) and `research/*` README and +PROOF text on main. A search with no hit does not prove novelty. + +## Open next questions + +- **Exact T(3), now in [7,16].** This decides whether 4n+1 continues. First + step: compute the centre action of the three-qubit Clifford group on class + functions at widths 7..13, as #5675 did at two qubits. Blocker: the group has + order 4 x 92,897,280 and no class or character table is in the repository. +- **A full-group residual.** The residual here lives in the Hadamard-free + subgroup, whose own threshold is only about 2n+3. Raising the all-n bound + toward 4n+1 needs a null vector that uses Hadamard-type elements. First + step: find an all-n analogue of #5675's width-8 determinant witness. The + determinant itself is trivial for n >= 3. + +## Credit + +This contribution was produced by Nick Petalas. MatShep posed the question in #5675 and proved the +n = 1, 2 thresholds (#5549, #5675). Ali Romman proved the 4n+4 upper bound +(#5526), the native grammar and Fourier framework (#5369, #5529) and the +cuspidal residual (#5635). Joseph Anglada (#5542) introduced the coset method. +The n = 2 (mod 4) refinement uses #5902. Self-orthogonal codes, Schur products +and Green's character theorem are classical. New work is Apache-2.0. diff --git a/research/clifford-threshold-linear-lower/SOURCES.json b/research/clifford-threshold-linear-lower/SOURCES.json new file mode 100644 index 0000000000..1ac69e952d --- /dev/null +++ b/research/clifford-threshold-linear-lower/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/clifford-pointwise-faithfulness/README.md", + "usage": "input", + "git_blob": "a250d034c5e7b9ac98e9049e039754b6b0c38158", + "sha256": "b929248f5ad414ac776a2fa9cdc52ab745305aa257946e9b3596684ba1d74721" + }, + { + "path": "research/full-clifford-two-qubit-centre/README.md", + "usage": "input", + "git_blob": "caf6938e3b78077c319dd8228fc3c6070f4cc451", + "sha256": "f5a6a0edfac72bc1899a484f0fd679d1173f4a9048d3e3e2e1f3bfca7658d90b" + }, + { + "path": "research/nine-axis-cutoff-sharpness/PROOF.md", + "usage": "input", + "git_blob": "1ba92a64c521f25f7aa50ff95731ba893be5fe56", + "sha256": "e4e38b0559b0d64de095bee68c0d7bddc61020e843d75f8ca66e3c7b6655a8c3" + } + ] +} diff --git a/research/clifford-threshold-linear-lower/TASK.json b/research/clifford-threshold-linear-lower/TASK.json new file mode 100644 index 0000000000..9da69a1d23 --- /dev/null +++ b/research/clifford-threshold-linear-lower/TASK.json @@ -0,0 +1,103 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "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 an all-n lower bound on the pointwise tensor-independence threshold T(n) of the full n-qubit Gaussian-dyadic Clifford group: its projective tensor Gram is singular at every width f <= 2n, so 2n+1 <= T(n) <= 4n+4 for n >= 2.", + "scope_change_reason": "The formal-interface card is narrowed away from proof-assistant formalization and selected callers to the explicit open question of MatShep PR5675 (does the sharp threshold 4n+1 continue beyond two qubits). This is a written native-interface side result, not a discharge of a selected framework assumption.", + "bottleneck_link": "Side result. Exact native interface tests need widths at or above the Clifford threshold; this proves that any such test window must grow at least like 2n+1 with the qubit count, complementing the 4n+4 sufficient window of PR5526. No kappa or invoice changes.", + "budget_minutes": 60, + "stop_rule": "Ship the first all-n lower bound; do not attempt the three-qubit character computation.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py exact finite corroboration (code step for n=2,3,4, cuspidal cosets for n=2,3, literal two-qubit Gram null vectors at widths 1..4, rejection controls)", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact three-qubit threshold T(3), now known to lie in [7,16]?", + "why_it_matters": "It decides whether the 4n+1 pattern of n=1,2 continues, and fixes the sharp native test window at three qubits.", + "first_step": "Compute the centre action of the 3-qubit Clifford group (order 4*92,897,280) on class functions at widths 7..13, as #5675 did at two qubits, or find which irreducible characters are absent from the 12th tensor power.", + "blocked_by": "No class or character table of the 3-qubit Clifford group is available in the repository; naive enumeration is far beyond the two-qubit method." + }, + { + "question": "Can Hadamard-type Clifford elements raise the all-n lower bound above 2n+1, toward 4n+1?", + "why_it_matters": "The present residual lives in the Hadamard-free monomial subgroup, whose own threshold is only about 2n+3; the gap to the n=2 value 9 comes from the full group.", + "first_step": "At n=2, identify the 1-dimensional determinant-character null vector of #5675 at width 8 and look for an all-n analogue supported on the full group (the determinant itself is trivial for n>=3).", + "blocked_by": "No candidate full-group residual is known beyond n=2." + } + ], + "question_source": "PR #5675", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19221825" +} diff --git a/research/clifford-threshold-linear-lower/VERIFY.json b/research/clifford-threshold-linear-lower/VERIFY.json new file mode 100644 index 0000000000..0d0e34fa5f --- /dev/null +++ b/research/clifford-threshold-linear-lower/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/clifford-pointwise-faithfulness/README.md", + "research/full-clifford-two-qubit-centre/README.md", + "research/nine-axis-cutoff-sharpness/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Code step for n=2,3,4 exhaustive and n=2..64 explicit tuple; cuspidal coset sums on GL(2,2) and GL(3,2); literal two-qubit Clifford membership, class Gram null vectors at widths 1..4 and visibility at 9..12; three rejection controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete finite check with optimization; checks use explicit require calls, not assert." + } + ] +} diff --git a/research/clifford-threshold-linear-lower/verify.py b/research/clifford-threshold-linear-lower/verify.py new file mode 100644 index 0000000000..28ef831e11 --- /dev/null +++ b/research/clifford-threshold-linear-lower/verify.py @@ -0,0 +1,399 @@ +#!/usr/bin/env python3 +"""Finite corroboration for the linear lower bound on the Clifford threshold. + +Checks, all in exact integer or Gaussian-integer arithmetic: + +1. Code lemma: for n = 2, 3, 4 no zero-phase multiset of at most 2n points + of F2^n has full affine span (exhaustive), and the explicit length-(4n+1) + tuple has zero phase and full affine span for n = 2..64. +2. Cuspidal cancellation input at n = 2, 3: every coset of every hyperplane + pointwise stabilizer has zero character sum. +3. Two-qubit transfer, literally: the 3072 monomial matrices are Clifford + (they normalize the Pauli group) and give 768 projective classes. At every + width f = 1..4 the residual P_(f mod 4) gives a nonzero class vector v with + H_f v = 0 for the exact class Gram (tr(U_a^* U_b))^f. The same residual is + visible at widths 9..12 on the explicit full-span tuple. +4. Rejection controls: the trivial character, the sign with its order-three + values negated, and a single perturbed coefficient each give H_4 v != 0. +""" + +from itertools import combinations_with_replacement, product + +MARKER = "PASS_CLIFFORD_THRESHOLD_LINEAR_LOWER" + + +def require(condition, message): + if not condition: + raise SystemExit("FAIL: " + message) + + +# ---------------------------------------------------------------- F2 helpers + +def rank_f2(rows): + rows = [r for r in rows if r] + rank = 0 + while rows: + pivot = rows.pop() + rank += 1 + low = pivot & -pivot + rows = [r ^ pivot if r & low else r for r in rows] + rows = [r for r in rows if r] + return rank + + +def full_affine_span(points, n): + """Points are n-bit ints; full span iff rank of (1, x) columns is n + 1.""" + return rank_f2([(x << 1) | 1 for x in points]) == n + 1 + + +def zero_phase(points, n): + for j in range(n): + if sum((x >> j) & 1 for x in points) % 4: + return False + for j in range(n): + for k in range(j + 1, n): + if sum((x >> j) & (x >> k) & 1 for x in points) % 2: + return False + return True + + +def check_code_lemma(): + counted = {} + for n in (2, 3, 4): + zero_count = 0 + for f in range(1, 2 * n + 1): + for tup in combinations_with_replacement(range(1 << n), f): + if zero_phase(tup, n): + zero_count += 1 + require(not full_affine_span(tup, n), + f"full-span zero-phase tuple n={n} f={f}: {tup}") + counted[n] = zero_count + for n in range(2, 65): + tup = [0] + [1 << j for j in range(n) for _ in range(4)] + require(len(tup) == 4 * n + 1, "explicit tuple length") + require(zero_phase(tup, n), f"explicit tuple phase n={n}") + require(full_affine_span(tup, n), f"explicit tuple span n={n}") + return counted + + +# ------------------------------------------------------------- GL(n,2) data + +def gl_maps(n): + """Invertible maps as column tuples; g(x) = XOR of columns at set bits.""" + cols = range(1, 1 << n) + out = [] + for c in product(cols, repeat=n): + if rank_f2(list(c)) == n: + out.append(c) + return out + + +def apply(cols, x): + y = 0 + for j, c in enumerate(cols): + if (x >> j) & 1: + y ^= c + return y + + +def compose(a, b): + """(a o b) as columns.""" + return tuple(apply(a, c) for c in b) + + +def order(cols, n): + ident = tuple(1 << j for j in range(n)) + g, k = cols, 1 + while g != ident: + g, k = compose(cols, g), k + 1 + return k + + +def psi(cols, n): + """Sum of cuspidal characters of GL(n,2), n = 2, 3 (Green; see PROOF.md). + + n = 2: GL(2,2) = S3 and the cuspidal character is the sign. + n = 3: the two degree-3 characters sum to 6, -2, 0, 2, -1 on classes of + order 1, 2, 3, 4, 7. + """ + o = order(cols, n) + if n == 2: + return {1: 1, 2: -1, 3: 1}[o] + return {1: 6, 2: -2, 3: 0, 4: 2, 7: -1}[o] + + +def check_cuspidal_cosets(): + checked = 0 + for n in (2, 3): + maps = gl_maps(n) + ident = tuple(1 << j for j in range(n)) + transvection = None + for phi in range(1, 1 << n): # hyperplane V = ker(phi . x) + stab = [g for g in maps + if all(apply(g, x) == x for x in range(1 << n) + if bin(phi & x).count("1") % 2 == 0)] + require(len(stab) == 1 << (n - 1), "stabilizer size") + for h in stab: + if h != ident: + require(rank_f2([apply(h, 1 << j) ^ (1 << j) + for j in range(n)]) == 1, + "stabilizer element is a transvection") + transvection = h + for g in maps: + require(sum(psi(compose(g, h), n) for h in stab) == 0, + f"coset sum n={n}") + checked += 1 + d = 1 + for i in range(1, n): + d *= 2 ** i - 1 + orbits = {2: 1, 3: 2}[n] # phi(2^n - 1) / n + d *= orbits + require(psi(ident, n) == d, "cuspidal degree") + require(psi(transvection, n) * (2 ** (n - 1) - 1) == -d, + "transvection value") + return checked + + +# ----------------------------------------------- two-qubit monomial group + +N_AXES = 2 +DIM = 1 << N_AXES + + +def gmul(a, b): + return (a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0]) + + +def gpow(a, e): + r = (1, 0) + for _ in range(e): + r = gmul(r, a) + return r + + +IPOW = [(1, 0), (0, 1), (-1, 0), (0, -1)] + + +def monomial_group(): + """Elements U(g,t,q): e_x -> i^q(x) e_(g x + t). Returns list of dicts.""" + elems = [] + for lin in gl_maps(N_AXES): + for t in range(DIM): + for c in range(4): + for a in product(range(4), repeat=N_AXES): + for b in range(2): + ph = [] + for x in range(DIM): + x0, x1 = x & 1, (x >> 1) & 1 + ph.append((c + a[0] * x0 + a[1] * x1 + + 2 * b * x0 * x1) % 4) + perm = tuple(apply(lin, x) ^ t for x in range(DIM)) + elems.append({"lin": lin, "t": t, "c": c, + "perm": perm, "ph": tuple(ph)}) + return elems + + +def dense(e): + m = [[(0, 0)] * DIM for _ in range(DIM)] + for x in range(DIM): + m[e["perm"][x]][x] = IPOW[e["ph"][x]] + return m + + +def matmul(a, b): + n = len(a) + out = [[(0, 0)] * n for _ in range(n)] + for i in range(n): + for k in range(n): + if a[i][k] != (0, 0): + for j in range(n): + if b[k][j] != (0, 0): + p = gmul(a[i][k], b[k][j]) + o = out[i][j] + out[i][j] = (o[0] + p[0], o[1] + p[1]) + return out + + +def adjoint(m): + n = len(m) + return [[(m[j][i][0], -m[j][i][1]) for j in range(n)] for i in range(n)] + + +def kron(a, b): + return [[gmul(a[i // len(b)][j // len(b)], b[i % len(b)][j % len(b)]) + for j in range(len(a) * len(b))] for i in range(len(a) * len(b))] + + +def paulis(): + i2 = [[(1, 0), (0, 0)], [(0, 0), (1, 0)]] + x = [[(0, 0), (1, 0)], [(1, 0), (0, 0)]] + z = [[(1, 0), (0, 0)], [(0, 0), (-1, 0)]] + singles = {"I": i2, "X": x, "Z": z, "XZ": matmul(x, z)} + table = {} + for a, b in product(singles, repeat=2): + table[(a, b)] = kron(singles[b], singles[a]) # qubit 0 is low bit + return table + + +def is_clifford(e, pauli_table): + u = dense(e) + ud = adjoint(u) + targets = [] + for p in pauli_table.values(): + targets.append(p) + for p in pauli_table.values(): + img = matmul(matmul(u, p), ud) + ok = False + for q in targets: + for s in IPOW: + if all(img[i][j] == gmul(s, q[i][j]) + for i in range(DIM) for j in range(DIM)): + ok = True + break + if ok: + break + if not ok: + return False + return True + + +def class_key(e): + """Projective class: strip the constant phase c.""" + return (e["perm"], tuple((p - e["c"]) % 4 for p in e["ph"])) + + +def sign_psi(lin): + return psi(lin, 2) + + +def residual(elems, r, coeff_fn): + """Integer-scaled P_r = |D| * A E_r as {element index: Gaussian int}.""" + out = {} + for idx, e in enumerate(elems): + w = coeff_fn(e["lin"]) + if w == 0: + continue + s = IPOW[(-r * e["c"]) % 4] + out[idx] = (w * s[0], w * s[1]) + return out + + +def class_vector(elems, coeffs, f): + """Combine scalar lifts at width f: U = i^c U0 gives i^(c f) U0^(x f).""" + v = {} + for idx, w in coeffs.items(): + e = elems[idx] + k = class_key(e) + term = gmul(w, IPOW[(e["c"] * f) % 4]) + o = v.get(k, (0, 0)) + v[k] = (o[0] + term[0], o[1] + term[1]) + return {k: w for k, w in v.items() if w != (0, 0)} + + +def trace_star(ka, kb): + """tr(U_a^* U_b) for class representatives (constant phase zero).""" + perm_a, ph_a = ka + perm_b, ph_b = kb + tot = (0, 0) + for x in range(DIM): + if perm_a[x] == perm_b[x]: + p = IPOW[(ph_b[x] - ph_a[x]) % 4] + tot = (tot[0] + p[0], tot[1] + p[1]) + return tot + + +def gram_apply(classes, v, f): + """Return max |(H_f v)_a| witness: list of nonzero entries (exact).""" + bad = 0 + for ka in classes: + acc = (0, 0) + for kb, w in v.items(): + t = trace_star(ka, kb) + if t == (0, 0): + continue + term = gmul(gpow(t, f), w) + acc = (acc[0] + term[0], acc[1] + term[1]) + if acc != (0, 0): + bad += 1 + return bad + + +def diagonal_entry(elems, coeffs, tup): + """ computed from the literal monomial action.""" + acc = (0, 0) + fixers = set() + for idx, w in coeffs.items(): + e = elems[idx] + if all(e["perm"][x] == x for x in tup): + fixers.add((e["lin"], e["t"])) + p = IPOW[sum(e["ph"][x] for x in tup) % 4] + term = gmul(w, p) + acc = (acc[0] + term[0], acc[1] + term[1]) + return acc, fixers + + +def check_two_qubit(): + elems = monomial_group() + require(len(elems) == 6 * 4 * 128, "monomial group size") + table = paulis() + require(all(is_clifford(e, table) for e in elems), + "every monomial element normalizes the Pauli group") + classes = sorted({class_key(e) for e in elems}) + require(len(classes) == 768, "projective class count") + + full_tuple = [0] + [1 << j for j in range(N_AXES) for _ in range(4)] + results = {} + for f in range(1, 2 * N_AXES + 1): + r = f % 4 + p = residual(elems, r, sign_psi) + v = class_vector(elems, p, f) + require(len(v) > 0, f"nonzero class vector f={f}") + require(gram_apply(classes, v, f) == 0, f"H_f v = 0 at f={f}") + results[f] = len(v) + visible = {} + for f in range(4 * N_AXES + 1, 4 * N_AXES + 5): + r = f % 4 + p = residual(elems, r, sign_psi) + tup = full_tuple + [0] * (f - len(full_tuple)) + entry, fixers = diagonal_entry(elems, p, tup) + require(len(fixers) == 1, "only the identity affine map fixes tuple") + require(entry == (128, 0), f"visible diagonal entry at f={f}") + visible[f] = entry[0] + + # Rejection controls. + trivial = residual(elems, 0, lambda lin: 1) + require(gram_apply(classes, class_vector(elems, trivial, 4), 4) > 0, + "control: trivial character must fail") + def not_a_character(lin): + return -1 if lin != tuple(1 << j for j in range(N_AXES)) else 1 + broken = class_vector(elems, residual(elems, 0, not_a_character), 4) + require(gram_apply(classes, broken, 4) > 0, + "control: sign with order-three values negated must fail") + mutated = dict(residual(elems, 0, sign_psi)) + first = min(mutated) + w = mutated[first] + mutated[first] = (w[0] + 1, w[1]) + require(gram_apply(classes, class_vector(elems, mutated, 4), 4) > 0, + "control: perturbed coefficient must fail") + return results, visible + + +def main(): + counted = check_code_lemma() + cosets = check_cuspidal_cosets() + support, visible = check_two_qubit() + print("zero-phase multisets of size <= 2n (all lack full span):", + {n: counted[n] for n in sorted(counted)}) + print("explicit full-span zero-phase tuples of length 4n+1: n=2..64") + print("cuspidal coset sums checked (n=2,3):", cosets) + print("two-qubit class-vector support sizes with H_f v = 0:", + {f: support[f] for f in sorted(support)}) + print("two-qubit visible diagonal entries (scaled by |D|=128):", + {f: visible[f] for f in sorted(visible)}) + print("rejection controls: trivial character, negated order-three values, " + "perturbed coefficient") + print(MARKER) + + +if __name__ == "__main__": + main()