Prove P112 six-dimensional incidence floor and exclude two literal C5 callers

research/p112-six-dimensional-incidence/CHECKS.json

@@ -0,0 +1,15 @@
+{
+  "environment": "3.12.3",
+  "primary": "Exact rational rank2/3 closure census passed; independent modular101 full closure census also matched during exploration, not part of the registered final verification contract.",
+  "independent": "23 positive definite Gram3 patterns/2875 integral targets;393 Gram4 patterns/245625 integral targets, max12 lines and complete case digest independently agree.",
+  "controls": "Meaningful boundary, actual-code, characteristic and optimized receipt-mutation checks.",
+  "unrun": [
+    "Selected cold replay",
+    "Lean or proof-kernel formalization",
+    "Docker",
+    "Full historical predecessor censuses",
+    "Human mathematical review"
+  ],
+  "scope": "Fresh local checks; committed-source/history/export verification and hosted CI are reported separately in PR/handoff.",
+  "peer_review": "Separate agent checked arbitrary characteristic-zero scalar transfer, singleton active-set counting, exact quotient, pair-incidence algebra and Gram3/4 certificates. No human/formal review."
+}

research/p112-six-dimensional-incidence/PREDECESSORS.json

@@ -0,0 +1,29 @@
+{
+  "canonical_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "credits": [
+    {
+      "contributor": "Nick Petalas",
+      "pr": 3269,
+      "commit": "ebe02d33157dc6c6d3b35df204e4a39242b7429e",
+      "role": "Inherited binary support capacities12/20; analytic proof retained as canonical input."
+    },
+    {
+      "contributor": "Nick Petalas",
+      "pr": 3300,
+      "scientific_commit": "4c811083d1a4a7cb084b9d972ac8e8f1c843cba9",
+      "public_head": "cd2cab515db136d7eb49242fc1111299f28a53a8",
+      "role": "Inherited binary rank7 support capacity36; analytic proof retained as canonical input."
+    },
+    {
+      "contributor": "DreamingOfClouds",
+      "pr": 3154,
+      "commit": "708f0ad8928c383de8294aea3c126e9461d2066d",
+      "role": "Historical TWOSIDE callers and generalized-weight context; original filter retained on main."
+    },
+    {
+      "contributor": "Nick Petalas; David Arias; joaqcoo and retained E8/P112 lineage",
+      "role": "Root-simplex coordinates, quadratic-model interpretation and decoder context; predecessor notices preserved."
+    }
+  ],
+  "new_contribution": "Root-matroid fiber incidence floor with common-zero charging; two literal maximal profile applications, not a first-exclusion or current-residue-count claim."
+}

research/p112-six-dimensional-incidence/PROOF.md

@@ -0,0 +1,232 @@
+# Six code dimensions force a support-incidence bill
+
+Let K be any characteristic-zero field. Let P be the fixed 112 doubled E8
+root lines in the declared P112 convention, and let
+
+    C = {(r dot h)_(r in P) : h in K^8}.
+
+For arbitrary vectors p_1,...,p_n in K^112 suppose their span contains a
+six-dimensional subspace D of C. Independence of the pieces is unnecessary.
+Write M=sum_i |supp(p_i)|, and let z coordinates vanish on every word of D.
+We prove both
+
+    M >= 224 - 6n + (n-2)z,                      (1)
+
+    M >= ceil(((2n-3)(112-z) - binomial(n,2)(12-z))/(n-2)).   (2)
+
+In particular eleven pieces require at least 164+4z, hence164, total support incidences.
+Consequently the literal historical TWOSIDE (b,t)=(6,5) profiles 5^10,7 and
+5^9,6^2 are impossible. Their inherited capacity sums are156 and148, giving
+strict contradiction margins 8 and 16. The profiles 5^11 and5^10,6 follow by
+componentwise domination. This is not an assertion that these four profiles
+were the only public residues, or a full reconciliation of the174 historical
+survivors in that cell.
+
+## The pairing of mathematical viewpoints
+
+Generalized Hamming weights constrain how many coordinates can vanish on a
+code subspace. The additional datum here is the size of each projective fiber
+of the evaluation map, which is controlled by a contraction of the rational
+root matroid. Singleton support incidence then combines the common zero set
+with all fibers at once. Charging their shared zero roots is what sharpens
+the naive bound using d_6>=109 from 152 to 158 at n=11. Pair incidence
+then improves the uniform bill further to 164, a gain of twelve over that
+naive relaxation. No common-cut extension,
+new high-dimensional binary-flat census or Weyl-chamber assumption is needed
+for the new incidence theorem.
+
+## Root-matroid capacity in rational rank three
+
+Every subset of full E8 root lines whose rational span has dimension at most
+three contains at most six lines. The primary certificate enumerates every
+pair and triple of the 120 root lines using exact primitive integer RREF.
+There are 7,140 independent pairs and 279,720 independent triples. Grouping
+bases by their rational span yields:
+
+| Rank | Distinct root-spanned flats | Closure-size histogram | Maximum |
+|---|---:|---|---:|
+| 2 | 4,900 | 2:3,780; 3:1,120 | 3 |
+| 3 | 85,680 | 3:37,800; 4:40,320; 6:7,560 | 6 |
+
+Each closure is the union of the roots occurring in its bases. This is complete:
+any root belonging to a root-spanned flat extends to a basis of that flat.
+The root shell has rank eight, so smaller root-spanned spaces can also be
+extended to a three-root span. Arbitrary ambient subspaces contain no more
+roots than the root-spanned subspace generated by their contained roots.
+The receipt binds all closure masks by canonical SHA256 and retains extremizers.
+
+There is also a much smaller independent integer certificate. Normalize root
+norms to two. Three independent roots have Gram matrix
+
+    G = [[2,a,b],[a,2,c],[b,c,2]],    a,b,c in {-1,0,1}.
+
+Positive definiteness gives det(G)=8+2abc-2(a^2+b^2+c^2)>0. Exactly 23 of the 27
+patterns qualify. For a root r in their span, its integral inner-product
+vector k lies in {-2,-1,0,1,2}^3 and satisfies
+
+    k^T adj(G) k = 2 det(G).
+
+The root is uniquely determined by k because the Gram matrix is invertible.
+Enumerating 23*125=2,875 possibilities gives signed-vector counts 6,8,12 with
+pattern multiplicities 1,6,16. Thus at most 12 signed roots, or six lines, occur.
+This argument is an upper bound: no claim that every enumerated k represents
+an actual E8 root is necessary. The separate checker imports neither the
+primary exact-elimination code nor the source geometry module. A separate
+review agent derived this Gram certificate while auditing the argument; this
+is computational and conceptual corroboration by the same assisted team,
+not independent human review or a formal proof-kernel check.
+
+## Root-matroid capacity in rational rank four
+
+The analogous uniform bound in dimension four is twelve root lines. Choose
+four independent roots and form their norm-two Gram matrix, with six free
+entries in {-1,0,1}. All 729 matrices are tested; Sylvester's criterion
+requires every leading principal minor to be positive, not just the determinant.
+Exactly 393 patterns survive. For each, enumerate all 625 integral vectors
+k in {-2,-1,0,1,2}^4 and retain k^T adj(G) k=2 det(G). The complete signed
+count histogram is10:12,12:12,14:64,20:200,24:105. Thus at most24 signed
+roots, or twelve root lines, fit into the span. Smaller root-spanned spaces
+extend to a four-root span, as the full shell has rank eight.
+
+The primary computes determinants by fraction-free Bareiss elimination; the
+separate checker uses the permutation formula, with a separately constructed
+Gram matrix. Both cover all 393*625=245,625 integral targets and agree on the
+canonical case digest. The characteristic-zero inference uses rational rank
+preservation, just as for the three-dimensional bound. The primary separately
+authenticates all distinct full-root inner products as -4,0,4 in doubled
+coordinates, so the normalized integral-pairing alphabet is source-bound.
+The actual twelve-root D4 coordinate section is an attaining control and
+also shows why the rank-three bound cannot be reused in dimension four.
+
+## Scalar extension and the common zero set
+
+Evaluation on P is injective: the live doubled-root Gram sum is 112 I_8.
+Choose independent normals h_1,...,h_6 whose codewords form a basis of D,
+and define E:K^8 -> K^6 by E(r)=(r dot h_j)_j. Its rank is six and its
+kernel has dimension two. Let Z={r in P:E(r)=0} and z=|Z|.
+
+A rational root matrix has the same rank over Q and over K. A rational minor
+nonzero over Q remains nonzero over characteristic zero; vanishing minors
+remain zero. Therefore the roots in Z have rational rank at most two and
+z<=3 by the rank-two certificate. This uses no embedding of K into R and
+makes no rationality assumption about h_j or their coefficients.
+
+Express each of the six chosen codewords as a linear combination of the n
+pieces. For piece i let v_i in K^6 be its six coefficients. At a coordinate
+r where exactly piece i is nonzero, E(r)=p_i(r)v_i. Count such a coordinate
+as an active singleton only if E(r) is nonzero. Let s_i be the number of
+active singletons of piece i.
+
+If v_i=0, then s_i=0. Otherwise every singleton root of piece i, together
+with every root in Z, lies in E^{-1}(K v_i). This preimage has dimension
+2+1=3. By rational rank preservation its rational roots have rank at most
+three, hence
+
+    s_i + z <= 6.
+
+The same inequality holds when v_i=0 because s_i=0 and z<=3. Crucially, Z
+is the same set for every piece. Projective fiber bounds for separately
+chosen code subspaces would not establish this simultaneous inequality.
+
+## Incidence count
+
+There are 112-z active coordinates. An active singleton consumes one piece
+incidence; every other active coordinate consumes at least two. Arbitrary
+cancellations are permitted. Therefore
+
+    2(112-z) <= M + sum_i s_i <= M+n(6-z).
+
+Incidences outside the active set only increase M and have not been silently
+removed. Rearranging proves(1). Because n>=6 and z>=0 it implies M>=224-6n.
+
+The weak route using only generalized support weight d_6>=109 and the
+unadjusted fiber bound six gives M>=218-6n, or152 at n=11. That relaxation
+does not exclude capacity156. Counting common zero roots in every fiber
+raises the necessary bill to 158, a measurable improvement of six incidences before the pair strengthening.
+Neither incidence formula is asserted to be attained by actual pieces.
+
+## Pair incidence raises the eleven-piece floor to 164
+
+For each unordered pair of piece indices i,j, every active coordinate whose
+nonzero pieces are contained in that pair has evaluation in span_K(v_i,v_j).
+Together with Z, these roots lie in its inverse image under E, of dimension
+at most2+2=4. This remains valid for zero or proportional coefficient columns.
+The rank-four bound therefore gives at most 12-z such active coordinates per
+pair.
+
+Let u,v,w count active coordinates of piece multiplicity exactly one,
+exactly two, and at least three. Then N=112-z=u+v+w. Summing the pair bound
+counts each singleton n-1 times and each doubleton once, yielding
+
+    (n-1)u+v <= binomial(n,2)(12-z).
+
+Substitute v=N-u-w. The exact rearrangement is
+
+    (n-2)u-w <= binomial(n,2)(12-z)-N.
+
+Since n>=6 and w>=0, it implies the weaker but useful bound
+
+    (n-2)(u-w) <= binomial(n,2)(12-z)-N.
+
+Meanwhile M>=u+2v+3w=2N-u+w. Substitution proves(2); M is an integer so the
+ceiling is legitimate. With eleven pieces this reads
+
+    M >= ceil((1468+36z)/9)=164+4z.
+
+No integrality or sign condition is imposed on piece coefficients. Multiple
+nonzero pieces can cancel at a coordinate, and all such costs are retained
+or omitted only in the direction that weakens the lower bound. Pair incidence
+is an additional constraint on this same actual caller, rather than an
+extension to a different cut budget or a larger historical multiset census.
+The parent coordination agent proposed this strengthening and the separate
+conceptual-review agent independently checked the inequality and all 393 Gram
+patterns. The registered primary and separate checker reproduce the result.
+
+## Literal caller and quotient binding
+
+Use the inherited binary support capacities g(5)=12,g(6)=20,g(7)=36 for the
+leading-one labels of the pinned geometry. Their analytic source proofs are
+explicit inputs; their large historical censuses are not replayed here.
+The original independent pieces span T, with dim(T intersect C)>=6.
+There are eleven pieces, so the quotient Q=T/(T intersect C) has dimension
+at most five. To bind the exact quotient, choose six rank-five pieces. Their
+union has size at most 72<d_2(C)=78. The inherited second generalized-weight
+bound implies their six-dimensional span meets C in dimension at most one.
+Their quotient images thus span dimension at least five. Consequently
+
+    dim Q=5,     dim(T intersect C)=6.
+
+This exact-quotient conclusion inherits d_2>=78; the new incidence contradiction
+only needs the original at-least-six intersection hypothesis and does not
+depend on that extra quotient calculation. The five smallest individual
+capacity sums equal 60, above distance 53, so a strict-below-distance quotient
+basis certificate is unavailable from those sums alone. No lower bound on
+actual support union is inferred.
+
+For 5^10,7, the strict excess is10*3+5=35<36, and M<=10*12+36=156<164.
+For 5^9,6^2, the excess is9*3+2*4=35<36, and M<=9*12+2*20=148<164.
+Both pass the original PR3154 necessary filters; the primary reimplementation
+and separate execution of its unchanged feasible/killed functions agree.
+We bind these two literal rows only, not a new exhaustive current frontier.
+
+## Dependencies, credit and remaining obligations
+
+The new support-incidence theorem is supplied by the written linear algebra
+and the two bounded exact root-capacity certificates. Its literal weight
+applications inherit Nick Petalas's global quadratic support capacities12/20,
+the retained rank-seven capacity36 proof and the declared label convention.
+The quotient annotation and historical survivor status retain
+DreamingOfClouds/PR3154's generalized-weight and TWOSIDE context. Credit also
+stays with the root-simplex geometry lineage, David Arias's quadratic-model
+work, joaqcoo and all named predecessors in their retained sources.
+SOURCES.json pins every input to canonical main20ecf2891d80b5acf18d980b2164fb44ea7faa90.
+Predecessor packages are unchanged. Substantial OpenAI Codex assistance was
+used; new work is Apache-2.0.
+
+This is a local C5 caller exclusion and a reusable incidence inequality. Full
+C5, a global decoder lower bound, physical realization, supplier admission,
+complete multiplication theorem and a kappa increase do not follow. Excluding
+an optimistic low-cost decoder shape does not construct a cheaper decoder.
+The selected conditional kappa remains 0.001672660197076918. Human or formal
+acceptance, complete historical/current caller reconciliation and constructive
+cost improvements remain separate obligations.

research/p112-six-dimensional-incidence/README.md

@@ -0,0 +1,71 @@
+# Six code dimensions force 164 support incidences at eleven pieces
+
+For arbitrary pieces spanning a six-dimensional subspace of the characteristic-zero
+P112 root-evaluation code, the total support-incidence bill satisfies
+
+    sum_i |supp(p_i)| >= 224 - 6n + (n-2)z,
+
+where z is the number of coordinates vanishing on that same code subspace.
+A pair-incidence strengthening gives
+
+    sum_i |supp(p_i)| >= ceil(((2n-3)(112-z)-binomial(n,2)(12-z))/(n-2)).
+
+In particular eleven pieces require at least 164+4z, hence164, incidences. This excludes the
+literal historical (6,5) profiles 5^10,7 and5^9,6^2, whose inherited support
+caps total156 and148. Their exact quotient is five-dimensional and their
+code intersection is six-dimensional under the stated inherited second-weight
+bound. The contradiction itself only requires six code dimensions.
+
+[PROOF.md](PROOF.md) pairs generalized Hamming weights with rational root-matroid
+contraction fibers and singleton incidence. Charging common zero roots raises
+the naive152-incidence floor to 158, and pair incidence strengthens this
+to 164. The first named caller is excluded with margin eight. The dominated profiles 5^11 and5^10,6 also follow. No complete
+current residue count or first-exclusion claim is made.
+
+The primary checks all 4,900 rank-two and 85,680 rank-three root-spanned flats
+using rational elimination. The separate checker proves the needed cap of six
+root lines through 23 integral rank-three Gram patterns and 2,875 target vectors.
+All 393 positive definite rank-four Gram patterns, covering 245,625 integral
+targets, independently certify the pair-fiber cap of twelve root lines.
+It imports no primary geometry or elimination code. Both literal profiles
+pass the unchanged original PR3154 necessary filter. A separate team agent
+critiqued the scalar-extension/common-zero argument and supplied the Gram
+certificate; this is assisted-team corroboration, not independent human or
+proof-kernel acceptance.
+
+## Reproduce
+
+From the repository root, with Python3.12 and its standard library:
+
+```sh
+python3.12 -I -Werror -B scripts/research_package.py --package research/p112-six-dimensional-incidence
+```
+
+The registered commands are also directly runnable in the official Git-free
+export. Normal replay is read-only; only `verify.py --write-expected` regenerates
+the receipt. `SOURCES.json` authenticates every canonical-main input; the
+historical filter is reused for binding and the capacities remain inherited
+proof dependencies. The bounded root-capacity theorem itself needs neither a
+Weyl-chamber theorem nor an embedding of the coefficient field into the reals.
+
+## Open next questions
+
+First independently audit the common-zero charging and the characteristic-zero
+rank transfer. A further application should name an actual caller whose total
+support cap reaches164 and identify additional multi-piece incidence structure.
+The uniform bound's attainability and such a caller are not established here;
+a larger census is not automatically warranted.
+
+This local C5 progress does not construct a cheaper decoder or improve kappa.
+Full C5, physical supplier admission, the full multiplication theorem and
+human/formal acceptance remain open. The selected conditional kappa remains
+0.001672660197076918.
+
+## Credit
+
+Nick Petalas/PR3269 and3300 supply the inherited12/20/36 capacities;
+DreamingOfClouds/PR3154 supplies the historical reduction. Retain the
+root-simplex lineage, David Arias's quadratic-model work and joaqcoo's decoder
+context. Exact source pins and scope distinctions are in `PREDECESSORS.json`
+and `SOURCES.json`. Chris R / Clear1nsight with substantial OpenAI Codex
+assistance. Apache-2.0. Predecessor packages and selected artifacts are unchanged.