Prove a uniform all-width annihilator for the doubled Gram (no κ)

research/uniform-centre-gram-annihilator/PROOF.md

@@ -0,0 +1,152 @@
+# One annihilator at every tensor width
+
+This scoped written proof was produced by Nick Petalas. The finite verifier
+corroborates the new algebraic formulas. It is not a proof-kernel certificate.
+
+## Statement and inherited operator
+
+Use the exact historical eight-by-112 integer query matrix R retained by
+Ali Romman's PR4958 and PR4720. Its columns are r_q, indexed by distinct
+odd nonzero q in F_2^9. For every positive integer f the doubled Gram is
+
+    A_f = (1/4) sum_q r_q r_q^T tensor Gamma_q^tensor(f).
+
+The root coefficient occurs once. Gamma_q is the doubled action of
+H_q = (X_q+Z_q)/sqrt(2). The Bell similarity and its exact signs are the
+credited premises in PR4958, PROOF.md section 1. In Bell coordinates,
+write c=a+b. Then
+
+    Gamma_q |c,a> = (-1)^[(1+q.c)(q.a)] |c,a+(q.c)q>.
+
+Dots and the exponent here are in F_2. In particular this action is a signed
+permutation, and it fixes |0,0>. The verifier authenticates the actual query
+and binds all its generators to the construction below. It does not rerun
+the predecessor's Bell embedding or spectral certificates.
+
+**Theorem.** There is one monic polynomial P in Q[x], independent of f,
+with degree at most 2^93, such that P(A_f)=0 for every integer f>=1.
+Consequently the scalar minimal-polynomial degrees are bounded uniformly,
+and the union of the spectra over all positive widths is finite.
+
+This answers the existence part of the uniform-upper-degree question in
+Krzysztof Wojt's PR5168. It gives neither the least degree nor the coefficients
+of a practical annihilator. PR5168's exact one-slot degree 881 and Ali
+Romman's PR5382 lower bound 1093 at widths at least two are cited results.
+They are compatible with this upper bound and are not recomputed here.
+
+## A finite enclosing group
+
+Work first with arbitrary n>=1. Let S be a symmetric n-by-n matrix over
+F_2, let d(S) be its diagonal as a column, and let h(c) be any squarefree
+Boolean polynomial of degree at most two with zero constant term. Define
+
+    T(S,h)|c,a> = (-1)^[(d(S)+Sc).a+h(c)] |c,a+Sc>.
+
+There are m=n(n+1)/2 independent entries of S. The polynomials h have
+n linear and n(n-1)/2 quadratic coefficients, also m in total. The normal
+forms therefore have 2^(2m)=2^[n(n+1)] parameter choices.
+
+These choices give distinct maps. The permutation recovers Sc for every c,
+hence recovers S. With S fixed, evaluate the sign at a=0 to recover h(c).
+Squarefree Boolean monomials are independent as functions: their linear
+coefficients are recovered at e_i and their quadratic coefficients at
+e_i+e_j after subtracting the two linear values. Thus the group below has
+exactly this many elements. This is the cardinality of an enclosing group,
+not a claim about the order of the subgroup generated by the actual ports.
+
+Put z_S(c)=d(S)+Sc. Applying the right map first gives
+
+    T(S,h) T(U,k) = T(S+U, h+k+z_S(c).Uc).                 (1)
+
+Indeed the right map contributes z_U(c).a+k(c). The left map contributes
+z_S(c).(a+Uc)+h(c). The terms multiplying a combine to z_(S+U)(c).a.
+The translation is a+(S+U)c. The remaining cross term has degree at most
+two and has zero constant term. Reducing c_i^2 to c_i preserves that form.
+
+The identity is T(0,0). The inverse, on either side, is
+
+    T(S,h)^-1 = T(S, h+z_S(c).Sc).                        (2)
+
+This also follows directly by applying the map twice. Associativity follows
+from composition of the actual signed permutations, and injectivity makes
+(1) a group law on the parameters. Call this finite group G_n.
+
+For each actual port q, take S=q q^T and h=0. Since d(S)=q and
+Sc=(q.c)q, its normal form is exactly Gamma_q. Thus all actual generators
+belong to G_9. The enclosing order is
+
+    |G_9| = 2^[9*10] = 2^90.                             (3)
+
+No quotient by scalar signs is taken. In particular h is essential.
+For example with n=2, S=diag(1,0), and U exchanging the two coordinates,
+the cross term is c_2+c_1 c_2. Discarding it changes the operator. Some
+enclosing maps have order four even though each actual port is an involution.
+
+## Matrix group algebra and a common polynomial
+
+Let Q[G_9] be the rational group algebra, with its actual group basis [g].
+Form the single element
+
+    B = sum_q r_q r_q^T [Gamma_q] in Mat_8(Q[G_9]).        (4)
+
+All coefficients are integers. Let L be its left regular action on
+Q^8 tensor Q[G_9]. This is an integer matrix of dimension
+
+    D = 8 |G_9| = 2^93.
+
+The matrix-algebra regular action is faithful. If an element acts as zero,
+apply it to every e_j tensor [identity]. These vectors recover every entry
+of every coefficient matrix, so the element itself is zero.
+
+Let p(t)=det(tI-L). Cayley-Hamilton gives p(L)=0. Faithfulness therefore
+gives p(B)=0 inside Mat_8(Q[G_9]). This is a monic integer polynomial of
+degree D. Its definition is finite and exact; no coefficients of this
+enormous determinant are claimed to have been generated.
+
+For each f>=1 the assignment
+
+    [g] -> g^tensor(f)
+
+extends linearly to a unital algebra homomorphism. This uses
+(gh)^tensor(f)=g^tensor(f) h^tensor(f). It does not send a sum to the
+tensor power of that sum. Extend the map entrywise to the matrix algebra.
+Equation (4) then maps to 4A_f. Thus
+
+    p(4A_f)=0 for every f>=1.
+
+Set P(x)=4^-D p(4x). It is monic and rational, is independent of f, and
+has degree D. This proves the theorem. The same similarity argument
+transfers the identity out of Bell coordinates.
+
+Every eigenvalue of every A_f is a root of P, so there are at most D
+distinct eigenvalues in their union. The common fixed vector |0,0>
+embeds A_f as an invariant restriction of A_(f+1). Therefore their spectra
+are nested, and eventually stabilize as sets. This argument supplies no
+useful stabilization width or exact stabilized spectrum.
+
+## Scope and verification
+
+This is a scoped algebraic existence proof. It is not a finite certificate
+of the huge characteristic polynomial, a new lower bound, a search failure,
+or a complete multiplication theorem. The 2^93 degree bound is deliberately
+coarse. It does not identify the actual generated subgroup, exploit the
+particular root coefficients, price a scalar-polynomial decoder, or provide
+an executable native implementation. All physical access, coefficient,
+precision, ownership, restoration, tape, compiler and supplier costs remain.
+
+The new verifier checks full normal-form injectivity at n=1,2,3 and every
+ordered enclosing-group product at n=1,2 by literal signed permutations.
+It checks the new cross term for all ordered actual-port generator pairs
+using Boolean interpolation and a separate monomial expansion. A separate
+small two-by-two matrix group-algebra example computes its regular
+characteristic polynomial, checks determinant values by rational elimination,
+and evaluates the same polynomial in three tensor representations. These
+finite calculations corroborate the written proof; they do not enumerate G_9.
+
+Classical ingredients are Boolean multilinear normal forms, the group
+algebra regular representation and Cayley-Hamilton. David Ganz's PR4885
+uses finite group-algebra annihilation for a different resonant channel.
+The contribution here is the explicit quadratic signed-translation envelope
+for this Bell action and its width-independent Gram consequence. No global
+literature priority is claimed. Independent human and formal proof-kernel
+review are unclaimed.

research/uniform-centre-gram-annihilator/README.md

@@ -0,0 +1,122 @@
+# A width-independent annihilator for the doubled centre Gram
+
+This scoped written proof was produced by Nick Petalas. For the historical
+actual 112-port query, there is one monic rational polynomial P such that
+
+    P(A_f)=0 for every positive tensor width f,
+    degree(P) <= 2^93.
+
+This answers the uniform-upper-degree existence question in Krzysztof
+Wojt's [PR5168](https://github.com/CrocSwap/integer-mult-bounds/pull/5168).
+The union of the spectra is finite and eventually stabilizes. The degree
+bound is coarse; this package does not materialize the polynomial or compute
+the least degree, stabilized spectrum or stabilization width. No new kappa
+or selected-frontier change is claimed.
+
+[PROOF.md](PROOF.md) puts the exact signed Bell generators in a finite group
+with 2^90 elements. Its normal forms are a symmetric binary matrix and a
+quadratic Boolean phase. A faithful eight-row matrix group-algebra regular
+action then gives the common annihilator by Cayley-Hamilton. Each root
+coefficient occurs once, outside the tensor power. Signs remain exact.
+
+## Evidence and reproduction
+
+From the repository root, CPython 3.12 and the standard library suffice:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/uniform-centre-gram-annihilator
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/uniform-centre-gram-annihilator/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/uniform-centre-gram-annihilator --check-source-history
+```
+
+Other machines may substitute their CPython 3.12 path. The registered replay
+includes warning-strict normal and optimized modes. Direct replay also works
+in the official Git-free export. It reads the declared historical query and
+writes nothing. [RESULT.json](RESULT.json) is a generated receipt bound to
+the source and all seven other package files; it is compared byte for byte.
+
+The verifier enumerates the complete enclosing normal forms at n=1,2,3,
+with 4,64,4096 distinct signed permutations respectively. All 4112 ordered
+products at n=1,2 agree with literal composition. The new quadratic cross
+term agrees by independent interpolation and monomial expansion on every
+one of the 12544 ordered actual-port generator pairs; five states per pair
+also agree with literal action. A separate eight-dimensional regular-action
+example has its polynomial checked at nine determinant values and in tensor
+representations of dimensions 8,32,128. Twelve controls cover missing signs,
+quadratic terms, product order, false involutions, wrong tensor coefficients,
+invalid inputs, source corruption and a changed polynomial.
+
+The universal theorem rests on the written proof. These finite checks do
+not enumerate the 2^90-element group or certify its huge regular determinant.
+No predecessor spectral certificate or complete scientific replay is used
+as the deliverable. Independent human and formal proof-kernel review are
+unclaimed.
+
+## Credit, overlap and limits
+
+Credit Krzysztof Wojt / PR5168 for the exact one-slot degree 881 and the
+uniform-upper-bound question. Ali Romman / [PR4958](https://github.com/CrocSwap/integer-mult-bounds/pull/4958)
+and PR4720 supply the query and Bell action; his
+[PR5382](https://github.com/CrocSwap/integer-mult-bounds/pull/5382) supplies
+the equal-label two-slot spectrum and higher-width lower bound 1093.
+Nick Petalas / PR5120 supplied the earlier lower bound 410. Those results
+are cited premises and context, not freshly validated here. PR1719 supplies
+the doubled representation, with the Gauge44/native/compiler lineage retained
+in the unchanged [source notice](../centre-polynomial-cache-limits/NOTICE.md).
+David Ganz / [PR4885](https://github.com/CrocSwap/integer-mult-bounds/pull/4885)
+supplies a related group-algebra recovery precedent for a different resonant
+operator. Boolean normal forms, group regular representations and
+Cayley-Hamilton are classical; no global literature priority is claimed.
+
+The new contribution is the exact finite quadratic signed-translation
+envelope and its all-width Gram consequence. [SOURCES.json](SOURCES.json)
+pins the live query and predecessor proof/notice provenance. Base is canonical
+main 2485805a6d47f36ea83ddde6327d453ac82d44dc, priority revision 8. The
+formal-interface-lemma card explicitly changes to this algebraic side result.
+The selected baseline passed at conditional kappa .003125804. This historical
+112-port result discharges none of the current selected framework assumptions.
+
+Live handoffs, active Discussions, open PRs, recent account work, merged
+object/formula searches and main README searches were checked. The overlap
+cache covered 363 open PRs and 6100 Discussion records. Its initial sparse
+local search covered 94 of 8722 tracked notes; relevant source packages were
+then materialized and Git-tree searches covered the candidate terms. These
+checks do not establish global novelty or cover unpublished work. The
+[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19299705)
+records the bounded question. No other open PR studying this historical Gram
+was found in the checked live data.
+
+Native access, coefficient preparation, physical implementation, precision,
+ownership, restoration, tape and storage costs, a complete supplier invoice
+and outer multiplication remain open. No selected cold replay, Lean or Docker
+run was performed. A huge polynomial existence bound is not a practical
+decoder or a bound on general ADD circuits. Apache-2.0.
+
+## Open next questions
+
+Structured first steps and blockers are in [TASK.json](TASK.json).
+
+- Determine the actual generated subgroup and its irreducible representations.
+  Start with the normal form's translation and central-phase subspaces; their
+  exact dimensions are not supplied here.
+- Determine the spectrum attained at each width, including unequal Bell labels.
+  A complete representation-multiplicity or similarity classification is missing.
+- Price one concrete decoder and its caller. Preparation, access, restoration,
+  precision and storage must enter the complete invoice before claiming a gain.
+
+## Verifier constraints
+
+Every function is below 60 lines, with no recursion, dynamic evaluation,
+subprocess or network access. Dimensions are fixed at n<=9, enumeration at
+n<=3, matrices at dimension 128, regular characteristic polynomials at eight,
+and all file reads at one MiB. The largest enumeration stores 4096 signed
+permutations of 64 states. Every loop is bounded by these fixed domains.
+Explicit exceptions keep all acceptance checks active under optimization.
+
+Power-of-ten rule 3 deviation: CPython allocates managed integers, Fractions
+and containers during checking. The fixed domains bound the live collections;
+no static-allocation claim is made. Rule 9 deviation: the rejection helper
+calls five fixed local lambdas, each with one bounded fixture. Python has no
+compiler warning mode; both registered commands use -W error and in-memory
+compilation is included in local validation. No separate static analyzer is
+assumed. Source and receipt mutations are exercised separately before publishing.

research/uniform-centre-gram-annihilator/RESULT.json

@@ -0,0 +1,55 @@
+{
+  "algebra_example": {
+    "determinant_evaluations": 9,
+    "lift_dimensions": [
+      8,
+      32,
+      128
+    ],
+    "polynomial_descending": [
+      1,
+      -4,
+      -12,
+      52,
+      54,
+      -220,
+      -140,
+      300,
+      225
+    ]
+  },
+  "controls": 12,
+  "enclosing_group_size_bound": 1237940039285380274899124224,
+  "exhaustive_composition_pairs": 4112,
+  "package_sha256": {
+    "PROOF.md": "3d0873737dd69c1808d4054d558a3de5178371d3fe1822dc955503287f74d0e0",
+    "README.md": "a4d32a5e0bbf29122280030ae75be71843e47fc331b523fb7ede4b2e042cb529",
+    "SOURCES.json": "279638c3f6f7cf07aa8f96f7610d15a453cff612687007d29608b7a9d30cb1d2",
+    "TASK.json": "23de534337bb8ff64a397571d95bf327c32ead6704ce00b76201ee92e72a5d42",
+    "VERIFY.json": "7ef2ba3648f3c7be54af66ebc0ab8ac87880be402d4b890cecb52ea3e76ce21e",
+    "group.py": "6c3bda022a097f4102b175328fe74274854126dc695d29fe05b94f6b971b90ba",
+    "verify.py": "ef0e7f417ae98388fa86a790b9a7304614e8a4e9546273813ece44d9983f1961"
+  },
+  "small_envelopes": [
+    {
+      "elements": 4,
+      "n": 1,
+      "states": 4
+    },
+    {
+      "elements": 64,
+      "n": 2,
+      "states": 16
+    },
+    {
+      "elements": 4096,
+      "n": 3,
+      "states": 64
+    }
+  ],
+  "source_generator_pairs": 12544,
+  "source_product_states": 62720,
+  "source_sha256": "5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3",
+  "status": "PASS_UNIFORM_CENTRE_GRAM_ANNIHILATOR",
+  "uniform_annihilator_degree_bound": 9903520314283042199192993792
+}

research/uniform-centre-gram-annihilator/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "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/exact-one-slot-gram/README.md",
+      "usage": "provenance",
+      "git_blob": "d783f028fd776e7536f4ac203211b7654f1af2b0",
+      "sha256": "0c6eefe9bcfef8325b7dcd7c87c4b93a045713f508fa0f75771b4ebfeebea442"
+    },
+    {
+      "path": "research/centre-polynomial-cache-limits/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "98e070a4e309010d76d7885b39366f9a9ef71341",
+      "sha256": "ebcd0912e990c71f3b29b87674c1b5e3efa8f5ea37ed20f4fd06d80ce27f6382"
+    },
+    {
+      "path": "research/centre-polynomial-cache-limits/NOTICE.md",
+      "usage": "provenance",
+      "git_blob": "b0262bd4f2a4dd701713914c3ae47cb1225848d6",
+      "sha256": "4dde831dc40b31d0edc23adbcd0aaeec3aa573eef6f4f27fcdb53d24eab173e8"
+    },
+    {
+      "path": "research/equal-bell-two-slot-spectrum/README.md",
+      "usage": "provenance",
+      "git_blob": "3e9e574cb86729bec406db9073610c340270ab05",
+      "sha256": "e20b09c62eda072e2db18d104b2edeb89083549557753c9cfe460809e44ec5a7"
+    },
+    {
+      "path": "research/resonant-all-width-projector/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "2a65c15bebaa9096d79dea2f0e898cdeee0b4ac4",
+      "sha256": "a11f8a97519ae94982b1a212d2cc9789d82a4452317eb1d3843080caf910c45c"
+    }
+  ]
+}