From 362a05a889ffc1ae923812f298a4186972be731e Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 08:02:27 +0000 Subject: [PATCH] feat(research): bound centre Gram stabilization by width ten --- .../centre-gram-width-stabilization/PROOF.md | 220 +++++++++ .../centre-gram-width-stabilization/README.md | 130 ++++++ .../SOURCES.json | 60 +++ .../centre-gram-width-stabilization/TASK.json | 113 +++++ .../VERIFY.json | 40 ++ .../centre-gram-width-stabilization/verify.py | 416 ++++++++++++++++++ 6 files changed, 979 insertions(+) create mode 100644 research/centre-gram-width-stabilization/PROOF.md create mode 100644 research/centre-gram-width-stabilization/README.md create mode 100644 research/centre-gram-width-stabilization/SOURCES.json create mode 100644 research/centre-gram-width-stabilization/TASK.json create mode 100644 research/centre-gram-width-stabilization/VERIFY.json create mode 100644 research/centre-gram-width-stabilization/verify.py diff --git a/research/centre-gram-width-stabilization/PROOF.md b/research/centre-gram-width-stabilization/PROOF.md new file mode 100644 index 0000000000..242980d397 --- /dev/null +++ b/research/centre-gram-width-stabilization/PROOF.md @@ -0,0 +1,220 @@ +# Width-independent annihilator and stabilization width for the doubled centre Gram + +Nick Petalas. Apache-2.0. + +This is a scoped written proof with a finite certificate. It answers the +uniform-bound half of open question 1 of Krzysztof Wojt's +`research/exact-one-slot-gram` ("the exact minimal polynomial of A_lambda for +lambda greater than one, or a uniform upper-degree bound"). It does not give the +width-two polynomial, prices no decoder and changes no selected bound. +Nick Petalas's merged #6302 (`research/uniform-centre-gram-annihilator`) already +proves a uniform degree bound `2^93` and qualitative eventual stabilization. +The additions here are the exact actual-group order `2^44`, the sharper degree +bound `2^47`, and the explicit stabilization width ten. The classical +Burnside-Brauer theorem is cited, not re-proved. + +## 1. Operator and notation + +All of this is inherited from `research/exact-one-slot-gram/PROOF.md`. Take the +112 pinned odd-weight labels q in F_2^9 and the integer columns r_q of the pinned +8-by-112 matrix R. For a label a in F_2^9 let X_a be the translation e_x -> e_(x+a) +and Z_a the character e_x -> (-1)^(a.x) e_x on C^512. Put + + H_q = (X_q + Z_q)/sqrt 2, Gamma_q = H_q tensor H_q, + A_lambda = (1/4) sum_q r_q r_q^T tensor Gamma_q^tensor(lambda), lambda >= 0, + +acting on R^8 tensor V^tensor(lambda), where V = R^512 tensor R^512 is the space +of real 512-by-512 matrices M with the Frobenius inner product, and Gamma_q acts +as M -> H_q M H_q (H_q is real symmetric). Write E_v = X_b Z_a for v = (a,b) in +F_2^18. The 2^18 matrices E_v are signed permutation matrices, orthogonal for the +Frobenius product with norm sqrt 512, so e_v = E_v/sqrt 512 is an orthonormal +basis of V. Let d_lambda be the degree of the minimal polynomial of A_lambda. + +Every A_lambda is real symmetric: r_q r_q^T is symmetric and Gamma_q^tensor(lambda) +is a tensor power of a symmetric matrix. So A_lambda is diagonalizable with real +eigenvalues and d_lambda is the number of distinct eigenvalues. The theorem below +does not use any property of R beyond it being a real matrix, except the numerical +value of the polynomial mu; the dimension counts use only the 112 labels. + +## 2. Statement + +Let G be the subgroup of O(V) generated by the 112 involutions Gamma_q. + +**Theorem.** + +1. G is a finite 2-group. For the pinned labels, |G| = 2^44 exactly. In general + |G| <= 2^(d_A + 18), where d_A is the F_2-dimension of span{q q^T}; here d_A = 36. +2. There is a real polynomial mu with simple real roots and degree at most + 8|G| <= 2^47 such that mu(A_lambda) = 0 for **every** lambda >= 0. It is + independent of lambda. +3. The minimal polynomial of A_lambda divides that of A_(lambda+1). So d_lambda + is nondecreasing. +4. For every lambda >= 10 the minimal polynomial of A_lambda equals mu. So + d_lambda = deg mu <= 2^47 for all lambda >= 10, and + d_1 = 881 < 1093 <= d_2 <= ... <= d_10 = d_11 = ... = deg mu. + +(The values 881 and 1093 are Wojt's theorem and Ali Romman's bound, cited.) + +So a uniform upper-degree bound exists, the sequence of exact degrees is +eventually constant, and the stable polynomial is the minimal polynomial of one +operator in the regular representation. The exact value of deg mu and the values +d_2, ..., d_9 are not determined here. + +## 3. The Bell identity + +For q of odd weight, X_q Z_q = -Z_q X_q, because Z_q X_q e_x = (-1)^(q.(x+q)) e_(x+q) +and q.q = 1. Hence H_q^2 = I, and Gamma_q is a symmetric orthogonal involution. +Expand 2 H_q E_(a,b) H_q = (X_q + Z_q) X_b Z_a (X_q + Z_q), using Z_a X_c = (-1)^(a.c) X_c Z_a: + + X_q X_b Z_a X_q = (-1)^(a.q) E_(a,b) + X_q X_b Z_a Z_q = E_(a+q,b+q) + Z_q X_b Z_a X_q = (-1)^(q.b + q.a + 1) E_(a+q,b+q) (q.q = 1) + Z_q X_b Z_a Z_q = (-1)^(q.b) E_(a,b). + +If q.(a+b) = 0 the E_(a+q,b+q) terms cancel and the other two add, giving +Gamma_q E_(a,b) = (-1)^(q.a) E_(a,b). If q.(a+b) = 1 the E_(a,b) terms cancel and +the others add, giving Gamma_q E_(a,b) = E_(a+q,b+q). This is the identity of +the one-slot package. `verify.py` re-checks it exactly, as integer 512-by-512 +matrices, on all 112 labels and 1,792 pairs (a,b) covering both cases. + +So each Gamma_q is a signed permutation of the basis e_v, namely +Gamma_q e_v = (-1)^(s) e_(sigma_q v) with sigma_q(v) = v + (q.(a+b)) t_q, where +t_q = (q,q) in F_2^18. Therefore G is a group of signed permutations of a finite +set and is finite. + +## 4. Structure of G (part 1) + +Define the symplectic form omega((a,b),(a',b')) = a.b' + a'.b on F_2^18 and +N_q(v) = omega(v, t_q) t_q = (q.(a+b)) t_q. Then sigma_q = I + N_q, and + + omega(t_q, t_q') = q.q' + q.q' = 0, + N_q N_q'(v) = omega(v, t_q') omega(t_q', t_q) t_q = 0. + +Hence the sigma_q commute, (I + N_q)(I + N_q') = I + N_q + N_q', and for a word +g = Gamma_(q_1) ... Gamma_(q_k) + + sigma_g = I + sum over S of N_q, S = labels occurring an odd number of times. + +Moreover N_q(a,b) = (M c, M c) with M = q q^T and c = a+b, so q -> N_q is injective +on matrices M and the group A = {sigma_g} has order 2^(d_A), d_A = dim span{q q^T} +inside Sym_9(F_2). `verify.py` computes d_A = 36 for the pinned labels. + +Let K be the kernel of g -> sigma_g. An element of K is a diagonal sign matrix: +g e_v = eps(v) e_v. Because g(MN) = g(M) g(N) for g a conjugation by an orthogonal +matrix, and E_v E_w = (-1)^(a.b') E_(v+w), the sign function is multiplicative: +eps(v+w) = eps(v) eps(w) (**). So eps(v) = (-1)^omega(s,v) for a unique s in F_2^18, +and K embeds in F_2^18. Thus |G| = |A||K| <= 2^(d_A + 18). + +For the exact order: choose generators whose N_q form an F_2-basis of span{N_q}. +Modulo the normal subgroup N generated by the commutators of the 112 generators +and by the words expressing each dependent generator through the chosen ones, G +is generated by commuting involutions, so |G/N| <= 2^(d_A). Since G/K = A has order +2^(d_A) and N is contained in K, N = K. Each sigma_q preserves omega: the two +cross terms in omega(v+omega(v,t_q)t_q, w+omega(w,t_q)t_q) cancel, and +omega(t_q,t_q)=0. Hence every sigma_g is symplectic. A conjugate of D_s by g +is D_(sigma_g s), so +K is the F_2-span of the orbit of the sign vectors of those commutators and relation +words under the maps s -> s + omega(s,t_q) t_q. `verify.py` computes that span. +Its dimension is d_K = 8, so |G| = 2^(36+8) = 2^44. On two small groups +(n = 3 with labels 1,2,4,7 and n = 4 with labels 1,7,14) the same computation is +compared with full enumeration of G, with equal kernels. + +## 5. The universal annihilator (parts 2 and 3) + +Let A = M_8(R) tensor R[G] and x = sum_q (r_q r_q^T / 4) tensor [Gamma_q], where +[Gamma_q] is the group element Gamma_q of G. For each lambda the map + + Phi_lambda(M tensor [g]) = M tensor g^tensor(lambda) + +is an algebra homomorphism A -> End(R^8 tensor V^tensor(lambda)), because +g -> g^tensor(lambda) is a representation of G. By definition Phi_lambda(x) = A_lambda. +So every polynomial that annihilates x in A annihilates every A_lambda. + +A is finite dimensional, so x has a minimal polynomial mu over R. A acts +faithfully on R^8 tensor R[G] (M tensor [g] -> M tensor L_g, with L_g the left +regular permutation matrix), and in that representation x is + + A_reg = sum_q (r_q r_q^T / 4) tensor L_(Gamma_q), + +a real symmetric matrix of size 8|G|: each L_g is orthogonal, and L_(Gamma_q) is +symmetric because Gamma_q^2 = I. So mu is the product of (t - theta) over the +distinct eigenvalues theta of A_reg: simple real roots, degree at most 8|G| = 2^47. +For the pinned integer R, A_reg is rational, so its minimal polynomial mu has +rational coefficients, by invariance of the rank of its rational matrix powers +under extension from Q to R. Thus the sharper bound also holds over Q. +This proves part 2. + +Part 3: u = e_0 = I/sqrt 512 is fixed by every Gamma_q, since Gamma_q I = H_q^2 = I. +For xi in R^8 tensor V^tensor(lambda), A_(lambda+1)(xi tensor u) = (A_lambda xi) tensor u. +So R^8 tensor V^tensor(lambda) tensor u is A_(lambda+1)-invariant and A_(lambda+1) +acts on it as A_lambda (this is the embedding recorded in the one-slot package). +Thus the spectrum of A_lambda lies in that of A_(lambda+1), and for symmetric +matrices the minimal polynomial is the product over the distinct eigenvalues. + +## 6. Trace values and stabilization (part 4) + +**Lemma 2.** For g in G the trace of g on V is 0 or 2^(18-r) for some 0 <= r <= 9. + +Proof. By section 3, g = Ad_U for an orthogonal U and g e_v = eps_g(v) e_(sigma_g v) +with eps_g(v) = +-1, where sigma_g = I + sum over S of N_q. Its fixed labels form +F = ker(sigma_g - I) = ker(sum over S of N_q) = {(a,b): M_S (a+b) = 0}, with +M_S = sum over S of q q^T, a symmetric 9-by-9 matrix over F_2. So |F| = 2^9 |ker M_S| = 2^(18 - rank M_S) and +rank M_S <= 9. For v, w in F the same argument as (**) (g is multiplicative, and +E_v E_w = +-E_(v+w) with v+w in F) shows eps_g(v+w) = eps_g(v) eps_g(w). So eps_g +restricted to F is a homomorphism F -> {+-1}. The trace is the sum of eps_g(v) +over v in F: |F| if the homomorphism is trivial, 0 otherwise. QED + +The character of V on G therefore takes at most 1 + 10 = 11 distinct values: +0 and 2^9, 2^10, ..., 2^18. `verify.py` checks the lemma, with every element, on +the two enumerated groups. + +V is a faithful G-module (G is a group of matrices on V). By the Burnside-Brauer +theorem (Isaacs, Character Theory of Finite Groups, Theorem 4.3; see also +[Steinberg's statement](https://arxiv.org/html/1409.7632v2#S1)), if a faithful +character takes m distinct values then every irreducible character of G is a +constituent of V^tensor(j) for some 0 <= j <= m-1. Here m <= 11, so every +irreducible occurs in V^tensor(j) for some j <= 10. Since V^tensor(j) embeds in +V^tensor(j+1) as a G-module (tensor with u), every irreducible occurs in +V^tensor(lambda) for every lambda >= 10. + +Now complexify. Decompose V_C^tensor(lambda) = sum over irreducible pi of +pi^(n_pi(lambda)). Then A_lambda is isomorphic to the direct sum of the +operators x_pi = sum_q (r_q r_q^T/4) tensor pi(Gamma_q), taken n_pi(lambda) times, +over the pi with n_pi(lambda) > 0. The regular representation contains every +irreducible pi with multiplicity dim(pi), so A_reg is isomorphic to the direct +sum of the same x_pi over all pi, each repeated dim(pi) times. For lambda >= 10 +every pi has n_pi(lambda) > 0, so A_lambda and A_reg have +the same set of distinct eigenvalues. Both are real symmetric, so their minimal +polynomials are the products over those sets and coincide: minpoly(A_lambda) = mu. +This is part 4. + +## 7. What is and is not proved + +- Proved here, in writing: parts 2, 3 and 4, given the Bell identity (derived in + section 3 and checked) and the Burnside-Brauer theorem (cited). +- Finite certificate: d_A = 36, d_K = 8, |G| = 2^44, the Bell identity on all + labels over 1,792 sampled pairs, and the group lemmas on two exactly enumerated + groups, with four rejecting controls. +- Not proved: the value of deg mu, the values d_2, ..., d_9, any improvement of + the lower bound 1093, and any statement about R beyond A_lambda being real + symmetric. The bound 2^47 is not a useful estimate; it only shows the degree + is finite and independent of the width. +- Nothing here prices a scalar-polynomial decoder, a physical source access, or + any native cost. No selected bound, supplier or frontier changes. +- No independent human or proof-kernel review is claimed. + +## 8. Credit + +Krzysztof Wojt's `research/exact-one-slot-gram` (#5168) defines A_lambda, derives +the Bell identity and the six-representative reduction, proves d_1 = 881 and +records the embedding of A_1 into every width. Ali Romman's +`research/equal-bell-two-slot-spectrum` (#5382) gives the equal-label spectrum and +the bound 1093 at every width at least two. The pinned query and its labels come +from Ali Romman's #4958 and #4720; Nick Petalas's #5120 is the degree-410 bound; +the doubled representation is #1719. The finite-group-algebra and +Burnside-Brauer viewpoint was already used in `research/clifford-tensor-gram` +for a different operator; that package, and the classical theorem of Burnside and +Brauer, receive credit for the method. Nick Petalas's #6302 already proves the +uniform annihilator and qualitative stabilization for this same operator; +the exact actual-group order, sharper degree bound and width-ten guarantee +are the contributions here. diff --git a/research/centre-gram-width-stabilization/README.md b/research/centre-gram-width-stabilization/README.md new file mode 100644 index 0000000000..b8aac4249f --- /dev/null +++ b/research/centre-gram-width-stabilization/README.md @@ -0,0 +1,130 @@ +# The doubled centre Gram stabilizes by tensor width ten + +**Scoped written proof with a finite certificate. No κ, no supplier admission.** + +The pinned one-slot doubled centre Gram `A_1` of +[`research/exact-one-slot-gram`](../exact-one-slot-gram/README.md) has a family +`A_lambda = (1/4) sum_q r_q r_q^T tensor Gamma_q^tensor(lambda)` of higher +tensor widths. Open question 1 of that package asks for the exact minimal +polynomial at `lambda > 1`, "or is there a uniform upper-degree bound?" +Nick Petalas's merged [#6302](https://github.com/CrocSwap/integer-mult-bounds/pull/6302) +already proves a uniform degree bound `2^93` and eventual stabilization, without +a stabilization width. This package sharpens the degree bound to `2^47`, computes +the actual generated-group order, and proves stabilization by width ten. + +**Theorem** (written proof in [PROOF.md](PROOF.md)). Let `G` be the group +generated by the 112 involutions `Gamma_q`, acting on the 2^18 Pauli labels by +signed permutations. + +1. `G` is a finite 2-group of order exactly `2^44`: its image on labels has order + `2^36` and its kernel has order `2^8`. +2. One real polynomial `mu` with simple real roots and degree at most + `8|G| = 2^47` annihilates `A_lambda` for **every** `lambda >= 0`. +3. The degree `d_lambda` of the minimal polynomial of `A_lambda` is nondecreasing. +4. For every `lambda >= 10` the minimal polynomial of `A_lambda` equals `mu`. + +Thus `881 = d_1 < 1093 <= d_2 <= ... <= d_10 = d_11 = ... = deg mu <= 2^47` +(881 is Krzysztof Wojt's theorem and 1093 is Ali Romman's bound, both cited). +The bound `2^47` is not a useful estimate. It shows only that the degree is +finite and independent of the width, and that the stable polynomial is the +minimal polynomial of one operator in the regular representation of `G`. + +**Method.** Every `A_lambda` is the image of one fixed element +`x = sum_q (r_q r_q^T/4) tensor [Gamma_q]` of `M_8(R) tensor R[G]` under +`id tensor rho^tensor(lambda)`. That gives the universal annihilator. The common +fixed vector `I/sqrt 512` embeds `A_lambda` in `A_(lambda+1)`, which gives +monotonicity. For stabilization, every element of `G` has trace 0 or `2^(18-r)` +with `r <= 9` (the sign function is additive on the fixed labels), so the +character of `V` takes at most 11 values, and the classical Burnside-Brauer +theorem puts every irreducible of `G` inside `V^tensor(10)`. + +## Claim types, kept distinct + +- **Scoped written proof:** parts 2, 3 and 4, given the Bell identity (derived in + PROOF.md section 3) and the Burnside-Brauer theorem (cited, not re-proved). +- **Finite certificate:** `d_A = 36`, `d_K = 8`, hence `|G| = 2^44`; the Bell + identity checked exactly as integer 512-by-512 matrices on all 112 labels and + 1,792 pairs; the trace lemma and the order formula on two exactly enumerated + groups; four rejecting controls. +- **Not claimed:** the value of `deg mu`, the values `d_2, ..., d_9`, any + improvement of the bound 1093, a complete multiplication theorem, or any + property of a physical decoder. + +## Reproduce + +From the repository root, standard library only: + +```sh +python3.12 -I -W error -B research/centre-gram-width-stabilization/verify.py +python3.12 -I -O -W error -B research/centre-gram-width-stabilization/verify.py +python3.12 -B scripts/research_package.py --package research/centre-gram-width-stabilization +``` + +Each run takes a few seconds. The marker is +`PASS_CENTRE_GRAM_WIDTH_STABILIZATION`. The printed JSON lists `d_A`, `d_K`, the +group order, the number of possible trace values and the two toy groups. The +pinned query is `INTERFACE.json` with SHA256 +`5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3`. + +## Limitations + +- The stabilization width 10 is an upper bound from counting possible trace + values. The true width may be smaller. +- The proof gives no information about which irreducibles of `G` occur in + `V tensor V`, so it does not determine `d_2`. +- `mu` depends on the matrix `R`; the existence and the degree bound use only the + 112 labels. The theorem holds for any real 8-by-112 matrix in place of `R`. +- No independent human or proof-kernel review is claimed. + +## Open next questions + +1. **Which irreducibles of `G` occur at widths 2 through 9, and what are `d_2`, + ..., `d_9`?** This is the unequal outer-label question left open by + `research/equal-bell-two-slot-spectrum`, restated as a finite + representation-theory problem. First step: use the exact normal series + `K` (dimension 8) by `A` (dimension 36), compute the orbits of `A` on the 256 + characters of `K`, and list the stabilizers. Blocker: the projective + irreducibles over the stabilizers can be large, and each needs the exact + spectrum of an operator of size `8 dim(pi)`. +2. **Can the stabilization width be lowered from 10?** First step: find which + ranks of `M_S = sum over S of q q^T` occur in the 36-dimensional span, and + which trace values `2^(18-r)` occur on `G`; each value that never occurs lowers + the Burnside-Brauer width. Blocker: the span has `2^36` elements, so this needs + an orbit or invariant argument rather than enumeration. +3. **Can `deg mu` be bounded far below `2^47`, or lower-bounded above 1093?** First + step: build one small irreducible of `G` from a character of `K` with a large + stabilizer and compute the exact spectrum of its `x_pi`, to find eigenvalues + outside the 1093 already known. Blocker: the size of `pi` and the cost of an + exact characteristic polynomial. + +## Credit + +This scoped proof was produced by Nick Petalas. Apache-2.0. + +Krzysztof Wojt's `research/exact-one-slot-gram` (#5168) defines `A_lambda`, +derives the Bell identity and proves `d_1 = 881`. Ali Romman's +`research/equal-bell-two-slot-spectrum` (#5382) gives the equal-label spectrum and +the bound 1093 at every width at least two; the pinned query comes from Ali +Romman's #4958 and #4720. Nick Petalas's #5120 is the degree-410 bound, and the +doubled representation is #1719. The finite-group-algebra and Burnside-Brauer +viewpoint was already in use in `research/clifford-tensor-gram` for a different +operator. Nick Petalas's `research/uniform-centre-gram-annihilator` (#6302) +already supplies the uniform existence theorem and qualitative stabilization +for this operator, using an enclosing group of order `2^90`. The new results +here concern the smaller actual group and a quantitative stabilization width. +The classical tensor-generation theorem is due to Burnside and Brauer. + +## Verifier constraints + +The verifier reads the fixed source files and writes nothing. It uses no +recursion, subprocesses or network access. The actual calculation has 112 +generators, at most 6,292 relation and commutator words, and an 18-dimensional +kernel module. Its closure queue processes at most `6292 + 18*112` vectors. +Full group enumeration is restricted to the two toy fixtures, with at most +2,048 signed permutations on at most 256 labels. All functions are below +60 lines. Explicit exceptions preserve acceptance checks under `-O`. + +Power-of-ten rule 3 deviation: CPython allocates integers and containers during +checking; the fixed domains above bound their live sizes. Rule 9 deviation: +the rejection helper invokes two fixed local lambdas. Both registered modes +use `-W error`. No independent static analyzer or proof-kernel check is claimed. diff --git a/research/centre-gram-width-stabilization/SOURCES.json b/research/centre-gram-width-stabilization/SOURCES.json new file mode 100644 index 0000000000..c81509adef --- /dev/null +++ b/research/centre-gram-width-stabilization/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/centre-polynomial-cache-limits/frozen/work/centre-encoding-campaign-20261014/lanes/circuit-interface/INTERFACE.json", + "usage": "input", + "git_blob": "4201e9a04c12273b919e2cae60a6b6482c8150f3", + "sha256": "5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3" + }, + { + "path": "research/clifford-tensor-gram/PROOF.md", + "usage": "input", + "git_blob": "cb8b75a33d0a623cfa64c32aaf7878d2a5816397", + "sha256": "f79c723a869a480c9959038f59db206359e4b6768e9839aff25b3921beaec84a" + }, + { + "path": "research/equal-bell-two-slot-spectrum/README.md", + "usage": "input", + "git_blob": "3e9e574cb86729bec406db9073610c340270ab05", + "sha256": "e20b09c62eda072e2db18d104b2edeb89083549557753c9cfe460809e44ec5a7" + }, + { + "path": "research/exact-one-slot-gram/PROOF.md", + "usage": "input", + "git_blob": "91854803c13d19d7962aafedf37aca0004827514", + "sha256": "30ccfa6d6623313a3c73c7107b7d9c3872eeffc07d2062e7e9b797162585e9b4" + }, + { + "path": "research/exact-one-slot-gram/TASK.json", + "usage": "input", + "git_blob": "61ccba17226d311b800516701e9f9ac57d6a5f24", + "sha256": "b9ec4b2e8e3efd832d5c23a3159a10ad0d38fcedc68f9d14b37163f38fdd4018" + }, + { + "path": "research/uniform-centre-gram-annihilator/README.md", + "usage": "provenance", + "git_blob": "8d88ecd138dff5ae724bfa9b5fc82ecf38a952e5", + "sha256": "a4d32a5e0bbf29122280030ae75be71843e47fc331b523fb7ede4b2e042cb529" + }, + { + "path": "research/uniform-centre-gram-annihilator/PROOF.md", + "usage": "provenance", + "git_blob": "6bd2a8f37af7e8c665086387eca0fcf4c300b218", + "sha256": "3d0873737dd69c1808d4054d558a3de5178371d3fe1822dc955503287f74d0e0" + } + ] +} diff --git a/research/centre-gram-width-stabilization/TASK.json b/research/centre-gram-width-stabilization/TASK.json new file mode 100644 index 0000000000..2f33c54aad --- /dev/null +++ b/research/centre-gram-width-stabilization/TASK.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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": "Compute the actual 112-generator doubled Bell group of order 2^44, sharpen the already known uniform degree bound from 2^93 to 2^47, and prove that the minimal polynomial is constant from width 10 on. The exact width-two polynomial and stable degree remain undetermined.", + "scope_change_reason": "The card asks for a formal caller binding. This is a written finite-group side result on the operator in Krzysztof Wojt PR5168. Merged PR6302 already proves uniform existence and qualitative eventual stabilization. The new scope is its quantitative sharpening by an independently derived exact group-order calculation and a trace-value argument; no Lean binding is added.", + "bottleneck_link": "Side result. It sharpens the known uniform degree bound and gives a finite width by which the scalar-polynomial decoder algebra reaches its stable spectrum. It prices no decoder, no source access and no restoration, and it does not change kappa.", + "budget_minutes": 60, + "stop_rule": "Stop at a proved universal annihilator, monotone degree and explicit stabilization width, or at a precise gap; do not search for the width-two polynomial.", + "outcome": "completed", + "evidence": "PROOF.md (written proof; Burnside-Brauer cited). verify.py (standard library): source binding, Bell identity on all 112 labels, d_A = 36, d_K = 8, |G| = 2^44, two exactly enumerated groups, four rejecting controls. Outcome: scoped written proof with a finite certificate; no kappa, no supplier admission, no selected-frontier change.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which irreducibles of G occur in V tensor V through V tensor(9), and what are d_2, ..., d_9?", + "why_it_matters": "It is the finite form of the unequal outer-label classification left open by equal-bell-two-slot-spectrum and fixes the exact width-two polynomial.", + "first_step": "Use the normal series K (dimension 8) by A (dimension 36), compute the A-orbits on the 256 characters of K and the stabilizers.", + "blocked_by": "Projective irreducibles over the stabilizers can be large and each needs the exact spectrum of an operator of size 8 dim(pi)." + }, + { + "question": "Can the stabilization width 10 be lowered?", + "why_it_matters": "A smaller width leaves fewer intermediate degrees d_2, ..., d_9 to determine.", + "first_step": "Find which ranks of M_S = sum of q q^T occur in the 36-dimensional span and which trace values 2^(18-r) occur on G.", + "blocked_by": "The span has 2^36 elements, so an orbit or invariant argument is needed instead of enumeration." + }, + { + "question": "Can deg mu be bounded far below 2^47, or the lower bound 1093 raised?", + "why_it_matters": "The present uniform bound only shows finiteness; a useful value would price the best scalar-polynomial decoder at every width.", + "first_step": "Build one small irreducible of G from a character of K with a large stabilizer and compute the exact spectrum of its x_pi.", + "blocked_by": "The dimension of pi and the cost of an exact characteristic polynomial." + } + ], + "overlap_checkpoint": { + "checked_at_utc": "2026-11-11T08:00:34.684168+00:00", + "canonical_main": "e54523517d0f03e58352e647c403a5af3e525a57", + "prior_uniform_bound_pr": 6302, + "delta": "Exact actual-group order, degree at most 2^47, and stabilization by width ten. Uniform existence and qualitative stabilization were already known." + } +} diff --git a/research/centre-gram-width-stabilization/VERIFY.json b/research/centre-gram-width-stabilization/VERIFY.json new file mode 100644 index 0000000000..75b924f74a --- /dev/null +++ b/research/centre-gram-width-stabilization/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/centre-polynomial-cache-limits/frozen/work/centre-encoding-campaign-20261014/lanes/circuit-interface/INTERFACE.json", + "research/clifford-tensor-gram/PROOF.md", + "research/equal-bell-two-slot-spectrum/README.md", + "research/exact-one-slot-gram/PROOF.md", + "research/exact-one-slot-gram/TASK.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source binding, exact Bell identity on all 112 labels, d_A, d_K and the group order, trace lemma and order formula on two enumerated groups, four controls" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same under optimization; acceptance uses explicit checks so -O skips nothing" + } + ] +} diff --git a/research/centre-gram-width-stabilization/verify.py b/research/centre-gram-width-stabilization/verify.py new file mode 100644 index 0000000000..53de04e529 --- /dev/null +++ b/research/centre-gram-width-stabilization/verify.py @@ -0,0 +1,416 @@ +#!/usr/bin/env python3 +"""Finite checks behind the width-independence theorem for the doubled centre Gram. + +Nick Petalas. Apache-2.0. Standard library only; every acceptance test is an +explicit `require`, so `python -O` skips nothing. + +PROOF.md proves, for the operators A_lambda of research/exact-one-slot-gram, +that one polynomial annihilates every width, that the minimal-polynomial degree +is nondecreasing, and that the minimal polynomial is constant from width 10 on. +The proof needs four finite facts, which this script checks: + + 1. Source binding: the pinned 8-by-112 query has 112 distinct odd-weight labels. + 2. The Bell identity Gamma_q E_(a,b) = +-E_(a',b'), exactly, on every label. + 3. The F_2-dimension d_A of span{q q^T}, which bounds the label action of G. + 4. On exactly enumerated small groups of the same kind: |G| = |A||K|, the trace + values lie in {0} U {2^(2n-r)}, and the sign function is additive on every + fixed-point space (the lemma behind the trace values). + +It does not compute the width-two or the stable minimal polynomial and says +nothing about physical cost. +""" +import hashlib +import json +import sys +from pathlib import Path + +PKG = Path(__file__).resolve().parent +ROOT = PKG.parents[1] +INTERFACE = ROOT / ("research/centre-polynomial-cache-limits/frozen/work/" + "centre-encoding-campaign-20261014/lanes/circuit-interface/INTERFACE.json") +INTERFACE_SHA256 = "5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3" +ONE_SLOT_PROOF = ROOT / "research/exact-one-slot-gram/PROOF.md" +OPERATOR_TEXT = "A_lambda = (1/4) sum_q r_q r_q^T tensor Gamma_q^tensor(lambda)" +N_BITS = 9 +POINTS = 512 +MARKER = "PASS_CENTRE_GRAM_WIDTH_STABILIZATION" + + +class CheckFailed(Exception): + pass + + +def require(condition, message): + if not condition: + raise CheckFailed(message) + + +def parity(x): + return bin(x).count("1") & 1 + + +def f2_rank(rows): + basis = {} + for row in rows: + while row: + top = row.bit_length() - 1 + if top in basis: + row ^= basis[top] + else: + basis[top] = row + break + return len(basis) + + +# ---------------------------------------------------------------- 1. source binding + +def load_model(): + raw = INTERFACE.read_bytes() + require(hashlib.sha256(raw).hexdigest() == INTERFACE_SHA256, "INTERFACE.json bytes differ from the pin") + data = json.loads(raw) + ports = data["ports"] + require(len(ports) == 112 and len(set(ports)) == 112, "expected 112 distinct labels") + require(all(isinstance(q, int) and 0 < q < POINTS and parity(q) == 1 for q in ports), + "every label must be an odd-weight nonzero 9-bit integer") + rows = data["R"] + require(len(rows) == 8, "R must have 8 rows") + columns = [dict() for _ in ports] + for i, row in enumerate(rows): + for key, value in row.items(): + j = int(key) + require(0 <= j < 112 and value in ("1", "-1"), "R entries must be +-1 on columns 0..111") + columns[j][i] = int(value) + require(all(len(col) == 4 for col in columns), "every column of R must have four +-1 entries") + for i in range(8): + for k in range(8): + gram = sum(columns[j].get(i, 0) * columns[j].get(k, 0) for j in range(112)) + require(gram == (56 if i == k else 0), "R R^T must equal 56 I") + text = ONE_SLOT_PROOF.read_text(encoding="utf-8") + require(OPERATOR_TEXT in text.replace("\n", " ").replace(" ", " ") or + "A_lambda = (1/4) sum_q r_q r_q^T tensor Gamma_q^tensor(lambda)" in text, + "operator definition not found in the pinned one-slot proof") + quoted = { + ROOT / "research/exact-one-slot-gram/TASK.json": "uniform upper-degree bound", + ROOT / "research/equal-bell-two-slot-spectrum/README.md": "at least\n1093", + ROOT / "research/clifford-tensor-gram/PROOF.md": "Burnside-Brauer", + } + for path, phrase in quoted.items(): + require(phrase in path.read_text(encoding="utf-8"), "pinned source no longer states: " + phrase) + return ports + + +# ---------------------------------------------------------------- 2. Bell identity + +def sandwich_column(q, a, b, x): + """Column x of (X_q + Z_q) E_(a,b) (X_q + Z_q), with E_(a,b) = X_b Z_a, as {row: integer}.""" + out = {} + for y, s1 in ((x ^ q, 1), (x, -1 if parity(q & x) else 1)): + z, s2 = y ^ b, s1 * (-1 if parity(a & y) else 1) + for w, s3 in ((z ^ q, s2), (z, s2 * (-1 if parity(q & z) else 1))): + out[w] = out.get(w, 0) + s3 + return {row: value for row, value in out.items() if value} + + +def predicted_column(q, a, b, x, flip=False): + """Column x of 2 * Gamma_q(E_(a,b)) by the claimed signed permutation; `flip` is a mutant.""" + if parity(q & (a ^ b)) == 0: + a2, b2, sign = a, b, (-1 if parity(q & a) else 1) + if flip: + sign = -sign + else: + a2, b2, sign = a ^ q, b ^ q, 1 + return {x ^ b2: 2 * sign * (-1 if parity(a2 & x) else 1)} + + +def bell_identity_holds(q, a, b, flip=False): + return all(sandwich_column(q, a, b, x) == predicted_column(q, a, b, x, flip) for x in range(POINTS)) + + +def sample_pairs(q, count): + state = (q * 2654435761 + 12345) & 0xFFFFFFFF + pairs = [(0, 0), (POINTS - 1, 0), (0, POINTS - 1), (q, 0), (0, q), (q, q), (1, q ^ 1), (q ^ 0x155, 0x0AA)] + while len(pairs) < count: + state = (state * 1103515245 + 12345) & 0x7FFFFFFF + a = state % POINTS + state = (state * 1103515245 + 12345) & 0x7FFFFFFF + pairs.append((a, state % POINTS)) + return pairs + + +def check_bell_identity(ports): + zero_cases = one_cases = 0 + for q in ports: + for a, b in sample_pairs(q, 16): + require(bell_identity_holds(q, a, b), "Bell identity fails at q=%d a=%d b=%d" % (q, a, b)) + if parity(q & (a ^ b)): + one_cases += 1 + else: + zero_cases += 1 + require(zero_cases > 0 and one_cases > 0, "both Bell cases must be exercised") + return zero_cases, one_cases + + +# ---------------------------------------------------------------- 3. label-group dimension + +def outer_product_bits(q, n=N_BITS): + bits = k = 0 + for i in range(n): + for j in range(i, n): + if (q >> i) & 1 and (q >> j) & 1: + bits |= 1 << k + k += 1 + return bits + + +def label_dimension(labels, n=N_BITS): + return f2_rank([outer_product_bits(q, n) for q in labels]) + + +def symmetric_rank(labels, n): + """F_2 rank of M_S = sum of q q^T over the given labels.""" + rows = [0] * n + for q in labels: + for i in range(n): + if (q >> i) & 1: + rows[i] ^= q + return f2_rank(rows) + + +# ---------------------------------------------------------------- 4. exactly enumerated groups + +def generator(n, q): + """Gamma_q as a signed permutation of the 4^n Pauli labels v = (a << n) | b. + + Entry v is (image << 1) | s, where s = 1 means the sign -1.""" + mask = (1 << n) - 1 + image = [] + for v in range(1 << (2 * n)): + a, b = v >> n, v & mask + if parity(q & (a ^ b)) == 0: + image.append((v << 1) | parity(q & a)) + else: + image.append((((a ^ q) << n) | (b ^ q)) << 1) + return tuple(image) + + +def compose(g, h): + """g after h.""" + return tuple(g[hv >> 1] ^ (hv & 1) for hv in h) + + +def check_element(g, n, labels, parity_set): + """Lemma behind the trace values; returns the trace and |Fix|.""" + fixed = [v for v in range(1 << (2 * n)) if (g[v] >> 1) == v] + basis = {} + for v in fixed: + vec, sign = v, g[v] & 1 + while vec: + top = vec.bit_length() - 1 + if top in basis: + bvec, bsign = basis[top] + vec ^= bvec + sign ^= bsign + else: + basis[top] = (vec, sign) + break + else: + require(sign == 0, "sign function is not additive on the fixed labels") + require(len(fixed) == 1 << len(basis), "fixed labels do not form a subspace") + trace = sum(-1 if g[v] & 1 else 1 for v in fixed) + trivial = all(sign == 0 for _, sign in basis.values()) + require(trace == (len(fixed) if trivial else 0), "trace is neither |Fix| nor 0") + chosen = [labels[i] for i in range(len(labels)) if (parity_set >> i) & 1] + require(len(fixed) == 1 << (2 * n - symmetric_rank(chosen, n)), "|Fix| differs from 2^(2n - rank M_S)") + return trace, len(fixed) + + +def check_group(n, labels, generators=None): + require(n in (3, 4) and 1 <= len(labels) <= 4, "enumeration is restricted to the two small dimensions") + d_a = label_dimension(labels, n) + cap = 1 << (d_a + 2 * n) + gens = generators or [generator(n, q) for q in labels] + identity = tuple(v << 1 for v in range(1 << (2 * n))) + seen = {identity: 0} + frontier = [identity] + for _ in range(cap): + if not frontier: + break + nxt = [] + for g in frontier: + for index, gen in enumerate(gens): + h = compose(gen, g) + if h not in seen: + require(len(seen) < cap, "group exceeds the proved order bound 2^(d_A + 2n)") + seen[h] = seen[g] ^ (1 << index) + nxt.append(h) + frontier = nxt + require(not frontier, "group enumeration exhausted its finite bound") + traces = set() + labelings = {} + for g, parity_set in seen.items(): + trace, _ = check_element(g, n, labels, parity_set) # Fixed-space size is checked inside the callee. + traces.add(trace) + labelings.setdefault(tuple(v >> 1 for v in g), []).append(g) + kernel = labelings.get(tuple(range(1 << (2 * n))), []) + require(len(seen) == len(labelings) * len(kernel), "|G| differs from |A||K|") + require(len(kernel) <= 1 << (2 * n), "kernel exceeds 2^(2n)") + require(len(labelings) == 1 << d_a, "label image does not have order 2^d_A") + for gen_a in gens: + for gen_b in gens: + require(tuple(x >> 1 for x in compose(gen_a, gen_b)) == tuple(x >> 1 for x in compose(gen_b, gen_a)), + "label actions of the generators do not commute") + allowed = {0} | {1 << (2 * n - r) for r in range(n + 1)} + require(traces <= allowed, "trace value outside {0} U {2^(2n-r)}") + if generators is None: + require(1 << kernel_dimension(n, labels) == len(kernel), "kernel module differs from the enumerated kernel") + return {"order": len(seen), "label_image": len(labelings), "kernel": len(kernel), "d_A": d_a, + "trace_values": sorted(traces), "width_bound": len(traces) - 1} + + +# ---------------------------------------------------------------- exact kernel dimension + +def apply_word(n, word, v): + """Apply Gamma_{q_1} ... Gamma_{q_k} (rightmost letter first) to the label v; return (image, sign bit).""" + mask = (1 << n) - 1 + sign = 0 + for q in reversed(word): + a, b = v >> n, v & mask + if parity(q & (a ^ b)) == 0: + sign ^= parity(q & a) + else: + v = ((a ^ q) << n) | (b ^ q) + return v, sign + + +def omega(n, s, v): + mask = (1 << n) - 1 + return parity((s >> n) & (v & mask)) ^ parity((s & mask) & (v >> n)) + + +def sign_vector(n, word): + """The vector s with word = diagonal sign matrix (-1)^omega(s, v); the word must act trivially on labels.""" + s = 0 + for i in range(n): + v = (1 << i) << n + image, sign = apply_word(n, word, v) + require(image == v, "word does not act trivially on labels") + s |= sign << i + v = 1 << i + image, sign = apply_word(n, word, v) + require(image == v, "word does not act trivially on labels") + s |= sign << (n + i) + state = (len(word) * 40503 + 7) & 0xFFFFFFFF + for _ in range(32): + state = (state * 1103515245 + 12345) & 0x7FFFFFFF + v = state % (1 << (2 * n)) + image, sign = apply_word(n, word, v) + require(image == v and sign == omega(n, s, v), "sign function of a trivial-label word is not linear") + return s + + +def kernel_dimension(n, labels): + """dim_F2 of K = ker(G -> label action), as the A-module generated by commutators and relation words. + + G/K is generated by the images of an F_2-independent subfamily of the generators (their label + actions I + N_q add), so K is the normal closure of the commutators of generators together with the + words that express each dependent generator through the independent ones.""" + require(1 <= n <= N_BITS and 1 <= len(labels) <= 112, "kernel model exceeds the fixed dimensions") + require(len(set(labels)) == len(labels), "kernel labels must be distinct") + require(all(0 < q < 1 << n and parity(q) for q in labels), "kernel labels must be odd n-bit integers") + basis, relations = {}, [] + for j, q in enumerate(labels): + vec, combo = outer_product_bits(q, n), 1 << j + while vec: + top = vec.bit_length() - 1 + if top in basis: + vec ^= basis[top][0] + combo ^= basis[top][1] + else: + basis[top] = (vec, combo) + break + else: + relations.append([labels[i] for i in range(len(labels)) if (combo >> i) & 1]) + words = [[x, y, x, y] for x in labels for y in labels if x < y] + relations + queue = [sign_vector(n, word) for word in words] + span = {} + pair_masks = [(q << n) | q for q in labels] + for _ in range(len(words) + 2 * n * len(labels)): + if not queue: + break + u = queue.pop() + while u: + top = u.bit_length() - 1 + if top in span: + u ^= span[top] + else: + span[top] = u + require(len(span) <= 2 * n, "kernel span exceeds its ambient dimension") + for q, t in zip(labels, pair_masks): + queue.append(u ^ (t if parity(q & ((u >> n) ^ (u & ((1 << n) - 1)))) else 0)) + break + require(not queue, "kernel closure exhausted its finite bound") + return len(span) + + +def expect_failure(label, function): + try: + function() + except CheckFailed: + return + raise CheckFailed("control did not reject: " + label) + + +def run_controls(ports): + q_even = 3 + require(not all(bell_identity_holds(q_even, a, b) for a, b in sample_pairs(q_even, 8)), + "an even-weight label must break the Bell identity") + odd = ports[0] + require(not all(bell_identity_holds(odd, a, b, flip=True) for a, b in sample_pairs(odd, 8)), + "a sign-flipped prediction must be rejected") + n, labels = 3, [1, 2, 4, 7] + mutated = [generator(n, q) for q in labels] + broken = list(mutated[3]) + broken[5] ^= 1 + mutated[3] = tuple(broken) + expect_failure("one extra sign flip in a generator", lambda: check_group(n, labels, mutated)) + expect_failure("a translation that does not fix the zero Pauli label", + lambda: check_element(tuple(((v ^ 1) << 1) | (v & 1) for v in range(64)), 3, [1], 1)) + return 4 + + +def main(): + ports = load_model() + zero_cases, one_cases = check_bell_identity(ports) + d_a = label_dimension(ports) + require(1 <= d_a <= N_BITS * (N_BITS + 1) // 2, "d_A out of range") + d_k = kernel_dimension(N_BITS, ports) + require(0 <= d_k <= 2 * N_BITS, "kernel dimension out of range") + require((d_a, d_k) == (36, 8), "actual group dimensions differ from the theorem") + log_g = d_a + d_k + toys = [(3, [1, 2, 4, 7]), (4, [1, 7, 14])] + toy_rows = [] + for n, labels in toys: + toy_rows.append((n, labels, check_group(n, labels))) + controls = run_controls(ports) + trace_values = 1 + (N_BITS + 1) + print(json.dumps({ + "interface_sha256": INTERFACE_SHA256, + "labels": len(ports), + "bell_cases_checked": {"q.(a+b)=0": zero_cases, "q.(a+b)=1": one_cases}, + "d_A": d_a, + "d_K": d_k, + "log2_group_order": log_g, + "annihilator_degree_bound": "8 * 2^%d = 2^%d" % (log_g, log_g + 3), + "possible_trace_values": trace_values, + "stabilization_width": trace_values - 1, + "toy_groups": [{"n": n, "labels": labels, **row} for n, labels, row in toy_rows], + "controls_rejected": controls, + }, indent=1, sort_keys=True)) + print(MARKER) + + +if __name__ == "__main__": + try: + main() + except CheckFailed as error: + sys.exit("FAIL: " + str(error))