Prove the uniform all-term Dn root-code cost floor

research/dn-unrestricted-root-code-floor/DEPENDENCY.json

@@ -0,0 +1,33 @@
+{
+  "schema_version": 1,
+  "repository": "CrocSwap/integer-mult-bounds",
+  "files": [
+    {
+      "head": "5ccad6aa04409ee2805d5638aa0fc84c76bbb881",
+      "author": "Aaron Wang with opencode",
+      "pr": 2518,
+      "path": "research/polar-law-t7-overcomplete-screen/search.py",
+      "retained": "references/PR2518-search.py",
+      "sha256": "c0335db5753be6535b25ece1dc14ed61e7688f20ce17180a4316a172e23d47fd",
+      "git_blob": "019540d5a75b17a606007131cb87e6181934fad5"
+    },
+    {
+      "head": "5ccad6aa04409ee2805d5638aa0fc84c76bbb881",
+      "author": "Aaron Wang with opencode",
+      "pr": 2518,
+      "path": "research/polar-law-t7-overcomplete-screen/README.md",
+      "retained": "references/PR2518-README.md",
+      "sha256": "ed9c61d8616fa4bc86a9d28d66f49aa774ef25fe56a4e3c895b69bf784e7880f",
+      "git_blob": "3d7a42855310f5251452bdb003300275b538efc3"
+    },
+    {
+      "head": "ca7f99921f03398d303bba90245d3ee2e38e95c3",
+      "author": "DreamingOfClouds",
+      "pr": 2277,
+      "path": "research/overcomplete-and-realisation-floors/README.md",
+      "retained": "references/PR2277-README.md",
+      "sha256": "1a11f33a8d358479cae0f39018fa9ebd3d439790cd1872de91d109fd4d23a088",
+      "git_blob": "02660b10d4f48cd39db3416def50cd944aef4ac9"
+    }
+  ]
+}

research/dn-unrestricted-root-code-floor/README.md

@@ -0,0 +1,244 @@
+# Full D_n root-code decoders cannot beat n(n-1)
+
+For every n >= 4, over every field K of characteristic other than two,
+the full dense D_n root-code Gram decoder has minimum algebraic rank cost
+**n(n-1)**, even when an arbitrary finite number of rank-one terms is allowed.
+The coordinate Gram expansion attains the floor. Every optimal expansion
+has exactly n nonzero terms. This does not classify its possible bases.
+
+The decision is to retire attempts to improve the coordinate bill by adding
+terms in this precise full-root-code model. Sparse pairings, punctures,
+factors outside the root code and different realizations change the premise.
+This is a written uniform proof with finite cross-checks, not a new physical
+decoder, Lean theorem, supplier or multiplication bound.
+
+## Priority and exact source contract
+
+DreamingOfClouds's [PR2228](https://github.com/CrocSwap/integer-mult-bounds/pull/2228)
+already settles D4 and D6 at every term count, and establishes the support
+deficiency method. Their [PR2277](https://github.com/CrocSwap/integer-mult-bounds/pull/2277)
+at `ca7f99921f03398d303bba90245d3ee2e38e95c3` settles D5 at every term count
+and supplies the overcomplete coupling lemma used below. Those individual
+floors and the coupling lemma retain that priority. Aaron Wang's
+[PR2518](https://github.com/CrocSwap/integer-mult-bounds/pull/2518) at
+`5ccad6aa04409ee2805d5638aa0fc84c76bbb881` gives the exact D generator and
+bounded overcomplete searches. Its generator uses twice the roots below;
+this common nonzero scale changes neither supports nor the argument.
+
+Our earlier [PR2659](https://github.com/CrocSwap/integer-mult-bounds/pull/2659)
+addresses only a fixed-coordinate one-extra update family. The present
+result allows arbitrary factors and arbitrary finite term counts in every
+dimension n >= 4. PR2582's uniform B_n/C_n proof concerns different roots;
+we do not count those floors again. The new contribution is the uniform
+D_n support classification and its all-term conclusion, including the
+odd-dimensional case where an unmatched axis term is cheaper.
+
+Original PR2277 and PR2518 READMEs and the unchanged PR2518 generator are
+retained with exact head, blob and SHA-256 pins in `DEPENDENCY.json`.
+Authentication precedes extracting only the source's canon/lines/D functions.
+No modified upstream file or selected record is used.
+
+Let R have one row r_(ij,+)=e_i+e_j and r_(ij,-)=e_i-e_j for every i<j.
+There are v=n(n-1) rows. The fixed binary matrix B has a one on its diagonal
+and between orthogonal real root lines, and zero elsewhere. This definition
+uses the integer root pattern even if K has positive characteristic.
+An allowed expansion is
+
+    R R^T = sum_j (R x_j) (R y_j)^T,    x_j,y_j in K^n,
+    cost = sum_j rank_F2 B[supp(R x_j), supp(R y_j)].
+
+The transpose is bilinear, not Hermitian. Zero outer factors may be removed;
+m always counts nonzero terms. Since 2 is invertible, the two signs on an
+edge span its coordinate axes, so R has full column rank. Left and right
+inverses show that exactness is equivalent to sum_j x_j y_j^T=I_n.
+The same theorem holds after fixed invertible diagonal scaling of the rows
+and the corresponding Gram matrix. Neither arbitrary non-root-code factors
+nor a changed binary mask is covered.
+
+## Binary support classification
+
+Both signs on an edge have the same B row. Deleting repeated rows/columns
+preserves binary rank. Put
+
+    E = {s in F2^n : sum_i s_i=0},  L=F2 direct-sum E,
+    u_ij=(1,e_i+e_j),  Omega((a,s),(b,t))=a b+s dot t.
+
+Then B is the Omega Gram matrix of the edge labels: its entry is one for
+equal/disjoint edges and zero for distinct edges sharing one vertex.
+The labels span L: the sum of a triangle's three labels is (1,0), and
+adding that vector to each label gives (0,e_i+e_j), which span E.
+The radical of Omega on L is zero for odd n, and is generated by
+(0,(1,...,1)) for even n. Consequently
+
+    h=rank_F2 B = n (n odd), or n-1 (n even).
+
+Work in the nondegenerate quotient V=L/rad(Omega). Its binary code consists
+of c_(a,s)(ij,+)=c_(a,s)(ij,-)=a+s_i+s_j with s in E, modulo the radical.
+For a root-code support S, let delta(S) be the dimension of codewords
+vanishing on S. Equivalently it is the codimension in V of span{u_e:e in S}.
+
+For x nonzero, a codeword c vanishes on supp(Rx) precisely when every edge
+with c(e)=1 has both x_i+x_j=0 and x_i-x_j=0. These equations force
+x_i=x_j=0. Thus every nonzero coordinate of x must be an isolated vertex
+of the graph whose edges satisfy c(e)=1.
+
+Suppose vertex i is isolated. For j != i, s_j=a+s_i. If a=0 then all s_j
+are equal and c is the zero codeword. If a=1 then c is the complete graph
+on the other n-1 vertices, with i its unique isolated vertex. The condition
+s in E permits this exactly when n is odd: it forces s_i=0 and all other
+s_j=1. (For even n the parity is always one.) Therefore
+
+* Even n: delta(supp(Rx))=0 for every nonzero x.
+* Odd n: delta(supp(Rx))=1 exactly when x is a nonzero coordinate-axis
+  vector; it is zero otherwise. For each axis the deficient code space
+  has exactly one nonzero word.
+
+For two supports S,T, nondegeneracy gives
+
+    rank B[S,T] >= h-delta(S)-delta(T).
+
+Indeed the left-label span has dimension h-delta(S); the kernel of its
+pairing with the right-label span lies in the latter's annihilator, of
+dimension delta(T). This also proves that when both deficiencies are zero
+the rectangle has rank h.
+
+For odd n the exact term costs are:
+
+| x,y | rank cost |
+|---|---:|
+| Neither is an axis | n |
+| Exactly one is an axis | n-1 |
+| Both lie on the same axis | n-1 |
+| They lie on distinct axes | n-2 |
+
+An axis support compresses to its n-1 incident edges. Its principal
+rectangle is I_(n-1), giving the first relevant upper bound and same-axis
+value. For two distinct axes, put their common edge first. The rectangle
+is 1 direct-sum (I_(n-2)+J_(n-2)). When n is odd, n-2 is odd, and the
+second block has precisely the all-ones kernel. This gives n-2. For even
+n every nonzero term instead has rank n-1 by the zero-deficiency result.
+
+## All numbers of terms
+
+Rank of the exact sum forces m>=n. Even n is immediate: every nonzero term
+costs n-1, so the total is m(n-1), strictly above the floor if m>n.
+
+Now let n be odd, hence n>=5. Call a term *cheap* when its cost is n-2.
+The table says these are exactly x_i=alpha_i e_(a_i),
+y_i=beta_i e_(b_i), with a_i != b_i and both scalars nonzero.
+
+If m=n, write X=[x_1 ... x_n] and Y=[y_1 ... y_n]. Exactness gives
+X Y^T=I, hence Y^T X=I. In particular y_i dot x_i=1, excluding cheap
+terms. The total is at least n(n-1).
+
+If m=n+1, use the credited overcomplete coupling lemma from PR2277:
+for K=Y^T X there are column vectors u,w such that
+
+    I-K=u w^T,  w^T u=1.
+
+For completeness, K is idempotent of rank n: X K=X and X has rank n.
+Thus I-K has rank one. A nonzero column factors it as u w^T, and its
+idempotence implies w^T u=1. For a cheap index i, K_ii=0, so u_i w_i=1.
+For distinct cheap indices i,j this forces K_ij=-u_i w_j != 0. But
+K_ij=y_i dot x_j is nonzero only if b_i=a_j. Three cheap indices i,j,k
+would give a_j=b_i=a_k and a_i=b_j=a_k, making a_i=b_i, a contradiction.
+There are therefore at most two cheap terms. Every other term costs at
+least n-1, and the total is at least
+
+    (n+1)(n-1)-2 = n^2-3 > n(n-1).
+
+If m>=n+2, even the crude per-term floor gives
+
+    m(n-2) >= (n+2)(n-2) = n^2-4 > n(n-1).
+
+Finally, x_i=y_i=e_i gives n principal star rectangles I_(n-1), attaining
+n(n-1). All inequalities for m>n are strict, as claimed. The one-extra
+bound n^2-3 is only a sufficient lower bound, not an asserted exact minimum.
+The n>=4 restriction matters to this proof: for n=3 its last displayed
+count is only 5<6. No counterexample or all-term statement for D3 is claimed.
+
+## Evidence and falsification
+
+The written proof establishes arbitrary dimension, field and term count.
+`RESULT.json` records bounded, exact checks of the actual source-generated
+roots, binary label/radical and support ranks, and exact Gram expansions.
+The checks enumerate every label codeword for n=4..12, compare 583,115
+support pairs over Q, F3 and F5 for n=4..7, and replay 366 exact expansions
+for n=4..9. These include nonintegral reciprocal factor scalings, mixed
+bases, cancelling cheap terms, and actual one-extra words with two cheap
+terms. The independent checker covers 1,482 axis rectangles for n=4..16
+and 208,348 possible cheap-triple extensions for n=3..16.
+The primary checker uses bit-vector binary elimination and actual root
+evaluations. The independent checker constructs the mask directly from
+edge intersections and uses a separate matrix elimination routine; it also
+enumerates the necessary axis relations for hypothetical cheap triples.
+Neither treats a finite search as proof of the uniform theorem.
+
+Controls demonstrate that characteristic two destroys the root-code
+injection, sparse identity masks change the term tariff, unmatched axes
+really are cheaper, an inexact cheap term does not supply I, and the
+small-dimensional counting boundary cannot be silently generalized.
+Export tests check optimized Git-free replay, source corruption rejection,
+typed receipt mismatch and refusal to overwrite an existing output.
+
+From the repository root, standard-library Python 3.12:
+
+```sh
+python3 -I -B scripts/research_package.py --package research/dn-unrestricted-root-code-floor
+python3 -I -B scripts/research_package.py --package research/dn-unrestricted-root-code-floor --check-only
+```
+
+Default verification compares the complete typed receipt and writes no
+files. `python3 -I -B research/dn-unrestricted-root-code-floor/verify.py
+--output NEW.json` creates a new receipt and refuses an existing path.
+The package works without Git when exported with its declared input.
+No Lean replay, native circuit replay or selected full cold replay is claimed.
+
+## Family decision and obligation ledger
+
+The priority-5 picker first selected P104-side-correction on main
+`6bd33bc0b87a01e9c9d8b1c01576f3ddbcaee850`; its binding baseline passed.
+`TASK.json` records the changed assignment to the suggested decoder-bound
+track after crowded P104 obligations were checked. The precise question
+is an all-dimension/full-code rejection, not another seeded search.
+
+The final checkpoint fetched canonical main `c3c94c2ea2ebcd5d69d1e51b5fe8a36bf79819f5`;
+guidance, family gate and selected record were unchanged. Both scientific
+predecessor heads above were rechecked unchanged. Overlap coverage included
+767 open PRs at 18:06Z and 1,239 Discussion records at 15:22Z on 2026-10-15,
+plus the newest 100 open PRs checked at 18:16Z and retained local notes.
+Later Discussion claims and arbitrary code diffs are not covered; absence
+of a search match is not a novelty certificate. Coordination is recorded
+on [PR2277](https://github.com/CrocSwap/integer-mult-bounds/pull/2277#issuecomment-6198818270).
+
+**Decision: reject improvements inside this full dense root-code family.**
+The floor already equals the number of ports. Overcomplete factors cannot
+save its algebraic rank mass. Stop larger searches in this same family;
+reopen only with a stated changed mask, root set, factor space or realization.
+
+| Obligation | Status |
+|---|---|
+| Exact root-code Gram identity | The hypothesis sum xy^T=I is necessary and sufficient |
+| Every term's binary rank charge | Proved uniformly; no omitted zero/cheap terms |
+| Arbitrary finite term count | Proved; nonzero optimum uses exactly n terms |
+| Source generator and predecessor binding | Pinned and authenticated |
+| Physical frames, dirty restoration, hosting, precision, all-size budget | Not supplied; unknown, not zero |
+| Changed global kappa or selected frontier | None |
+
+The next consumer is a researcher considering dense-root-code synthesis:
+use this result to rule out that family before paying for a larger census.
+The algebraic result alone makes no runtime or physical allocation claim.
+
+## Open next questions
+
+Which specific punctured or sparse D_n pairing changes this floor enough
+to survive a fully charged decoder/hosting budget? First identify a mask
+outside the full dense theorem and a complete intended consumer; do not
+reuse its full-mask tariff after removing constraints. Physical admissibility
+and the complete downstream cost remain unresolved here.
+
+Prepared for ywz65 with substantial OpenAI Codex assistance. DreamingOfClouds
+retains priority for the deficiency method, overcomplete coupling lemma and
+the D4/D5/D6 all-term results; Aaron Wang with opencode retains credit for
+the PR2518 generator and finite screens. Copied artifacts retain their
+original attribution and Apache-2.0 provenance.