Prove doubled centre Gram degree at least 410 (no new κ)

research/centre-gram-degree410/PROOF.md

@@ -0,0 +1,138 @@
+# The doubled centre Gram needs degree at least 410
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Operator and inherited identities
+
+Use Ali Romman's actual historical query in PR4958, with eight-by-112
+matrix R and distinct port labels q in F2^9. Its exact source digest is
+5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3.
+Write r_q for its column. No normal columns are added.
+
+The cited doubled representation and Bell identity give
+
+    A_lambda = (1/4) sum_q r_q r_q^T tensor Gamma_q^tensor(lambda),
+    Gamma_q = H_q tensor H_q,  H_q = (X_q + Z_q)/sqrt(2).
+
+The root coefficient occurs once, not once per tensor slot. We use PR4958's
+Bell-block formula and common fixed vector as premises. Its degree-409
+certificate is not replayed or used as an input to the new certificate.
+
+In one doubled slot, c=a+b is invariant. In block c, the action on the
+remaining address a in F2^9 is
+
+    P_q(c) e_a = e_(a+q)                    if q dot c = 1,
+    P_q(c) e_a = (-1)^(q dot a) e_a        if q dot c = 0.
+
+Thus the 4,096-dimensional block on the eight query coordinates is
+
+    A_c = (1/4) sum_q r_q r_q^T tensor P_q(c).
+
+Different c give disjoint invariant subspaces. This permits a new
+certificate on B=A_1 direct-sum A_11, of dimension 8,192. It is a
+restriction of the full one-slot operator, not a sum of operators on the
+same subspace. This distinction is needed for the moment argument.
+
+## New finite certificate
+
+Set p=65537. This is prime, as trial division through 256 verifies.
+Let v and w be eight-by-512 arrays obtained from 8,192 SHAKE256 bytes,
+read as little-endian unsigned 16-bit integers and reshaped in row order.
+The exact ASCII seeds are
+
+    v: new-degree410-centre-gram
+    w: new-degree410-centre-gram-observer
+
+Put V=(v,v) and W=(w,w) on the direct sum. For j=0,...,818 calculate
+
+    s_j = W^T B^j V
+        = w^T A_1^j v + w^T A_11^j v     in F_p.
+
+The new Hankel matrix is H_ij=s_(i+j), 0<=i,j<410. Direct exact
+calculation gives
+
+    det(H) = 58805 mod 65537, which is nonzero.
+
+The verifier regenerates every moment. It checks every one of the 1,638
+block Krylov vectors using two implementations: a factored R^T/labeled
+port/R action and a literal sum of the 112 signed rank-one port actions.
+It then computes the same determinant using modular Gaussian elimination
+with NumPy integer arrays and fraction-free condensation with Python
+integers. No floating-point arithmetic or eigensolver occurs.
+
+The optional --emit-result command prints the two complete moment lists,
+their summed list, the determinant, exact seeds and SHA256 hashes of all
+six package files and the actual query input. This is a generated receipt.
+Default verification and receipt generation write no files.
+
+## Characteristic-zero consequence
+
+All entries of B, V, W and H belong to Z[1/2]. Reduction modulo the odd
+prime p is therefore defined. A nonzero reduced determinant implies that
+the original determinant is nonzero over Q, and remains nonzero after any
+characteristic-zero field extension.
+
+If V,BV,...,B^409 V were linearly dependent, left multiplication by
+W^T B^i for i=0,...,409 would give the same dependence among the columns
+of H. Hence these 410 vectors are independent. No nonzero polynomial
+of degree below 410 can annihilate B. Since B is a restriction of A_1,
+no such polynomial can annihilate the full A_1 either.
+
+This is a finite exact certificate with a characteristic-zero implication.
+It excludes degree exactly 409 for the full operator. It does not supply
+an annihilating polynomial or the exact minimal-polynomial degree.
+
+## Every positive tensor size and inverse polynomials
+
+PR4958 supplies a common positive-one eigenvector e of every Gamma_q,
+namely the Bell vector a=b=0. For lambda>=1, restrict A_lambda to the
+first-slot direct sum above, tensored with e in every remaining slot.
+Every term preserves this subspace and acts there exactly as B. The
+query coefficient r_q r_q^T is still applied once. Consequently,
+
+    degree(minimal polynomial of A_lambda) >= 410
+
+for every positive lambda, even if the proposed polynomial depends on
+lambda. This uses the cited Bell/tensor identities; it is not a new
+native all-column implementation proof.
+
+Let alpha,beta lie in any characteristic-zero field containing the
+operator entries, beta!=0, and assume alpha I+beta A_lambda is invertible.
+If q(A_lambda) is its inverse, then
+
+    ((alpha+beta t) q(t) - 1)(A_lambda) = 0.
+
+The polynomial on the left is nonzero and has degree at most deg(q)+1.
+Therefore deg(q)>=409. This improves the predecessor's necessary bound
+408 by one. It does not assert that an inverse exists or that 409 is
+attainable.
+
+## Exact arithmetic and executable bounds
+
+After each application every vector entry is in [0,p-1]. The factored
+root projection has at most four signed terms. The return projection has
+at most 112 terms. Their absolute pre-reduction bounds are 4(p-1) and
+112(p-1). In the literal implementation the accumulated output is at most
+112*4*(p-1) in absolute value. Reduction precedes multiplication by 4^-1,
+so that multiplication is below 2^32. Each moment sum is at most
+4096(p-1)^2=2^44. Gaussian elimination products are at most (p-1)^2;
+subtractions also fit in signed 64-bit integers. Condensation uses
+unbounded Python integers. These bounds exclude integer overflow.
+
+All loops have fixed bounds from the authenticated 8-by-112 query,
+512 addresses, two blocks, 819 moments and a 410-by-410 matrix. Functions
+have fewer than 60 physical lines. Failure checks use explicit exceptions
+and remain active under optimization. The verifier has no recursion,
+subprocesses, network access or file writes. Both registered commands
+make warnings errors. No external static analyzer is claimed.
+
+Power of Ten rule 3 deviation applies to verify.py. CPython and NumPy
+allocate integers, lists and arrays during arithmetic; these runtime
+allocations cannot be prohibited by preallocation. The scope is this
+bounded finite replay. At most two 8-by-512 evolving vectors, fixed
+112-by-512 action tables, bounded intermediate arrays, 1,638 moments and
+410-by-410 determinant storage are live in each block/determinant phase.
+Condensation retains one 410-by-410 Python-integer matrix; temporary
+integer sizes are bounded by the modular formula. Runs in both modes
+exercise these capacities. A larger executable domain would require a
+new capacity review. There are no user-controlled scientific dimensions.

research/centre-gram-degree410/README.md

@@ -0,0 +1,98 @@
+# Doubled centre Gram degree at least 410
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+The actual historical doubled centre Gram has scalar minimal-polynomial
+degree at least **410 at every positive tensor size**, improving Ali
+Romman's PR4958 bound 409. Thus PR4958 Open next question 1 has a negative
+answer: its full operator does not have degree exactly 409. Whenever
+alpha I+beta A is invertible with beta!=0, a scalar-polynomial inverse
+has degree at least 409, improving the necessary bound 408.
+
+Claim type: a new finite exact certificate, with a scoped written
+characteristic-zero and all-positive-tensor-size proof. The exact full
+minimal polynomial is not determined. No new kappa follows.
+
+The new step joins the distinct Bell blocks c=1 and c=11 as invariant
+summands. On their 8,192-dimensional direct sum, 819 new moments give a
+410-by-410 Hankel determinant **58805 modulo 65537**. The certificate uses
+new seeds and does not consume or rerun the predecessor's 409 minor.
+[PROOF.md](PROOF.md) states the operator, seeds, arithmetic bounds and
+all-size/inverse deductions.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and NumPy 2.5.4:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/centre-gram-degree410/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/centre-gram-degree410/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/centre-gram-degree410
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/centre-gram-degree410 --check-source-history
+```
+
+Any equivalent Python 3.12 path can replace the local interpreter. The
+direct marker is PASS_CENTRE_GRAM_DEGREE410. Both operator implementations
+agree on all 1,638 block Krylov vectors; two exact determinant algorithms
+agree on the new minor. Eight controls cover the missing new block,
+linear dependence, pivoting, source corruption and truncated moments.
+The complete generated receipt is available by adding --emit-result;
+redirect it outside the checkout. It binds all package files and the
+sole live input by SHA256. No receipt is handwritten.
+
+VERIFY.json registers both warning-strict normal and optimized modes,
+with 180-second limits. The actual query JSON is the sole live external
+input. SOURCES.json also pins the original card, selected record and
+PR4958's mathematical/source documents as historical provenance. The
+scientific verifier needs neither Git nor any predecessor executable.
+The official committed-package export includes the declared input and
+can replay offline with the same Python/NumPy installation.
+
+## Scope, overlap and credit
+
+Base: canonical main 81e9bd69e4a5b00ba9c713a1620e36d576d5522e, priority
+revision 7. [Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19142769).
+TASK.json changes the formal-interface-lemma card to this explicit
+algebraic handoff. The current selected source-binding orientation passed;
+that check is metadata orientation, not scientific admission.
+
+Credit Ali Romman's [PR4958](https://github.com/CrocSwap/integer-mult-bounds/pull/4958),
+head c8c48ef5a497ffd7f7e778434c1f074b7b777a03, for the actual query,
+Bell-block identity, common fixed vector, degree-409 certificate and open
+question. PR4720 retains the historical query and source/native lineage;
+PR1719 supplies the doubled port representation. The historical selected
+source is bce54fb3f895cbe5cd4c0eb477c3afeed100190f. Retain icekylinx's
+Gauge44 attribution and the K-triangle, porting, helper, compiler and
+upstream lineage in PR4958's unchanged NOTICE.md and retained notices.
+No predecessor code or notice is copied or modified. Krylov/Hankel minors
+and modular nonvanishing are standard methods; no literature-priority
+claim is made for those methods.
+
+The live pre-claim overlap covered 323 open PR records and 4,243 Discussion
+records with complete remote pagination. Sparse local coverage was
+incomplete and was supplemented by distinctive-term searches of all
+main-tree research READMEs and merged/all-state PRs. The target is
+PR4958's open question, rather than a recent own-account follow-up.
+No exhaustive arbitrary-diff or unpublished-work coverage is asserted.
+
+This is one local obstruction, with no family construction round. Native
+access, rounded precision, dirty restoration, storage, physical movement,
+recursive pricing and complete supplier admission remain unknown. General
+ADD circuits, rational expressions and matrix-valued encodings are outside
+the scalar-polynomial restriction. No selected frontier, complete
+multiplication theorem, independent human acceptance or formal proof-kernel
+acceptance is claimed. Lean, Docker, predecessor scientific replays and the
+selected cold replay were not run.
+
+## Open next questions
+
+- What is the exact full minimal-polynomial degree? Start by deriving a
+  characteristic-zero annihilator from the joint Bell-block decomposition.
+  The new modular minor gives a lower bound, not that missing upper bound.
+- Can a useful decoder avoid scalar polynomials? Start with one specified
+  general ADD, rational-expression or matrix-valued decoder and its source,
+  output, dirty restoration and complete cost contract. Native access and
+  the paid implementation remain blockers.
+
+The structured versions, relevance and first steps are in TASK.json.

research/centre-gram-degree410/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "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/centre-polynomial-cache-limits/README.md",
+      "usage": "provenance",
+      "git_blob": "85f1b44f4876af674a77897068f80d0bb4db5ed7",
+      "sha256": "7569c606042bacf8c36b75fbbd1dfef9a8861d194659c4a93dfa68fddc7c044f"
+    },
+    {
+      "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"
+    }
+  ]
+}