Prove common30 P112 span bound and exclude the 2^5,6,7^5 caller

research/p112-common30-span/PREDECESSORS.json

@@ -0,0 +1,89 @@
+{
+  "schema_version": 1,
+  "pins": [
+    {
+      "number": 3154,
+      "head": "708f0ad8928c383de8294aea3c126e9461d2066d",
+      "title": "C(P112) >= 64: complete reduction to stated conjectures",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3154",
+      "state": "open",
+      "merged": false,
+      "author": "DreamingOfClouds",
+      "role": "Original TWOSIDE/C5 and necessary filter, retained by PR3282; original author DreamingOfClouds."
+    },
+    {
+      "number": 3163,
+      "head": "89419106cd86896c366e853795978f1bc85f9112",
+      "title": "test(research): certify a complete P112 common-deletion slice",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3163",
+      "state": "closed",
+      "merged": true,
+      "author": "petalas",
+      "role": "Complete fixed-first-space shared-four-deletion predecessor; retains the common-set quantifier and full-direction coverage."
+    },
+    {
+      "number": 3269,
+      "head": "ebe02d33157dc6c6d3b35df204e4a39242b7429e",
+      "title": "Prove analytic E8 binary-support capacities 12 and 20",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3269",
+      "state": "closed",
+      "merged": true,
+      "author": "petalas",
+      "role": "Prior global binary support capacities12/20; rank-six20 is rechecked here."
+    },
+    {
+      "number": 3282,
+      "head": "9607079de93907d87e6430d6de154f21a66c03e4",
+      "title": "Certify source-bound P112 caller coverage for the (6,4) cell",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3282",
+      "state": "closed",
+      "merged": true,
+      "author": "petalas",
+      "role": "Canonical retention of original filter and TWOSIDE note; conditional caller-inventory predecessor."
+    },
+    {
+      "number": 3289,
+      "head": "e8570c50f9591c9ca653a527ed9626aaa703c3bc",
+      "title": "Reconcile original P112 cover contracts for three caller rows",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3289",
+      "state": "closed",
+      "merged": true,
+      "author": "petalas",
+      "role": "Original cover and quotient-composition predecessor, not a claim about the present public frontier."
+    },
+    {
+      "number": 3931,
+      "head": "33b6be488be1e9e38f2f3f9bcfc4a7db0e8a332d",
+      "title": "Exclude a historical C5 caller with a common-cut23 bound",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3931",
+      "state": "open",
+      "merged": false,
+      "author": "Clear1nsight",
+      "role": "Same donor's prior common23 bound and different caller. Adjacent ten-piece cut22 reuse is credited, not a new geometric result."
+    },
+    {
+      "number": 3951,
+      "head": "9aacf01037f6e19cabb95ccbea15fcc2965dcd4d",
+      "title": "Independently audit inherited P112 support and A2 bounds",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3951",
+      "state": "open",
+      "merged": false,
+      "author": "Clear1nsight",
+      "role": "Same donor's preceding dependency audit and chamber/field argument. model.py is explicitly adapted from its table model; the new core is separate."
+    }
+  ],
+  "geometry": {
+    "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3164",
+    "head": "857384079ab640a949fb7618b7909664d3e737e5",
+    "author": "Nick Petalas",
+    "role": "Root-simplex/geometry lineage, literal simple-system definition retained in canonical main."
+  },
+  "runtime": "All executable inputs resolve at canonical main20ecf289. No pending predecessor Git object or executable is required. The primary executes only the authenticated original filter definitions for the literal caller.",
+  "new_pending_predecessor": {
+    "pr": 3960,
+    "head": "7e8d98e351ac153d81943218bf168dc8548b1cea",
+    "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3960",
+    "role": "Common24 result and actual cap30 handoff; model.py and independent shell/Cramer reconstruction explicitly adapted; new graph and common30 theorem here."
+  },
+  "status_scope": "Historical predecessor metadata retained from PR3960; exact heads/roles are bindings, not a refreshed scientific acceptance claim."
+}

research/p112-common30-span/PROOF.md

@@ -0,0 +1,168 @@
+# Common30 rank-seven span and one literal C5 caller
+
+Fix the full 120 doubled E8 root lines R, oriented by first nonzero coordinate,
+the frame F={2e_0 +/- 2e_1,...,2e_6 +/- 2e_7}, and P=R\F. The original table
+orders P lexicographically. Labels are ell(r)=(1,c(r) mod2) in F2^9 for the
+pinned integral simple coordinates. Binary support weight is the rank of
+these labels, rather than the number of support sites.
+
+For a characteristic-zero field K let C={c_h:h in K^8}, c_h(r)=r dot h on P,
+and write Off(h) for its nonzero support.
+
+**Theorem.** Under ONE fixed S subset P of size at most30, the normals h with
+rank_F2 ell(Off(h)\S)<=7 span a K-space of dimension at most **three**.
+An explicit independent triple at a common cut of size30 attains three.
+Moreover, for |S|<=29 there are at most **two projective normal directions**.
+These are universal common-cut statements, allowing arbitrary S and arbitrary
+characteristic-zero coefficient fields.
+
+**Literal caller.** The eleven collectively independent pieces with binary
+weights 2,2,2,2,2,6,7,7,7,7,7 cannot have code-intersection dimension at least5.
+This is the named historical TWOSIDE (b,t)=(5,6) profile, not the whole C5
+problem, a decoder theorem, supplier admission or a selected-bound change.
+
+## 1. Reduction to all120 root normals, including the frame
+
+The table and simple coordinates are authenticated against canonical main.
+The model checks the 56 two-coordinate and64 all-odd root-line patterns,
+exact coordinate equations, signs, original112 labels, and the live Gram
+matrix112I. Thus evaluation is injective over every characteristic-zero K.
+
+The reversed-pivot RREF enumeration covers every two-dimensional annihilator
+of a seven-space in F2^9 exactly once. All43,435 seven-spaces have full-root
+trace at most36. A qualifying direction consequently satisfies
+
+    |Off(h)| <= 30+36 = 66 < 70.
+
+Here are the full-root chamber and field arguments, adapted with credit from
+PR3951/3960. The eight simple reflections permute the240 signed roots; they
+therefore generate a finite group, since their action on a spanning set is
+faithful. Solve rationally for rho dot alpha_i=1. For a real normal v maximize
+rho dot g(v) over the finite group. Any negative simple pairing would make a
+simple reflection increase the functional. The maximizing normal is in the
+closed chamber. Every positive root has nonnegative simple coordinates, so
+its pairing vanishes exactly when its support is in the zero simple nodes.
+The zero roots form the corresponding simple face. No Weyl move is assumed
+to preserve the removed frame or the binary labels.
+
+The checked faces on at most six nodes have at most36 root lines. The
+seven-node face counts are42,28,22,14,16,23,37,63; the last has a root normal.
+For a qualifying h in K^8, let Z be the rational span of its perpendicular
+live roots. There are at least112-66=46 such roots. If rank_Q Z<=6, a generic
+real normal to Z avoids every root hyperplane not forced by Z, so its zero
+roots span Z. Its chamber face has rank at most6, contradicting46>36.
+Therefore rank_Q Z=7: rank8 would force h=0 over K by a nonzero rational minor.
+Rational elimination preserves rank under extension to any characteristic-zero
+K, so h is a K-multiple of a rational generator of the one-dimensional kernel.
+That real generator has at least46 perpendicular roots. Only the63-line
+seven-node face can occur because46>42. Reflection transport then identifies
+its normal with one of the120 root lines. This argument requires no embedding
+K into R or C. Direct evaluation gives live-root support53 and frame-root
+support56. The same reasoning applied to a hypothetical support below53
+proves the code distance is53, attained by live root normals.
+
+## 2. Complete completion-cut graph
+
+For a root normal a and binary seven-space V set
+
+    C(a,V) = Off(a) \ Lambda(V).
+
+Normal a qualifies for S exactly when C(a,V) subset S for some V: extend its
+residual label span to a seven-space. Every one of120*43,435=5,212,200 pairs
+is tested. There are24,264 completion records with cut size<=30, and24,264
+distinct (normal,cut) nodes. Their cut-size counts are:
+
+| Size | Nodes |
+|---:|---:|
+| 21 | 336 |
+| 23 | 5,376 |
+| 24 | 504 |
+| 25 | 3,136 |
+| 27 | 10,752 |
+| 28 | 1,024 |
+| 29 | 3,136 |
+
+Join two nodes of distinct normal owners exactly when their cuts have union
+size<=30. Exhaustive pair comparison gives9,828 edges. A collection admitted
+by the SAME S gives a clique and its total cut union has size<=30; pairwise
+compatibility alone is never substituted for this total-union condition.
+
+The primary walks increasing-index cliques while retaining the total union.
+It continues a prefix only when its normals are rationally independent.
+Every independent four-tuple has all its ordered prefixes independent,
+so pruning dependent prefixes cannot omit a four-dimensional witness.
+The full visited counts are:
+
+| Prefix length | Union size | Rational rank | Count |
+|---:|---:|---:|---:|
+| 1 | as above | 1 | 24,264 |
+| 2 | 22,24,25,26,28,29,30 | 2 | 9,828 |
+| 3 | 30 | 2 | 896 |
+| 3 | 30 | 3 | 3,584 |
+| 4 | 30 | 3 | 2,688 |
+
+There is no independent four-prefix. Thus if the qualifying directions for
+an arbitrary S spanned dimension>=4, choosing four independent root normals
+and one contained completion cut for each would produce a visited independent
+four-prefix, a contradiction. Rational ranks of these root vectors equal
+their ranks over K. This proves the common30 span bound.
+
+Every triple of distinct root normals has an independent first pair. All
+admitted triples are consequently visited, including dependent triples.
+Their union size is always30. Hence |S|<=29 permits at most two projective
+normal directions. The listed independent triple at30 also shows that the
+cut allowance29 is maximal for a uniform span-at-most-two statement.
+
+A separate finite-core checker imports neither primary nor predecessor
+executables. It reconstructs the shell, computes integral coordinates with
+Cramer's rule/Bareiss determinants, and enumerates10,795 six-spaces in F2^8
+with four affine cosets each, plus255 leading-zero spaces. All flat,
+completion-record, node and edge digests agree. It directly tests all
+compatible quadruples with total cut union<=30, including those with a
+dependent first triple, using exact Gram determinants rather than the
+primary's rational-elimination/prefix-pruning algorithm. This corroboration
+is within the same donor/assistant context, not independent human or
+formal-kernel acceptance.
+
+## 3. The actual quotient and intersection dimension
+
+Let T be the span of the eleven independent pieces in the stated profile,
+D=T intersect C, and assume dim D>=5. Then dim(T/D)<=6. The first six pieces
+have support union S of size at most5*2+20=30. A binary rank-two support has
+at most2 sites because all labels have leading one. The global rank-six
+capacity20 is credited to Nick Petalas/PR3269 and rechecked here on every
+788,035 binary six-space. Since30<53, every nonzero combination of those
+six independent pieces has support below the code distance and is not a
+codeword. Their quotient images are independent. Thus dim(T/D)=6 and dim D=5.
+
+For each of the five remaining rank-seven pieces q_y, its quotient image
+has a unique representative a_y in the six-piece span. Then c_y=q_y-a_y lies
+in C. These five codewords are independent: their coefficients on the five
+distinct nonbasis pieces are the identity matrix in the original independent
+piece basis. Injectivity of evaluation gives five independent normals h_y.
+Outside the SAME S, their supports lie in support(q_y), so their binary
+support ranks are at most7. The theorem allows span dimension at most3,
+contradicting5. Coefficients, overlaps and cancellations are unrestricted.
+
+The authenticated original PR3154 necessary filter retains the literal list.
+Its strict excess is29<30. All462 six-piece subsets are checked: the minimum
+certified capacity sum is30, attained only by the five rank-two and one
+rank-six pieces. This is not a lower bound on an actual support union.
+
+## 4. Credit and limits
+
+Nick Petalas supplies the global capacities, root-shortening and common-cut
+lineage (including PR3269,3163,3282,3289); DreamingOfClouds/PR3154 supplies
+TWOSIDE/C5; David Arias supplies the quadratic model; joaqcoo and retained
+E8/P112 sources retain their attribution. This donor's PR3951 audits inherited
+bounds and the field step; PR3960 supplies the common24 theorem and two
+other callers. The table model and separate shell/Cramer implementation are
+explicitly adapted from PR3960, and are not claimed newly independent of it.
+The new finite graph, complete common30 span proof and named caller exclusion
+are this package's contribution. Frozen predecessors are unchanged.
+
+No complete cell reconciliation, full C5, complete decoder floor, native
+physical/restoration/consumer/all-size/supplier admission, selected cold
+replay or new kappa is claimed. Written proof and finite computation remain
+subject to mathematical review. Chris R / Clear1nsight, with substantial
+OpenAI Codex assistance, Apache-2.0.

research/p112-common30-span/README.md

@@ -0,0 +1,84 @@
+# P112 common30 span and the literal 2^5,6,7^5 caller
+
+For ONE common set S of at most30 live P112 sites, all characteristic-zero
+normals whose residual support labels have binary rank<=7 span at most
+**three dimensions**. A literal independent triple at30 attains three.
+For |S|<=29 there are at most **two projective directions**. This settles the
+exact relaxed geometric obligation for the historical (b,t)=(5,6) independent
+piece profile **2^5,6,7^5**: six small pieces have support cap30<distance53,
+force quotient dimension6 and intersection dimension5, then the five rank7
+pieces require five independent code directions, contradicting5>3.
+
+[PROOF.md](PROOF.md) supplies the complete root-normal/characteristic-zero
+reduction, finite graph coverage, threshold29/30 and actual quotient transfer.
+[RESULT.json](RESULT.json) stores exact digests, counts, literal normals and
+cut labels. The five-direction caller uses linear independence; a count of
+projective directions alone is not substituted for span dimension.
+
+The finite domain contains43,435 seven-spaces,5,212,200 root/space pairs,
+24,264 completion records and9,828 compatible distinct-owner pairs. All4,480
+admissible triples require cut30;3,584 are independent. The primary traverses
+2,688 four-node extensions of independent triples, all rank3. A separate
+implementation directly checks **all3,360 compatible quadruples**, including
+those with dependent first triples, and finds zero Gram determinants. It
+uses separately coded shell/Cramer labels and affine-generator spaces,
+imports no primary/predecessor executable and matches full record/graph
+digests. This is computational corroboration within one donor/assistant
+context, not independent human or formal-kernel acceptance.
+
+## Reproduction
+
+CPython3.12, standard library only, from the repository root:
+
+```
+python3.12 -I -Werror -B scripts/research_package.py --package research/p112-common30-span
+```
+
+The three explicit optimized commands are in [VERIFY.json](VERIFY.json).
+They read pinned sources and compare results; they do not rewrite evidence.
+The direct scripts also work in a source export with the declared input paths.
+Controls compare the independence-pruned search with a subset oracle across
+all1,024 graphs on five vertices (testing every graph that spans three in this
+fixture); they check a real attaining triple, reject a synthetic independent
+fourth direction, expose the characteristic-two boundary and reject actual
+optimized CLI source/manifest corruption. No selected cold replay, Lean,
+Docker or physical/supplier validation is run.
+
+## Source, scope and overlap
+
+Canonical main20ecf2891d80b5acf18d980b2164fb44ea7faa90, priority revision6.
+The assigned item explicitly follows PR3960's cap30 caller handoff. The parent
+coordinator fetched canonical main and checked671 open PR bodies and rendered
+C5/start/handoff/active-board discussions before the split; no matching
+common30 item was found. This worker checked PR3960's live head and body,
+canonical retained caller sources, an open-PR lexical common30 query and the
+local overlap helper. That helper searched2,490 local records but had no usable
+remote snapshot because the gh executable was unavailable. Closed-work,
+arbitrary-diff, discussion-wide and private-work coverage remains partial;
+these checks are not a novelty certificate. Publication refresh is reported
+in the PR. The scoped package changes no selected record or frozen source.
+
+The root model and separate shell/Cramer reconstruction are explicitly adapted
+from this donor's PR3960, whose model is adapted from PR3951. Their code lineage
+is credited; "separate" does not mean newly independent of those predecessors.
+Nick Petalas supplies the global capacities and root/common-cut predecessors;
+DreamingOfClouds/PR3154 supplies TWOSIDE and C5; David Arias, joaqcoo and the
+retained E8/P112 lineage retain their attribution. Exact predecessor heads and
+roles are in [PREDECESSORS.json](PREDECESSORS.json). The new contribution is
+the complete common30 graph/span proof and this named literal exclusion.
+
+This is not a full cell reconciliation, full C5, decoder floor, supplier,
+multiplication theorem or new kappa. Literal caller survival is independently
+checked against the authenticated retained necessary filter; survival alone
+is never treated as an actual construction.
+
+## Open next questions
+
+Review the generic-normal rational-rank argument and finite graph coverage,
+then reconcile a different actual caller against current public contracts
+before expanding the search. Each structured question in [TASK.json](TASK.json)
+states relevance, first step and blocker. The current session stops at this
+one caller; no continuing reservation is made.
+
+Prepared by Chris R / Clear1nsight with substantial OpenAI Codex assistance,
+including parallel research agents. Apache-2.0.