Prove sharp 1/4 error for every real rank-seven P104 approximation (no κ)

research/p104-rank-seven-error-floor/PROOF.md

@@ -0,0 +1,121 @@
+# Sharp error for every real rank-seven Gram approximation
+
+## Statement and scope
+
+Let the rows of R be one representative of squared norm 2 from each of
+the 56 D8 lines e_i +/- e_j in R^8, together with any proper subset of
+the 64 half-spin lines of one parity. Write m for the number of rows and
+K=RR^T/2. Then
+
+    min { max_ij |K_ij-C_ij| : C in R^(m x m), rank C <= 7 } = 1/4.
+
+There is no assumption on C's symmetry, sign, spectrum, or row and column
+spaces. In particular C need not have the form RDR^T/2. This strengthens
+Nick Petalas's PR6183 theorem for symmetric positive contractive carrier
+filters, answering its first open question and the larger unrestricted
+real-matrix question. Its attaining projection is retained with credit.
+
+The theorem uses the full coefficient matrix, real scalars, and the fixed
+Gram target. It is not a statement about masked entries, complex matrices,
+nonlinear consumers, a changed total target, or physical implementation cost.
+
+## Eight columns detect every deficient-rank candidate
+
+Choose the eight retained column labels J corresponding to
+
+    e_1+e_2, e_1-e_2, e_3+e_4, e_3-e_4,
+    e_5+e_6, e_5-e_6, e_7+e_8, e_7-e_8.
+
+Let U=R[J,:]. Stored representatives may differ by row signs. These roots
+are mutually orthogonal with squared norm 2, so UU^T=U^TU=2I.
+
+For arbitrary C of rank at most seven, the m-by-8 submatrix C[:,J] has
+a nonzero real null vector a. Put z=U^T a. Then z is nonzero,
+a=Uz/2, and K[:,J]a=Rz/2. For real s,t,
+
+    (|s+t|+|s-t|)/2 = max(|s|,|t|).
+
+Consequently, writing b_1>=...>=b_8 for the sorted absolute coordinates
+of z and h=b_1+b_2>0,
+
+    ||a||_1 = sum_(four coordinate pairs) max(|z_i|,|z_j|)
+            <= b_1+b_2+b_3+b_4 <= 2h.
+
+The first inequality holds because the four maxima select four distinct
+coordinates; the second uses b_3<=b_1 and b_4<=b_2. Row sign choices in
+U do not change its left-hand side. The retained D8 roots include a signed
+root joining the two largest absolute coordinates of z. Hence
+
+    ||Rz||_infinity >= h.
+
+The extra half-spin rows may make this inequality strict. If
+epsilon=max_ij |K_ij-C_ij|, coefficientwise triangle inequality gives
+
+    h/2 <= ||K[:,J]a||_infinity
+         = ||(K-C)[:,J]a||_infinity
+         <= epsilon ||a||_1 <= 2 epsilon h.
+
+Divide by h to obtain epsilon>=1/4. This is an all-real-matrix proof,
+not an inference from the finite verifier. It uses only the D8 rows and
+eight D8 columns; no projection back to the carrier spaces is needed.
+
+Equivalently, an approximation with entry error strictly below 1/4 must
+have eight independent columns at J, and therefore rank at least eight.
+The norm ratio is sharp: take z with one nonzero coordinate in each of
+the four pairs, all of the same magnitude. Then ||a||_1=2h.
+
+## Attainment (PR6183's construction)
+
+Choose an omitted half-spin root q. It has squared norm 2. Set
+
+    D = I-qq^T/2,
+    C = RDR^T/2 = K-(Rq)(Rq)^T/4.
+
+D is a rank-seven orthogonal projector. R has column rank eight because
+it contains U. Therefore C has rank seven: a left inverse of R shows
+rank D<=rank(RDR^T), and the opposite inequality is immediate.
+
+For every D8 root r, r dot q belongs to {-1,0,1}. For two distinct lines
+in the same half-spin parity shell, their sign patterns differ in an
+even number of coordinates, and the inner product also belongs to
+{-1,0,1}. The line of q is absent, so
+
+    |K_ij-C_ij| = |(r_i dot q)(r_j dot q)|/4 <= 1/4.
+
+A D8 root has inner product of magnitude one with q; its diagonal error
+is 1/4. This proves attainment, including when the half-spin subset is
+empty. No optimality or invention of this projection is attributed here.
+
+## P104 binding, precision consequence, and limits
+
+Matarener's PR6166 at 096938513138868f0ed27639061f1a5054900f96 identifies
+the relevant P104 configuration with all 56 D8 lines plus 48 half-spin
+lines in orthonormal coordinates. This identification remains a cited
+premise, as it was in PR6183; it is not independently audited here.
+The source-pinned MISSING.json from PR6183 records its sixteen omitted
+lines. The verifier constructs and checks the resulting mathematical
+root set and the sixteen attaining matrices. That is distinct from
+checking the physical selected ports' coordinate identification.
+
+PR6183 at eaf77790466f34b86ce72080e3ec690e26dfacab supplies the preceding
+question, Gram convention and attaining projection. Rohan Arun's PR1972,
+Chafik Boukhalfa's PR1991 and their retained lineage supply the earlier
+Gram channel. Their native/operator theorems are not replayed or adopted
+as new results here.
+
+For any real rank-seven C, some entry (i,j) of K-C has magnitude at least
+1/4. On input B e_j the i-th output bias is at least |B|/4. Unlike the
+positive-error predecessor, this argument need not locate a diagonal
+entry. The maximum-entry norm here equals the induced l1-to-l_infinity
+norm; the theorem does not assert an l2 operator-norm optimum.
+Increasing arithmetic precision cannot make this fixed approximation
+bias vanish. Any changed side correction or consumer must account for it.
+
+This closes arbitrary real linear rank-seven replacement of this whole
+Gram block. It does not price corrections, transport, restoration,
+native calls, compiler operations, precision/tape work or the completed
+supplier. No selected framework assumption is discharged and no kappa
+improvement follows. General literature priority, independent human
+review and formal proof-kernel acceptance are unclaimed.
+
+Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0.

research/p104-rank-seven-error-floor/README.md

@@ -0,0 +1,116 @@
+# Every real rank-seven P104 Gram approximation has error at least 1/4
+
+The exact minimum maximum coefficient error is **1/4 over all real
+104-by-104 matrices of rank at most seven**. This removes symmetry,
+positivity, contractivity, and fixed carrier row/column spaces from
+Nick Petalas's [PR6183](https://github.com/CrocSwap/integer-mult-bounds/pull/6183)
+result. It answers that package's first open question. No new kappa is claimed.
+
+Eight orthogonal D8 root columns turn any deficient-rank candidate into
+a nonzero null vector. A sharp l1 norm comparison forces the error floor.
+PR6183's omitted-root projector attains it. The [written proof](PROOF.md)
+covers every real candidate; exact finite checks corroborate its identities
+and exercise candidates outside the predecessor's domain.
+
+The P104 coordinate identification remains an explicitly cited premise
+from Matarener's PR6166, retained through PR6183. This contribution verifies
+the resulting root configuration, not its physical port identification.
+Both predecessors are archived as partially reviewed in the current ledger;
+archival inclusion is not scientific acceptance.
+The theorem also applies to all D8 lines plus any proper subset of one
+half-spin shell. Root representative signs do not matter.
+
+## Reproduce
+
+With CPython 3.12 and the standard library, from the repository root:
+
+```sh
+python3.12 -I -W error -B research/p104-rank-seven-error-floor/verify.py
+python3.12 -I -W error -O -B research/p104-rank-seven-error-floor/verify.py
+python3.12 -I -W error -O -B research/p104-rank-seven-error-floor/independent.py
+python3.12 -B scripts/research_package.py --package research/p104-rank-seven-error-floor
+```
+
+The direct marker is `PASS_P104_RANK_SEVEN_ERROR_FLOOR`; the registered
+marker is `PASS_REGISTERED_RESEARCH_PACKAGE`. Direct runs read only and
+emit a deterministic JSON receipt with computed coverage counts. They work
+in a Git-free export with an empty PATH when Python is invoked absolutely.
+SOURCES.json authenticates the three predecessor document/data inputs;
+VERIFY.json declares all of them. No predecessor executable is imported.
+
+The checks cover the orthogonal eight-column frame, exact null-vector norm
+inequalities, all sixteen attaining projections and every matrix entry,
+oblique filters, candidates with row/column spaces outside the root code,
+and hypothesis/normalization controls. Normal and optimized replay pass
+6,560 nonzero ternary directions, 128 rational directions, sixteen projections
+with 173,056 literal matrix-error entries, three carrier fixtures and one
+candidate outside both carrier spaces. Four boundary/normalization controls
+and three malformed-input rejections also pass. The proof, rather than these
+finite fixtures, establishes the universal quantifier. See the emitted receipt
+for exact counts and [TASK.json](TASK.json) for verification coverage.
+
+The separately written `independent.py` uses literal Fraction roots and a
+different root order, with no primary-checker import. Its optimized registered
+replay passes 147 vector fixtures (including two tight norm witnesses) and
+194,688 matrix entries across sixteen attaining projectors, an oblique
+projector (error 3/8), and a matrix outside the carrier factorization
+(error 1/2). It corroborates arithmetic and scope boundaries; it does not
+mechanically prove the universal statement or constitute human review.
+
+## Selection, overlap, and expansion decision
+
+Canonical main was pulled first at
+`a5bff3bf133e482541c09eba4e773884bdb2b1b7`, priority revision 8. The selected
+record still specifies conditional kappa `781451/250000000` with five
+framework assumptions. Its previously passing binding-only orientation
+was reused after all 1,227 recorded inputs were unchanged from the prior
+checkpoint; this is not a fresh scientific replay.
+
+This takes the released [PR6183 handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19268192).
+The original `coverage-law-change` card is retained in TASK.json, with
+scope explicitly changed to an algebraic approximation question. The
+[canonical investigation](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19271534)
+records the initial arbitrary-carrier question and its extension to all
+real rank-seven matrices. Bounded all-state PR searches and the newest
+visible handoffs found no competing result. The local overlap helper
+searched only 28 of 8,623 notes and had no remote cache; neither it nor
+the bounded live search certifies exhaustive novelty.
+
+Nearest work: PR6183 proves the contractive case and provides attainment;
+PR6181 concerns exact joint-bank spectral conjugacy over Gaussian dyadics;
+PR6173 concerns generalized code support over F3 and Q. Their different
+quantities are not compared numerically or silently treated as validated.
+
+Decision: close this approximation escape, then stop. The boundary is the
+whole real Gram block on arbitrary inputs. A seven-dimensional real linear
+intermediate cannot approximate it arbitrarily accurately, even with new
+encoder/decoder spaces. Correction, native implementation, restoration
+and complete costs remain unknown. This local proof justifies no further
+construction campaign or selected-frontier change on its own.
+
+## Open next questions
+
+- Can a changed side correction absorb an attaining residual at a favorable
+  complete cost? Start with one omitted-root residual in an actual scalar
+  word, charging acquisition, delivery and restoration. A physical caller
+  and complete invoice are missing. This is PR6183's remaining second question.
+- What is the optimum for arbitrary **complex** rank-seven approximants?
+  The real absolute-value identity used here does not hold for complex
+  coordinates. Start with a dual norm certificate or an exact complex
+  factorization beating 1/4; numerical searches alone cannot settle it.
+  No complex lower bound or physical realization is supplied.
+
+## Credit and limits
+
+New lower-bound proof and verifier: apoursh, with substantial OpenAI Codex
+assistance and separate agent proof checks. Nick Petalas retains PR6183's
+question, contractive theorem and attaining projection. Matarener retains
+the D8 coordinate identification and omitted lines. Rohan Arun, Chafik
+Boukhalfa, Ali Romman, DreamingOfClouds, Cinna Davis, Pierre-Loic Doulcet,
+icekylinx, zxv, Jacob Alan Sussman and the retained P104/root/frame/native/
+helper/compiler/BIT contributors retain their source results.
+
+This is a scoped written proof with exact finite corroboration, not a
+physical supplier, full multiplication theorem, independent human review,
+or formal proof-kernel result. Masked accuracy and nonlinear consumers
+remain outside scope. Sources and shared code are unchanged. Apache-2.0.

research/p104-rank-seven-error-floor/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7",
+  "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/p104-contractive-gram-deflation/MISSING.json",
+      "usage": "input",
+      "git_blob": "d5f76681db5edb99899ce6509913b0db60f7280c",
+      "sha256": "9ddfcf087912e02c46722d5a82eea5f1221a4a33d5037a0d90d392dfcd3c06d4"
+    },
+    {
+      "path": "research/p104-contractive-gram-deflation/PROOF.md",
+      "usage": "input",
+      "git_blob": "2cf92ff47f0271c6fd2266884a1b307a09b35c63",
+      "sha256": "8e44fe3d11d777535131e0a4c7cdde8fbc4c0d2b69254e587432c71ce39a61a6"
+    },
+    {
+      "path": "research/p104-contractive-gram-deflation/README.md",
+      "usage": "input",
+      "git_blob": "d3a11f74d5c908d7b9bf28235c36ea9850e458b3",
+      "sha256": "5643af3d891e2731237c0f8a4ae97d5ae0515b03d369e835fbf80cc612821415"
+    }
+  ]
+}