Prove centre Gram degree and least invariant scalar-cache bounds

research/centre-polynomial-cache-limits/NOTICE.md

@@ -0,0 +1,42 @@
+# Credit, source pins, and limits
+
+The source is the historical selected construction at commit
+`bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. Its selected archive is
+[retained here at the source commit](https://github.com/CrocSwap/integer-mult-bounds/blob/bce54fb3f895cbe5cd4c0eb477c3afeed100190f/research/community-frontier1042-audit/selected-replay.tar.gz).
+The two needed archive members are copied without edits. Their original
+compressed digests and the complete archive digest are in SOURCES.json.
+
+The original supplier notices are retained under `notices/`. They identify
+the source work, compiler work, and earlier contributor lineage. In
+particular, the [Gauge44 notice](https://github.com/CrocSwap/integer-mult-bounds/blob/bce54fb3f895cbe5cd4c0eb477c3afeed100190f/research/gauge44-slots-t16/NOTICE.md)
+credits icekylinx and retains the upstream notices. This package does not
+infer contributor identity from a PR submitter account.
+
+The circuit-interface lane derived the actual R. The history-encoding
+lane supplied the Bell certificate. The interface-proof lane supplied
+the separate sparse replay, the all-size extension, and the inverse
+corollary. The native-encoding lane supplied the scalar-cache theorem.
+These are OpenAI Codex research roles under Ali Romman's direction.
+They are not independent human authors or reviewers. Substantial
+OpenAI Codex assistance was used for research, checks, and packaging.
+
+[PR #1719](https://github.com/CrocSwap/integer-mult-bounds/pull/1719)
+published the historical doubled Walsh lift at commit
+`3ae9a6f3ac74ded022ab3b4872a7357a621af6fb`. This package uses the doubled
+port representation to study one weighted Gram; it does not re-publish
+that lift as a new construction.
+
+The actual query source is already retained by
+[PR #4720](https://github.com/CrocSwap/integer-mult-bounds/pull/4720) at
+[this exact source path](https://github.com/CrocSwap/integer-mult-bounds/blob/cb102a57254748651ce16aa4454bb611f6380e53/research/actual-query-information-bounds/payload/lanes/circuit-interface/INTERFACE.json).
+That PR also publishes the separate scalar source-span theorem.
+[PR #4750](https://github.com/CrocSwap/integer-mult-bounds/pull/4750)
+publishes the [fixed-code projector criterion](https://github.com/CrocSwap/integer-mult-bounds/blob/3c6a768e5391e6bc8355fe2bc849d2978afef8f6/research/phase-coded-callers/annexes/fixed-code-interface/PROOF.md).
+The new package does not claim those results again.
+
+The 22 October cleanup audit found these two notes outside the fixed
+469-observation closure. It checked the exact published source objects
+and found no equivalent adopted statement in the 15 campaign packages.
+A bounded source search is not a universal literature novelty check.
+
+Apache-2.0 applies. Original notices and license text are unchanged.

research/centre-polynomial-cache-limits/PACKAGE-MANIFEST.json

@@ -0,0 +1,164 @@
+{
+  "files": [
+    {
+      "path": "NOTICE.md",
+      "bytes": 2804,
+      "sha256": "4dde831dc40b31d0edc23adbcd0aaeec3aa573eef6f4f27fcdb53d24eab173e8"
+    },
+    {
+      "path": "PROOF.md",
+      "bytes": 5655,
+      "sha256": "ebcd0912e990c71f3b29b87674c1b5e3efa8f5ea37ed20f4fd06d80ce27f6382"
+    },
+    {
+      "path": "README.md",
+      "bytes": 3420,
+      "sha256": "7569c606042bacf8c36b75fbbd1dfef9a8861d194659c4a93dfa68fddc7c044f"
+    },
+    {
+      "path": "SOURCES.json",
+      "bytes": 5809,
+      "sha256": "b3ad9ed33fda0ffb64d50ed6d026168651b9351a16a21ca0b9821c179b474d3d"
+    },
+    {
+      "path": "check_phase_cache.py",
+      "bytes": 5314,
+      "sha256": "16ed9b27047d065c7a7648ebc8dc46438ec93c7cfbc530f9cc996e878d1ffe5d"
+    },
+    {
+      "path": "frozen/work/centre-encoding-campaign-20261014/lanes/bounds-review/review_centre_free.py",
+      "bytes": 8966,
+      "sha256": "33b6b73303275e481f12cc2f946d1273ca9ac03d9294600016f03e84e6921088"
+    },
+    {
+      "path": "frozen/work/centre-encoding-campaign-20261014/lanes/circuit-interface/INTERFACE.json",
+      "bytes": 23232,
+      "sha256": "5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3"
+    },
+    {
+      "path": "frozen/work/centre-encoding-campaign-20261014/lanes/history-encoding/BELL-GRAM-DEGREE-PROOF.md",
+      "bytes": 4001,
+      "sha256": "bc3a72690735230e8d9995df1a343f69fe8afed7dce056a82505efc83a884698"
+    },
+    {
+      "path": "frozen/work/centre-encoding-campaign-20261014/lanes/history-encoding/BELL-GRAM-DEGREE.json",
+      "bytes": 10174,
+      "sha256": "4b198523d498b85b96445681fdcd8020402b1abb31c6a27e7d2a45d5df2217e2"
+    },
+    {
+      "path": "frozen/work/centre-encoding-campaign-20261014/lanes/history-encoding/BELL-GRAM-INVERSE-COROLLARY.md",
+      "bytes": 1058,
+      "sha256": "d1d3011e26d5768edc10ac234aeb9cb80c721addc28f9aabc784f56383ca4fe3"
+    },
+    {
+      "path": "frozen/work/centre-encoding-campaign-20261014/lanes/history-encoding/certify_bell_gram_degree.py",
+      "bytes": 5140,
+      "sha256": "8604d1665862593efc146644fbf47a85c4a2aca88106284096d723853a064e45"
+    },
+    {
+      "path": "frozen/work/centre-encoding-campaign-20261014/lanes/interface-proof/BELL-GRAM-DEGREE-REVIEW.json",
+      "bytes": 1996,
+      "sha256": "4f48be6cfd0f7ab316d1dc957ba18668b56a4feed55ef8cae5c205560e13b16a"
+    },
+    {
+      "path": "frozen/work/centre-encoding-campaign-20261014/lanes/interface-proof/BELL-GRAM-DEGREE-REVIEW.md",
+      "bytes": 3113,
+      "sha256": "3a670ff14be1db7109d12d1fc6c28704543d3a19ad2e9d4ac6431a0a86a57d9f"
+    },
+    {
+      "path": "frozen/work/centre-encoding-campaign-20261014/lanes/interface-proof/review_bell_gram_degree.py",
+      "bytes": 9719,
+      "sha256": "0d9983c288292f568c1f1595b944ca81131f79119855b7ad5c64e28c3cbfd899"
+    },
+    {
+      "path": "frozen/work/centre-encoding-campaign-20261014/lanes/native-encoding/PHASE-CACHE.md",
+      "bytes": 7975,
+      "sha256": "bd53f0c38ac06e20b8361543086bb5f6310bdeb552fb692dc29978434cd4dc84"
+    },
+    {
+      "path": "frozen/work/five-pr-sprint-20261013/lanes/centre-sharing/CANONICAL-WORD.json.gz",
+      "bytes": 84805,
+      "sha256": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219"
+    },
+    {
+      "path": "frozen/work/five-pr-sprint-20261013/lanes/centre-sharing/LOCAL-PROGRAMS.json.gz",
+      "bytes": 209318,
+      "sha256": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a"
+    },
+    {
+      "path": "notices/LICENSE",
+      "bytes": 11357,
+      "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4"
+    },
+    {
+      "path": "notices/research/gauge44-slots-t16/NOTICE.md",
+      "bytes": 1964,
+      "sha256": "7a8d17b04da1e6c9d0ec217fb5bda72faa09d9a21695128722dd1e2827870fcf"
+    },
+    {
+      "path": "notices/research/gauge44-slots-t16/UPSTREAM-NOTICE.md",
+      "bytes": 6406,
+      "sha256": "a75967ebc34e3bf2ff2c25c08e6c7f1a61b0c0d171cfd1b62196ae2caaf2c610"
+    },
+    {
+      "path": "notices/research/gauge44-slots-t16/construction/NOTICE.md",
+      "bytes": 950,
+      "sha256": "defe7e44af610e25a6c50c1c3b2efd0972d0690574995c0c872fc50eebf4c816"
+    },
+    {
+      "path": "notices/research/gauge44-slots-t16/t16/NOTICE.md",
+      "bytes": 2245,
+      "sha256": "902370e6bfcd39dbea2ece474f15fccbcce3b8e966b2b94066bd03e5174591b5"
+    },
+    {
+      "path": "replay.py",
+      "bytes": 3216,
+      "sha256": "20f3436ba77856ba233650bd04a42daad6c597bb19b439e5291cc3226057e98c"
+    },
+    {
+      "path": "requirements.txt",
+      "bytes": 12,
+      "sha256": "a83a2a4ed7ab2e022b9b8a83cfa2b8cf52cc243006c597e8b96f90a8365590ac"
+    },
+    {
+      "path": "validation/PHASE-CACHE-CHECK.json",
+      "bytes": 1376,
+      "sha256": "34386095a77c0aa3008e652fb2dc982a654b17b525dd0f85bf3b72c8867d3556"
+    },
+    {
+      "path": "validation/REPLAY.json",
+      "bytes": 2075,
+      "sha256": "7898245ca60369fcae643ce6f5bec5065e2e2aa0d46c1658b8e5f5ca56253779"
+    },
+    {
+      "path": "validation/bell-producer-stderr.txt",
+      "bytes": 0,
+      "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    {
+      "path": "validation/bell-producer-stdout.txt",
+      "bytes": 200,
+      "sha256": "b8a03214ced2b88ff097a6a7f5ba55f40dd931299b1fe75cb6d62d2108877b29"
+    },
+    {
+      "path": "validation/bell-review-stderr.txt",
+      "bytes": 0,
+      "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    {
+      "path": "validation/bell-review-stdout.txt",
+      "bytes": 135,
+      "sha256": "04001332aac6a4120ebb33bc8a6f1946fe96094f7ef6bd2d8ea73ed52f60c1e8"
+    },
+    {
+      "path": "validation/phase-cache-stderr.txt",
+      "bytes": 0,
+      "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    {
+      "path": "validation/phase-cache-stdout.txt",
+      "bytes": 39,
+      "sha256": "3fad44ed5923785fcc2c7534cd9887c315168ffbcd5d9f1c5935a461585d7622"
+    }
+  ]
+}

research/centre-polynomial-cache-limits/PROOF.md

@@ -0,0 +1,126 @@
+# Exact scope of the retained results
+
+The input is the actual eight-by-112 rational query matrix R at historical
+source commit `bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. It satisfies
+`R R^T = 56 I`. Its 112 labels q are distinct, nonzero, odd vectors in
+`F_2^9`. Each column has four entries in `{1,-1}`. This package does not
+replace these columns with the completed 120-root system.
+
+## 1. Scalar-polynomial degree
+
+Let `H_q = (X_q+Z_q)/sqrt(2)` and `Gamma_q = H_q tensor H_q` on the
+doubled binary payload. A common scalar phase does not change the
+conjugation used below. Define, for each positive integer lambda,
+
+```text
+A_lambda = (1/4) sum_q r_q r_q^T tensor Gamma_q^tensor(lambda).
+```
+
+Here r_q is the corresponding column of R. The root coefficient occurs
+once. It is not raised to a tensor power.
+
+Identify doubled payload vectors with Pauli matrices `X^b Z^a`. The
+four-term expansion of conjugation by H_q gives
+
+```text
+|a,b> -> (-1)^(q dot a) |a,b>       if q dot (a+b) = 0,
+|a,b> -> |a+q,b+q>                 if q dot (a+b) = 1.
+```
+
+Thus c=a+b is fixed. On the a coordinate in the block c=11, the port
+operator is Z_q when `q dot c=0` and X_q otherwise. The resulting block
+A has dimension 4,096 and entries in `Z[1/2]`.
+
+The [retained certificate](frozen/work/centre-encoding-campaign-20261014/lanes/history-encoding/BELL-GRAM-DEGREE.json)
+fixes integer vectors v,w by SHAKE256 seeds and gives 817 moments
+`s_j=w^T A^j v` modulo 65,537. The 409-by-409 Hankel matrix
+`H[i,j]=s_(i+j)` has determinant 2,984 modulo 65,537. The separate
+[review](frozen/work/centre-encoding-campaign-20261014/lanes/interface-proof/BELL-GRAM-DEGREE-REVIEW.md)
+derives R from the original word, builds the sparse integer matrix 4A,
+and checks the same determinant by fraction-free elimination in the
+prime field. It also checks every Bell sign and the common fixed vector.
+
+This determinant belongs to `Z[1/2]`, and its reduction is nonzero,
+so the determinant itself is nonzero. The first
+409 Krylov vectors are therefore independent. No scalar polynomial of
+degree below 409 annihilates A. The nonzero minor remains nonzero over
+any characteristic-zero field extension.
+
+The Bell identity vector is fixed by every Gamma_q. Tensor the certified
+block with this vector in all remaining tensor slots. The restriction of
+A_lambda to that invariant subspace is exactly A. The degree bound holds
+at every positive lambda, including when the proposed polynomial depends
+on lambda.
+
+If `aI+bA_lambda` is invertible, `b != 0`, and
+`q(A_lambda)=(aI+bA_lambda)^-1`, then
+`(a+bt)q(t)-1` is a nonzero annihilating polynomial. It has degree at most
+`degree(q)+1`. Therefore `degree(q) >= 408`.
+
+The result does not give the exact minimal polynomial. It does not bound
+rational expressions, matrix-valued encodings, general scalar ADD
+circuits, or the native cost of a decoder.
+
+## 2. The least scalar cache for diagonal updates
+
+Let R be any complex matrix with finitely many columns. Let D_1,...,D_t
+be diagonal matrices. Put two columns in the same fiber F when all D_j
+have the same diagonal entries at those columns. Then the smallest row
+space E that contains row(R) and satisfies `E D_j subset E` for every j
+is
+
+```text
+E = direct_sum_F row(R restricted to F),
+dim(E) = sum_F rank(R restricted to F).
+```
+
+Each summand has support only on F. This direct sum contains row(R) and
+is invariant under every D_j. Conversely, choose a linear combination D
+of the D_j whose diagonal values distinguish the finitely many fibers.
+Such coefficients exist over C: a finite union of proper hyperplanes
+does not fill the coefficient space. Polynomial interpolation in D gives
+each fiber projector. Any invariant E that contains row(R) must contain
+the projection of every row onto every fiber. The supports are disjoint,
+so their dimensions add. A basis in each fiber attains the bound.
+
+For the historical R, use sign characters `D_s[p,p]=(-1)^(q_p dot s)`.
+For the ordered normal directions
+
+```text
+42, 7, 25, 52, 82, 127, 97, 76
+```
+
+the successive dimensions, including the empty family, are
+
+```text
+8, 15, 28, 44, 44, 56, 56, 56, 56.
+```
+
+The final fibers are fourteen eight-column groups of rank four. For the
+first zero through nine coordinate characters the dimensions are
+
+```text
+8, 16, 31, 53, 85, 101, 112, 112, 112, 112.
+```
+
+Thus six specified coordinate characters already require all 112 source
+directions in this cache model. The 56-row cache does not support the
+full source-phase family. The exact rank histogram of the two-demand
+stack `[R; R D_s]`, over all 512 sign characters, is two of rank eight,
+sixteen of rank fifteen, and 494 of rank sixteen.
+
+The original [phase-cache note](frozen/work/centre-encoding-campaign-20261014/lanes/native-encoding/PHASE-CACHE.md)
+contains this argument and these counts. The package check independently
+reconstructs the counts from R and the labels. It checks the row-basis
+construction directly. This is a scalar representation result. It permits
+redundant cache rows, but does not permit a source-dependent payload
+operator before the cache unless the input contract is changed.
+
+The related fixed-code graph theorem in
+[PR #4750](https://github.com/CrocSwap/integer-mult-bounds/pull/4750)
+tests whether one given code is invariant. The result here gives the
+smallest invariant enlargement of a specified query space. The
+[source-span theorem in PR #4720](https://github.com/CrocSwap/integer-mult-bounds/pull/4720)
+uses a different payload-query grammar and independently gives 112 scalar
+source directions. These earlier published results are not new claims
+of this package. No universal novelty claim is made.