diff --git a/research/clifford-seven-rotation-gap/PROOF.md b/research/clifford-seven-rotation-gap/PROOF.md new file mode 100644 index 0000000000..2a2d7907a7 --- /dev/null +++ b/research/clifford-seven-rotation-gap/PROOF.md @@ -0,0 +1,203 @@ +# A seven-rotation improvement to the odd-axis Clifford Gram bound + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written mathematical proof, with exact finite corroboration. +Independent human and formal proof-kernel review are unclaimed. + +## Statement and cited inputs + +Let n be odd, n>=3, D=2^n, and choose one unitary representative U_g +of each projective n-axis Gaussian-dyadic Clifford operator. The scalar +kernel of the exact group is {1,i,-1,-i}. For every integer f>=4n+4, +define the normalized tensor Gram matrix + + G_f[g,h] = (tr(U_g* U_h)/D)^f. + +Then + + G_f >= gamma I, + gamma = 14601049/29130752 > 1/2. (1) + +Equivalently, arbitrary complex coefficients, including coefficients chosen +separately at each width, satisfy + + D^(-f) ||sum_g b_g U_g^(tensor f)||_HS^2 + >= gamma sum_g |b_g|^2. (2) + +Principal submatrices inherit the bound. Changing representative phases +conjugates G_f by a diagonal unitary and preserves it. + +We cite, without re-enumerating or auditing, the following inputs from Ali +Romman's #5526 and Hiroki KUMAZAKI's #5694. Put N=2n and let c_(N,k) +count symplectic Pauli actions S with rank(S-I)=k. + +* c_(N,k) <= 2^(Nk-k(k-1)/2). +* Exactly 2^k projective lifts of each such S have nonzero trace. Their + normalized trace modulus is 2^(-k/2). +* Every rank-one S is the transvection associated with a unique nonzero + binary Pauli label v. Its two nonzero-trace lifts are C_P and C_P^(-1), + where P is a Hermitian Pauli with label v and + + C_P = ((1+i)I + (1-i)P)/2. + +The last item also follows directly from C_P's Pauli conjugation action: +C_P^2=P, its symplectic action is that transvection, and the cited lift +count is two. The two projective lifts are distinct because P is nonscalar. + +The cited count and trace formula bound the absolute row contribution at +each displacement rank k, when f>=2N+4, by + + 2^k c_(N,k) 2^(-kf/2) <= 2^(-k(k+1)/2). (3) + +Set T=sum_(k>=1) 2^(-k(k+1)/2). The exact rational upper tail certificate +in #5694 gives + + T <= T_plus = 2670177/4161536. + +Javier Vera's #5714 proves that T is the limiting absolute row sum, and +explicitly leaves spectral improvement open. We change the treatment of +rank one, rather than strengthen that asymptotically sharp count. + +## 1. Seven commuting quarter turns + +Take three independent commuting Hermitian Paulis P_1,P_2,P_3. For each +nonzero a in F_2^3 put P_a=product_j P_j^(a_j) and C_a=C_(P_a). +The seven C_a commute and have fourth power I. Moreover, + + product_(a!=0) C_a = I. (4) + +To see this, simultaneously diagonalize the three commuting involutions. +Write their joint eigenvalues as (-1)^(x_j). On this eigenspace C_a has +eigenvalue i^(a dot x). If x=0 all seven exponents vanish. If x!=0, +exactly four a have a dot x=1, so the product is i^4=1. + +This relation holds as an exact operator identity, before taking a +projective quotient. For a general isotropic label space, choosing the +signed products P_a is essential. Arbitrary independent sign choices +need not give (4). + +Let R be any unitary representation of the projective Clifford group. +The seven R(C_a) still commute, have fourth power I, and have product I. +On a simultaneous eigenspace their eigenvalues lambda_a are fourth roots +with product one. Therefore + + sum_(a!=0) (lambda_a + conjugate(lambda_a)) >= -10. (5) + +Here is an elementary proof. Each summand belongs to {-2,0,2}. A sum +below -10 is either -14, requiring seven eigenvalues -1, or -12, +requiring six eigenvalues -1 and one eigenvalue i or -i. Their products +are respectively -1 and i or -i, contradicting product one. Six -1 +and one +1 give -10 and product one, so this root constraint alone +cannot give a larger constant. Thus, in operator order, + + sum_(a!=0) (R(C_a)+R(C_a)*) >= -10 I. (6) + +## 2. Average over Clifford conjugation + +For each of the m=2^(2n)-1 nonzero unsigned Pauli labels v choose a +Hermitian representative P_v and define + + A = sum_(v!=0) (R(C_(P_v))+R(C_(P_v))*). + +The pair of summands is independent of the sign choice. Indeed +C_(-P)=i C_P^(-1), so their projective classes are inverses. Clifford +conjugation acts transitively on the nonzero labels, and consequently +averaging a conjugate of the left side of (6) gives (7/m) A. Every +conjugate obeys the same operator inequality. Hence + + A >= -(10/7) m I. (7) + +This is the new step. The absolute row bound for this adjacency operator +would only give A>=-2m I. Its lower coefficient improves by the factor 5/7. +We assert a sufficient bound, not the exact full-group minimum eigenvalue. + +## 3. Apply the bound to the tensor Gram matrix + +First take f_0=4n+4. Since n is odd, f_0 is divisible by eight. Its +Gram kernel is well-defined on the projective group because the exact +scalar kernel has order four. Choose the right-regular convention +(R(a)b)(g)=b(ga). Then the kernel convolution has entries +G_(f_0)[g,h]=(tr(U_g*U_h)/D)^(f_0). Products of representatives can differ +by a scalar fourth root, whose f_0-th power is one. + +For C_P and its inverse, + + tr(C_P)/D = (1+i)/2, + (tr(C_P)/D)^(f_0) = 2^(-f_0/2) = w > 0. + +Thus the complete displacement-rank-one contribution is exactly w A in +the right-regular representation. All other nonidentity nonzero-trace +contributions have displacement rank at least two. Write + + G_(f_0) = I + w A + H. + +The remaining matrix H is Hermitian. Equation (3) bounds its absolute +off-diagonal row sum by T-1/2, so H>=-(T-1/2)I. This uses the elementary +inequality 2|b_g b_h|<=|b_g|^2+|b_h|^2 in its quadratic form. +Meanwhile (7) and m<2^(2n) give + + w A >= -(10/7) m 2^(-2n-2) I >= -(5/14) I. + +Combining the two bounds yields + + G_(f_0) >= (1-5/14-(T-1/2)) I + = (1-T+1/7) I + >= (1-T_plus+1/7) I + = (14601049/29130752) I. (8) + +The improvement over #5694's rational lower constant is exactly 1/7 +in this odd-axis domain. The new constant exceeds 1/2 by +35673/29130752. No sharpness for the complete Gram matrix is claimed. + +For later widths, G_(f+1)=G_f entrywise-multiplied by G_1. The matrix G_1 +is positive semidefinite with diagonal one. If G_f>=gamma I, its entrywise +product with G_1 preserves the same lower bound. Explicitly, write +G_1=sum_j v_j v_j*. Then + + (G_f-gamma I) entrywise-multiplied by G_1 + = sum_j diag(v_j)(G_f-gamma I)diag(v_j)* >= 0. + +This proves (1) at every f>=f_0. It also explains why the projective +convolution argument only needs to be used at the initial width. + +## 4. Scope, finite evidence and remaining questions + +The written argument supplies all odd n>=3 and all f>=4n+4. The finite +verifier checks its new local ingredients, not those universal quantifiers +or the cited predecessor counts. In F_2^6 it enumerates every isotropic +three-space and checks uniform point incidence. For a chosen signed basis +in each space it applies all seven literal 8-by-8 quarter turns to every +input basis column, using Gaussian integers and an explicit denominator. +An abstract fourth-root enumeration and a separate 512-character diagonal +subgroup calculation both give minimum -10. Wrong words and the excluded +phase residue supply rejection controls. The emitted receipt binds the +package and cited input bytes by SHA-256. + +For the diagonal calculation the three coordinate turns generate the +three order-four single-axis phases. The turn on e_i+e_j, divided by +the two coordinate turns, gives the order-two controlled phase on i,j. +These six independent parameters give Z4^3 x Z2^3. The turn on v has +coordinates (v_i; v_i v_j), since binary parity modulo four is +sum_i v_i x_i - 2 sum_(i=3 and every tensor width f>=4n+4, the normalized Gram +matrix of the full projective Gaussian-dyadic Clifford alphabet satisfies + + Gram_f >= (14601049/29130752) I > (1/2) I. + +This improves Hiroki KUMAZAKI's #5694 sufficient lower constant +1491359/4161536 by exactly 1/7 in this domain. The new constant is +approximately 0.501224582187. It answers the odd-axis part of the +phase-aware spectral-strengthening question in Javier Vera's #5714. +The exact spectrum and optimal constant remain open. + +Claim type: scoped written mathematical proof with exact finite +corroboration. Independent human and formal proof-kernel review are +unclaimed. No new kappa or physical supplier follows. + +## New step and dependencies + +Seven quarter turns associated with the nonzero vectors of a +three-dimensional isotropic Pauli space commute and multiply to I. +Their regular-action adjacency sum is at least -10 I. Averaging over +Clifford conjugation improves the rank-one displacement contribution +by the factor 5/7. At the odd-axis initial width its coefficient is +positive. The cited higher-rank count bounds the remaining terms. +Entrywise Gram multiplication propagates the result to later widths. + +[PROOF.md](PROOF.md) gives the argument, normalization and phase restriction. +We cite Ali Romman's #5526 trace framework and #5694's count and rational +tail certificate. No predecessor executable, group census or caller replay +is run. [SOURCES.json](SOURCES.json) pins their proof bytes and #5714's +explicit open question on canonical main +de5ec2e7a6074068452f45b1a191b5c72832df4a. + +This is a side result with scope changed from the `scalar-to-moment` +suggestion. The revision-8 selected baseline binding example passed; +the result concerns quantitative native-alphabet separation rather than +a complete paid/target invoice. The selected record is unchanged. + +## Reproduction and evidence + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/clifford-seven-rotation-gap/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/clifford-seven-rotation-gap/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/clifford-seven-rotation-gap +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/clifford-seven-rotation-gap --check-source-history +``` + +Another CPython 3.12 path can replace the absolute interpreter path. +[VERIFY.json](VERIFY.json) registers both warning-strict normal and +optimized commands, each with a 120-second limit. The verifier writes +only to stdout, including a generated SHA-256-bound receipt. No saved +receipt is maintained by hand. + +The exact finite checks enumerate: + +* All 135 isotropic three-spaces in F_2^6, with each of the 63 points + occurring exactly 15 times. This tests the new averaging geometry. +* All 1,080 basis columns of their signed seven-rotation words, using + literal Pauli actions and integer Gaussian arithmetic. +* All 4,096 fourth-root tuples with product one. Their adjacency + minimum is -10. +* All 512 characters of the diagonal subgroup Z4^3 x Z2^3. Its adjacency + spectrum has multiplicities {-10:7, -6:56, -2:203, 2:168, 6:77, 14:1}. +* Forty-nine omitted/replaced-word controls, two semantic controls and + five out-of-scope controls, plus 120 width fixtures and exact arithmetic + for the new rational constant. + +Finite corroboration does not enumerate the full three-axis Clifford +group or prove the all-dimension quantifiers. Those are supplied by the +written argument using the cited inputs. The receipt authenticates bytes, +not mathematical correctness. The verifier neither imports nor executes +the predecessor checks. + +## Limits and implementation constraints + +The initial-width improvement requires odd n>=3. For even n, the starting +width is four modulo eight and the rank-one coefficient has the opposite +sign. Arbitrary non-Clifford operators, nonunitary scales, nonlinear leaves +and rounded equalities are outside the theorem. Exact scalar-phase copies +must be combined before using a projective Gram matrix. Source-dependent +physical costs, ownership, restoration and the five selected framework +assumptions are not discharged. + +The standalone verifier has fixed finite domains, no recursion, no child +processes and no output files. Functions remain below 60 physical lines. +Explicit exceptions keep every check active under optimized execution. +Managed Python allocation is a deviation from Power of Ten rule 3: +the root scan streams at most 4^7 tuples, stores seven spectral bins, +135 seven-point spaces and at most 512 eight-entry character tuples. +The source inventory has at most eight rows, its JSON at most 64 KiB, +and each authenticated input/package file at most 1 MiB. Runtime/library +allocation is not inspected. A port to a restricted runtime would require fixed arrays +before a constant-allocation claim. Library iteration and dispatch are +bounded by these domains; there are no user-supplied callbacks. +Warning-strict execution and the repository metadata/commit checks provide +the available diagnostics; no external static analyzer is required by the +package. + +## Open next questions + +1. Can a phase-aware argument improve the even-axis bound at f=4n+4? + Its rank-one sign is negative, so the new lower adjacency estimate + does not help there. First seek an upper adjacency or joint-rank + inequality that accounts for the trivial character. No such bound + or complete even-axis spectrum is provided. +2. What is the best odd-axis Gram lower constant? The seven-root + inequality is sharp for that local relation, while the full-group + averaging and higher-rank triangle bounds can lose information. + First relate the higher displacement classes to the same local + subgroups. A full representation argument remains missing. + +## Credit and overlap + +Credit Javier Vera / #5714 for the explicit open question and row-method +limitation, Hiroki KUMAZAKI / #5694 for the count and tail certificate, +and Ali Romman / #5526 for the trace-lift/projective Gram framework. +Their classical Pauli, symplectic and Clifford sources and retained +native/kernel attribution remain with those pinned packages. +MatShep's #5549/#5594/#5675 one-/two-axis spectra and Ali Romman's #5727 +finite-span contraction tools concern distinct results and are not replayed. +No global literature-priority claim is made. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214984) +states the odd-axis scope. Overlap checking covered live open titles, +recent account contributions, recent handoffs, active Discussions, +relevant PR bodies, distinctive main README/proof terms and merged searches. +The card overlap helper reported incomplete local sparse coverage, which +was supplemented by Git-object searches. These checks do not establish +universal novelty or cover unpublished work. diff --git a/research/clifford-seven-rotation-gap/SOURCES.json b/research/clifford-seven-rotation-gap/SOURCES.json new file mode 100644 index 0000000000..be370ce883 --- /dev/null +++ b/research/clifford-seven-rotation-gap/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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/PROOF.md", + "usage": "input", + "git_blob": "465009d9d1b6947e80e6f1e868022f47ddab1f3c", + "sha256": "45483e4b5f604a5e70602c5caaa4394d4a0d0d1a6d0b6e8a93b836d50b23f764" + }, + { + "path": "research/clifford-residual-count-bound/PROOF.md", + "usage": "input", + "git_blob": "1a604a44071dd65bbf070ac151ad2e85ce7e6d46", + "sha256": "c7e99a80da4c651edce8ffa854ee70e7fed6d68db8474ae3f8a66ac554d79dd9" + }, + { + "path": "research/clifford-row-sharpness/README.md", + "usage": "input", + "git_blob": "70ab9d3a62fd0cf6589e034c89f22a49a9411084", + "sha256": "8fc1af282142444ba9a3b910bb890fc48b4dec032774e77ba3a7111306681e92" + } + ] +} diff --git a/research/clifford-seven-rotation-gap/TASK.json b/research/clifford-seven-rotation-gap/TASK.json new file mode 100644 index 0000000000..f2cad50d98 --- /dev/null +++ b/research/clifford-seven-rotation-gap/TASK.json @@ -0,0 +1,119 @@ +{ + "schema_version": 1, + "task_id": "scalar-to-moment", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "scalar-to-moment", + "question": "Can a scalar/frame rewrite improve the complete signed moment through paid jobs, productive targets, or both?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Require a legal chronological rewrite and favorable complete signed target-minus-paid moment with all extra charges. Unchanged ADD counts or unchanged paid-call counts alone decide neither success nor failure. Compiler, native and outer admission remain separate obligations.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Construct one legal source-bound rewrite and compare complete before/after P and T. Charge restoration, source windows and owned helpers. A paid call need not disappear: a legal target split or rank redistribution may win. Stop if the signed moment is unchanged or the consumer repays the gain. Do not extend a scalar-only census on ADD counts.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "signed moment", + "target split", + "rank exchange", + "scalar rewrite" + ], + "existing_checks": [ + { + "scope": "PR #3998: consecutive A2 scalar contraction", + "evidence": "research/staged544-a2-graph-rewrite/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4019: separated A2 sites with unchanged recursive histogram", + "evidence": "research/staged544-separated-a2/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "f408e09df300b575235f7f77f81948071397e16d", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4112: composition audit", + "evidence": "research/staged544-a2-composition-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "205b7380656ba4b6316a8a493b1a3c679b8f7a0e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4152: A1858 contraction audit", + "evidence": "research/staged544-a1858-contraction-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "caaa14cde5962adc372fdca71f63d0f29e73c8b2", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the uniform Clifford tensor Gram lower constant 14601049/29130752 > 1/2 for every odd n>=3 and every f>=4n+4, by averaging the seven commuting Pauli quarter-turn relation.", + "scope_change_reason": "The picker suggested scalar-to-moment, but live overlap favors the explicit phase-aware spectral question in Javier Vera PR5714. This is an algebraic side result, not a complete paid/target rewrite or an invoice improvement.", + "bottleneck_link": "Quantitative native-alphabet separation supports recursive-interface error obstructions. This improves the odd-axis robustness constant only and supplies no physical caller or paid savings.", + "budget_minutes": 60, + "stop_rule": "Ship the first spectral improvement after exact local relation checks. No new full-group census, complete caller or larger construction search.", + "outcome": "completed", + "evidence": "PROOF.md derives a 5/7 rank-one adjacency bound from seven commuting quarter turns and combines the cited higher-rank envelope with Schur propagation. verify.py checks the new finite relation, incidence, spectra and failure controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the even-axis starting-width Gram bound be improved using phases?", + "why_it_matters": "The rank-one coefficient is negative there, so the new lower adjacency estimate cannot be substituted.", + "first_step": "Seek an upper adjacency or joint-rank inequality at f=4n+4 accounting for the trivial character.", + "blocked_by": "No matching phase-aware even-axis operator inequality is supplied." + }, + { + "question": "What is the best uniform odd-axis lower constant?", + "why_it_matters": "The seven-root relation is locally sharp, but averaging and the higher-rank triangle bound may lose information.", + "first_step": "Relate higher displacement classes to the same local subgroups.", + "blocked_by": "Requires a full representation argument beyond the present local relation." + } + ], + "selection": { + "seed": "89c4bad5e85495b5d9350c3ab424e711", + "scope_key": "dc097aa37157d89dcb0c", + "question_source": "PR #5714, Open next question 2", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214984" + } +} diff --git a/research/clifford-seven-rotation-gap/VERIFY.json b/research/clifford-seven-rotation-gap/VERIFY.json new file mode 100644 index 0000000000..cceb20c55c --- /dev/null +++ b/research/clifford-seven-rotation-gap/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/clifford-pointwise-faithfulness/PROOF.md", + "research/clifford-residual-count-bound/PROOF.md", + "research/clifford-row-sharpness/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact signed seven-rotation endpoints, complete three-space incidence, abstract/diagonal spectra, rational bound and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete checks with optimization enabled and warnings treated as errors." + } + ] +} diff --git a/research/clifford-seven-rotation-gap/verify.py b/research/clifford-seven-rotation-gap/verify.py new file mode 100644 index 0000000000..9be77b2d1e --- /dev/null +++ b/research/clifford-seven-rotation-gap/verify.py @@ -0,0 +1,231 @@ +"""Exact finite corroboration of the seven-rotation spectral argument. + +No predecessor executable is imported or run. The all-dimension theorem is +the written proof; these fixed finite checks test its new local ingredients. +""" + +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations, product +import json +from pathlib import Path +import sys + + +PACKAGE = Path(__file__).resolve().parent +REAL = (1, 0, -1, 0) +PACKAGE_FILES = ( + "README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py" +) + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def symplectic(u: int, v: int) -> int: + return (((u & 7) & (v >> 3)) ^ ((u >> 3) & (v & 7))).bit_count() % 2 + + +def span(basis: tuple[int, int, int]) -> tuple[int, ...]: + a, b, c = basis + return tuple(sorted((a, b, c, a ^ b, a ^ c, b ^ c, a ^ b ^ c))) + + +def isotropic_spaces() -> dict[tuple[int, ...], tuple[int, int, int]]: + spaces = {} + # Exactly C(63,3)=39711 candidate triples; no larger domain is accepted. + for basis in combinations(range(1, 64), 3): + points = span(basis) + if len(set(points)) != 7 or 0 in points: + continue + if any(symplectic(u, v) for u, v in combinations(basis, 2)): + continue + spaces.setdefault(points, basis) + require(len(spaces) <= 135, "space capacity exceeded") + incidences = Counter(v for points in spaces for v in points) + require(len(spaces) == 135, "isotropic-space census") + require(incidences == Counter({v: 15 for v in range(1, 64)}), "nonuniform incidence") + return spaces + + +def pauli(label: int) -> tuple[int, int, int]: + x, z = label & 7, label >> 3 + return x, z, (x & z).bit_count() % 4 + + +def multiply(a: tuple[int, int, int], b: tuple[int, int, int]) -> tuple[int, int, int]: + x, z, phase = a + xx, zz, pp = b + return x ^ xx, z ^ zz, (phase + pp + 2 * (z & xx).bit_count()) % 4 + + +def signed_axes(basis: tuple[int, int, int]) -> tuple[tuple[int, int, int], ...]: + axes = [] + for mask in range(1, 8): + value = (0, 0, 0) + for j in range(3): + if mask & (1 << j): + value = multiply(value, pauli(basis[j])) + require(multiply(value, value) == (0, 0, 0), "non-Hermitian axis") + axes.append(value) + return tuple(axes) + + +def rotate(value: tuple[int, int], phase: int) -> tuple[int, int]: + a, b = value + return ((a, b), (-b, a), (-a, -b), (b, -a))[phase % 4] + + +def turn(vector: list[tuple[int, int]], axis: tuple[int, int, int]) -> list[tuple[int, int]]: + """Apply 2 C_P with Gaussian integers, so denominators stay explicit.""" + x, z, phase = axis + result = [(a - b, a + b) for a, b in vector] + for column in range(8): + a, b = rotate(vector[column], phase + 2 * (z & column).bit_count()) + c, d = result[column ^ x] + result[column ^ x] = c + a + b, d + b - a + return result + + +def is_identity_word(axes: tuple[tuple[int, int, int], ...]) -> bool: + require(len(axes) <= 7, "word exceeds seven rotations") + for column in range(8): + vector = [(int(row == column), 0) for row in range(8)] + for axis in axes: + vector = turn(vector, axis) + expected = [(int(row == column) * 2 ** len(axes), 0) for row in range(8)] + if vector != expected: + return False + return True + + +def literal_relations(spaces: dict) -> tuple[int, int]: + columns = 0 + for basis in spaces.values(): + require(is_identity_word(signed_axes(basis)), "literal seven-turn endpoint") + columns += 8 + axes = signed_axes((8, 16, 32)) + rejected = 0 + for omitted in range(7): + mutant = axes[:omitted] + axes[omitted + 1:] + require(not is_identity_word(mutant), "omitted rotation survived") + rejected += 1 + for replacement in range(7): + if replacement == omitted: + continue + mutant = axes[:omitted] + (axes[replacement],) + axes[omitted + 1:] + require(not is_identity_word(mutant), "replaced rotation survived") + rejected += 1 + return columns, rejected + + +def abstract_spectrum() -> Counter: + spectrum = Counter() + for exponents in product(range(4), repeat=7): + if sum(exponents) % 4 == 0: + spectrum[2 * sum(REAL[a] for a in exponents)] += 1 + require(sum(spectrum.values()) == 4096, "incomplete root domain") + require(min(spectrum) == -10, "seven-root lower constant") + require(spectrum == Counter({-10: 49, -6: 490, -2: 1519, + 2: 1484, 6: 511, 10: 42, 14: 1}), "root spectrum") + require(2 * sum(REAL[2] for _ in range(7)) < -10, "missing-product control") + return spectrum + + +def diagonal_group_spectrum() -> Counter: + """Characters of Z4^3 x Z2^3, separately from the abstract root scan.""" + spectrum = Counter() + functions = set() + for linear in product(range(4), repeat=3): + for quadratic in product(range(2), repeat=3): + phases = [] + for mask in range(8): + x = tuple((mask >> j) & 1 for j in range(3)) + pairs = (x[0] * x[1], x[0] * x[2], x[1] * x[2]) + phase = sum(linear[j] * x[j] for j in range(3)) + phase += 2 * sum(quadratic[j] * pairs[j] for j in range(3)) + phases.append(phase % 4) + functions.add(tuple(phases)) + require(sum(phases[1:]) % 4 == 0, "character violates product relation") + spectrum[2 * sum(REAL[a] for a in phases[1:])] += 1 + require(len(functions) == 512, "diagonal character parametrization") + require(spectrum == Counter({-10: 7, -6: 56, -2: 203, 2: 168, 6: 77, 14: 1}), + "diagonal regular-action spectrum") + # At the excluded f=4 mod 8, the rank-one coefficient has the opposite sign. + require(-max(spectrum) == -14 < -10, "wrong-width-sign control") + return spectrum + + +def scope(n: int, f: int) -> None: + if n < 3 or n % 2 == 0 or f < 4 * n + 4: + raise ValueError("requires odd n>=3 and f>=4n+4") + + +def constants() -> dict: + partial = sum((Fraction(1, 2 ** (k * (k + 1) // 2)) for k in range(1, 6)), Fraction()) + tail = Fraction(1, 2**21) / (1 - Fraction(1, 2**7)) + inherited_upper = partial + tail + gamma = 1 - Fraction(5, 14) - (inherited_upper - Fraction(1, 2)) + require(gamma == Fraction(14601049, 29130752) > Fraction(1, 2), "new constant") + checks = 0 + for n in range(3, 32, 2): + for offset in range(8): + scope(n, 4 * n + 4 + offset) + checks += 1 + f = 4 * n + 4 + require(f % 8 == 0, "starting phase residue") + mass = Fraction(2 * (2 ** (2 * n) - 1), 2 ** (f // 2)) + require(Fraction(5, 7) * mass < Fraction(5, 14), "rank-one normalization") + invalid = ((1, 8), (2, 16), (4, 24), (3, 15), (9, 39)) + for n, f in invalid: + try: + scope(n, f) + except ValueError: + continue + raise ValueError("out-of-scope fixture accepted") + return {"lower_constant": str(gamma), "gap_above_half": str(gamma - Fraction(1, 2)), + "width_fixtures": checks, "scope_rejections": len(invalid)} + + +def source_hashes() -> dict[str, str]: + root = PACKAGE.parent.parent + require((PACKAGE / "SOURCES.json").stat().st_size <= 65536, "manifest capacity") + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + require(len(manifest["files"]) <= 8, "source inventory capacity") + hashes = {} + for row in manifest["files"]: + if row["usage"] == "input": + path = root / row["path"] + require(path.stat().st_size <= 1048576, "source file capacity") + data = path.read_bytes() + digest = sha256(data).hexdigest() + require(digest == row["sha256"], "source hash: " + row["path"]) + hashes[row["path"]] = digest + require(len(hashes) == 3, "scientific source inventory") + for name in PACKAGE_FILES: + require((PACKAGE / name).stat().st_size <= 1048576, "package file capacity") + hashes["research/" + PACKAGE.name + "/" + name] = sha256((PACKAGE / name).read_bytes()).hexdigest() + return hashes + + +def main() -> None: + require(len(sys.argv) == 1, "verifier accepts no arguments") + hashes = source_hashes() + spaces = isotropic_spaces() + columns, rejected = literal_relations(spaces) + abstract = abstract_spectrum() + diagonal = diagonal_group_spectrum() + receipt = {"status": "PASS_CLIFFORD_SEVEN_ROTATION_GAP", "constants": constants(), + "isotropic_spaces": len(spaces), "point_incidence": 15, + "literal_endpoint_columns": columns, "word_rejections": rejected, + "abstract_root_spectrum": dict(sorted(abstract.items())), + "diagonal_group_spectrum": dict(sorted(diagonal.items())), + "semantic_controls": 2, "sha256": hashes} + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()