Prove doubled centre Gram stabilization by width ten (no κ)

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.

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.