Research: exclude three larger-simplex P112 beta shapes

research/p112-larger-root-simplices/CHECKS.json

@@ -0,0 +1,67 @@
+{
+  "status": "local checks passed",
+  "baseline_main": "997e6a9ca7b4f95d50e366f61412fd640d72a88a",
+  "priority_revision": 6,
+  "environment": {
+    "python": "3.12.15",
+    "second_python": "3.13.5",
+    "platform": "Linux 6.6.87.2, WSL2, x86_64, glibc 2.41",
+    "dependencies": "Python standard library only"
+  },
+  "executed": [
+    {"command": "python3 -B scripts/research_baseline.py", "result": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY; not a selected cold replay"},
+    {"command": "python3.12 -W error -B research/p112-larger-root-simplices/verify.py --output SESSION/RESULT.json", "result": "PASS_LARGER_ROOT_SIMPLICES; exact margins 9,4,12; all 4,097,782 flat kernels, 7,140 root planes, 960 reflections and original 24-cell table recomputed"},
+    {"command": "python3.13 -O -W error -B research/p112-larger-root-simplices/verify.py", "result": "PASS; exact committed-receipt equality on a second interpreter"},
+    {"command": "python3.12 -O -W error -B research/p112-larger-root-simplices/test_verify.py", "result": "PASS; 15 behavioral groups, including losing support budgets, strict geometric cutoffs, source/input/receipt mutants and rational fixture ranks"},
+    {"command": "python3.12 -B scripts/research_package.py --package research/p112-larger-root-simplices --check-only", "result": "PASS_PACKAGE_METADATA_AND_PINS"},
+    {"command": "TMPDIR=SESSION python3.12 -B scripts/research_package.py --package research/p112-larger-root-simplices", "result": "PASS_REGISTERED_RESEARCH_PACKAGE outcome=completed; both commands run sequentially"},
+    {"command": "TMPDIR=SESSION python3.13 -O -W error -B SESSION/source-export/research/p112-larger-root-simplices/verify.py", "result": "PASS; read-only Git-free source export with only this package and its declared data input"},
+    {"command": "ruff check --no-cache research/p112-larger-root-simplices/{simplex,verify,test_verify}.py research/p112-larger-root-simplices/vendor/__init__.py", "result": "All checks passed; immutable predecessor sources are not reformatted"},
+    {"command": "PYTHONPYCACHEPREFIX=SESSION/bytecode python3.12 -W error -m compileall -q research/p112-larger-root-simplices", "result": "PASS; compiled output kept outside the checkout"},
+    {"command": "Compare retained source bytes with git show SOURCE_HEAD:SOURCE_PATH", "result": "All six retained original files match their stated Git objects exactly"}
+  ],
+  "mathematical_review": {
+    "method": "Local proof review separate from executable inspection; no independent reviewer is claimed",
+    "checked": ["quotient dimension and nonzero normalization", "characteristic-zero rational-kernel argument", "A2 coefficient signs and common root scale", "both incidence cases for seven through nine vertices", "outside endpoint charging", "actual original weight-filter membership", "four-piece cover and rank-four-anchor overlap limits"],
+    "result": "No unresolved local objection; all exact controls pass"
+  },
+  "engineering": {
+    "principles": {
+      "Build the lever": "The retained deterministic checker reconstructs geometric quantities and the three named applications.",
+      "Prove it works": "Full mathematical replay, negative controls, a second interpreter and a read-only Git-free export check the actual package.",
+      "Power of Ten": "New code has no recursion, bounded domains, narrow state, checked source and subprocess boundaries, explicit exceptions and warning-clean validation."
+    },
+    "bounds": [
+      "New incidence/fixture loops have at most nine vertices, 36 edges and 120 root lines; exact fixture elimination uses eight columns.",
+      "The three production survivor cells enumerate at most 5*C(17,5)=30,940 raw rows per cell; the public helper's larger supported t<=6 domain is bounded by 7*C(19,5)=81,396 raw rows.",
+      "Basis packing has at most 2^6 assignments. The cover audit has at most C(12,4)=495 indexed bases and 3^4=81 assignments per distinct weight multiset.",
+      "The original source program has fixed b=5..8, t=1..6 and a 120-second subprocess timeout; output is exactly 24 short integer rows.",
+      "Input files are capped at 2,000,000 bytes. Source inventory has at most ten entries. All new functions are below 60 physical lines."
+    ],
+    "deviations": [
+      {"rule": "3: fixed memory allocation", "location": "new Python checker and immutable geometry module", "reason": "Managed Python arithmetic and iteration allocate at runtime.", "scope": "Finite proof replay only", "compensating_control": "Fixed 112-label/120-root domains; flat census streams one kernel at a time; supported weight bounds and file-size limits bound live state.", "verification": "Complete normal/optimized replays, fixture and invalid-input tests pass.", "follow_up": "Use fixed arrays only if this proof replay is moved to a constrained runtime."},
+      {"rule": "9: indirect calls", "location": "test_verify.py unittest discovery", "reason": "The standard unittest framework dispatches named tests.", "scope": "Fifteen local behavioral tests only", "compensating_control": "One fixed Controls class and explicit unittest.main entry point.", "verification": "The optimized test run reports all fifteen tests.", "follow_up": "Retain framework dispatch unless the test framework changes."},
+      {"rule": "10: immutable-source diagnostics", "location": "vendor/bk2b.py and vendor/geometry.py", "reason": "These are authenticated frozen scientific source bytes; restyling them would break provenance.", "scope": "Unchanged retained originals only", "compensating_control": "SHA256/Git-blob equality, warnings-as-errors compilation and complete source-bound execution; new code passes Ruff.", "verification": "Full replay and origin-byte comparison pass.", "follow_up": "Any source cleanup belongs in a separately pinned successor, never this frozen copy."}
+    ]
+  },
+  "upstream_checkpoint": {
+    "checked_at": "2026-10-17T14:12:25Z",
+    "main": "997e6a9ca7b4f95d50e366f61412fd640d72a88a",
+    "priority_revision": 6,
+    "guidance_changed": false,
+    "open_pr_snapshot": "2026-10-17T14:11:57.624241+00:00",
+    "discussion_snapshot": "2026-10-17T14:12:25.361600+00:00",
+    "complete_pagination": true,
+    "warnings": [],
+    "subsequent_live_check": "PR3169 at b859f7791a6d2dad68652d5a54e266cb020a1302 has distinct (5,5) scope; body read, not cold-replayed."
+  },
+  "limits": [
+    "The standard Weyl-chamber theorem is used, not formally proved.",
+    "One literal simplex per size does not prove the universal incidence bound; the written argument does.",
+    "No independent human/proof-kernel review or hosted CI result is claimed.",
+    "No complete C5 cell, C(P112)>=64, native/outer replay, supplier admission or new kappa is claimed.",
+    "The generic selected-frontier cold replay was not run because no selected construction or input was changed.",
+    "The cover audit excludes only weight-certified predecessor applications, not all possible geometric covers.",
+    "Generic Git provenance pins resolve only at main. Pending source heads are authenticated through the retained-file byte inventory and the separately executed origin comparison, avoiding dependence on unmerged Git objects in hosted CI."
+  ]
+}

research/p112-larger-root-simplices/PROOF.md

@@ -0,0 +1,168 @@
+# Three larger-simplex exclusions
+
+## Proposition
+
+Let `K` be a characteristic-zero field. Let `r_t` and `ell(t)` be the pinned
+P112 root representatives and binary labels. On its 112 coordinates put
+
+```
+C = {c_h : c_h(t) = <r_t,h>, h in K^8},
+w(q) = rank_F2 {ell(t) : q(t) != 0}.
+```
+
+For each `b in {6,7,8}`, there do not exist `b+4` independent pieces spanning
+`T` such that `dim(T intersect C) >= b` and their weights are bounded by
+
+```
+2,5,5,5, followed by b copies of 6.
+```
+
+Thus the proposition excludes the named `2,5^3,6^b` weight shape in each
+pinned TWOSIDE cell `(b,t)=(6,4),(7,4),(8,4)`. It is a theorem about these
+piece configurations, not the whole C5 conjecture or a decoder lower bound.
+
+## Replayed geometric premises
+
+The unchanged geometry implementation from PR3164 reconstructs the 120 E8
+root lines, removes the eight frame lines and reconstructs all 112 labels.
+The data match the exact main-branch input. The labels have a leading one,
+so `g(2)<=2`, where `g(d)` is the maximum number of live labels in a
+`d`-dimensional binary linear space. Complete unique reverse-echelon
+annihilator enumeration gives `g(5)=12` and `g(6)=20`. It covers 3,309,747
+five-flats and 788,035 six-flats. Every lower-dimensional support can be
+extended to a flat of the stated dimension.
+
+Every nonzero codeword in `C` has support at least 53. Every codeword with
+support below 70 is proportional to a root codeword. For completeness, the
+argument behind the retained finite quantities is as follows. Below 70
+means at least 43 perpendicular live root lines. Move a real direction into
+a closed Weyl chamber. The perpendicular roots are generated by vanishing
+simple nodes. Every six-node subsystem has at most 36 root lines. The eight
+seven-node subsystems have `42,28,22,14,16,23,37,63` root lines. Only the last
+can contain 43; its normal is a root direction. Root directions have live
+supports 53 or 56, which also proves the distance 53. The replay checks all
+960 simple reflections, simple-system positivity and these subsystem counts.
+The standard finite-root-system Weyl-chamber theorem is used, not proved by
+the executable.
+
+The statement extends to `K`. The rational roots perpendicular to a nonzero
+field-valued direction have rational rank at most seven. If the rank were
+at most six, a generic real normal to their span would contradict the
+36-line bound. Hence a direction with at least 43 perpendicular roots is in
+a one-dimensional rational kernel, and is proportional over `K` to a real
+rational direction. Apply the real argument. The replay also checks that
+the P112 root matrix has full rank eight, making `h -> c_h` injective.
+
+## A quotient with seven through nine vertices
+
+Choose three small pieces of weights `2,5,5`, and let `S` be the union of
+their supports. Write the other pieces as `q_0,...,q_b`, with weights
+`5,6,...,6`. Let `D=T intersect C` and `lambda:T -> T/D`. Then
+
+```
+|S| <= 2+12+12 = 26,
+dim(T/D) <= (b+4)-b = 4.
+```
+
+The small pieces together with any one `q_i` have support at most
+`26+20=46<53`. Their quotient images must be independent. Otherwise a
+nonzero combination of four independent pieces would be a nonzero
+codeword supported on fewer than 53 coordinates. Consequently the quotient
+has dimension exactly four, the three small images are independent and
+every `q_i` has nonzero image after quotienting by their span.
+
+This last quotient is one-dimensional. Rescale the `q_i` so that they have
+the same nonzero image. Supports and piece independence are unchanged.
+There are unique small-piece combinations `a_i` for which
+
+```
+c_0=0,
+c_i=q_i-q_0-a_i belongs to D,  i=1,...,b.
+```
+
+The `b` codewords `c_i` are independent, since their coefficients on the
+independent pieces `q_1,...,q_b` are distinct unit vectors. Each nonzero edge
+`c_i-c_j` is supported on `S union supp(q_i) union supp(q_j)`, hence has
+support at most `26+20+20=66<70`. All edges are root directions.
+Injectivity supplies `b` independent directions `h_i` with `c_i=c_{h_i}`.
+
+## The larger root-simplex incidence lemma
+
+Normalize roots to squared norm two. In the plane of two independent E8
+roots, any third root line is an A2 sum or difference, with coefficients of
+absolute value one. All 7,140 root-plane checks are replayed exactly. This
+fact holds over `K` too: a rational root in the `K`-span of two rational
+roots is already in their rational span, by solving a nonsingular rational
+coordinate minor.
+
+Write `h_i=z_i alpha_i` for roots `alpha_i`. Every `h_i-h_j` is a third
+root line, so `z_i/z_j` is `+1` or `-1`. Absorb signs into the roots. There
+is a common nonzero `z` such that `h_i=z alpha_i`; moreover
+`<alpha_i,alpha_j>=1` for distinct indices. Thus
+`0,alpha_1,...,alpha_b` is a root A_b simplex with `n=b+1` vertices.
+
+For any E8 root `r`, its evaluations on these vertices are integers and all
+pair differences lie in `{-2,-1,0,1,2}`. If a difference has absolute value
+two, equality in Cauchy-Schwarz makes `r` that edge root. The evaluation
+multiplicities are then `1,1,n-2`, so there are `2n-3` unequal pairs. If no
+difference has absolute value two, there are at most two consecutive integer
+levels, giving at most `floor(n^2/4)` unequal pairs. Therefore each live
+coordinate occurs in at most
+
+```
+M_n = max(2n-3, floor(n^2/4))
+```
+
+edge supports. For `n=7,8,9`, these bounds are `12,16,20`. They are universal
+upper bounds; sharpness in E8 is not asserted for every size. In particular,
+the literal nine-vertex fixture has maximum 18, not 20. Multiplication by
+the common field scalar `z` does not change which evaluations vanish.
+
+## Incidence contradiction
+
+There are `E=n(n-1)/2` edges, each with at least 53 support coordinates.
+At most `M_n |S|` edge incidences occur in `S`. Outside `S` each edge is
+exactly `q_i(t)-q_j(t)`. Every unequal pair has a nonzero endpoint, and one
+nonzero endpoint can meet only `n-1=b` pairs. Set
+`U=sum_i |supp(q_i)| <= 12+20b`. It follows that
+
+```
+E*53 - M_n*|S| <= outside edge incidences <= b*U.
+```
+
+Substituting upper bounds only weakens the contradiction:
+
+| b | n | E | M_n | S cap | U cap | Required inequality | Margin |
+|---|---|---|---|---|---|---|---|
+| 6 | 7 | 21 | 12 | 26 | 132 | 801 <= 792 | 9 |
+| 7 | 8 | 28 | 16 | 26 | 152 | 1068 <= 1064 | 4 |
+| 8 | 9 | 36 | 20 | 26 | 172 | 1388 <= 1376 | 12 |
+
+All three are impossible. Smaller supports or overlaps strengthen the bound.
+Increasing the allowed small-support union by just one removes each of these
+contradictions; the checker retains this failure control.
+
+## Actual residue and overlap boundary
+
+The unchanged original `bk2b.py` reproduces all 24 pinned survivor counts.
+A separate implementation reproduces the three relevant counts
+`69,154,251`, and retains each target shape. The original filters are source
+context, not new universal proof obligations established by this computation.
+
+There are exactly two four-piece weight multisets whose support capacities
+are below 53 in each target: `(2,5,5,5)` and `(2,5,5,6)`. Exhaustively assigning
+each to two groups of total weight at most six, with the rest paid as line
+deletions, gives minimum deletion budget fourteen. The nonbasis pieces have
+weight at least five, so this weight-certified calculation cannot invoke
+PR3167's rank-four anchor. Consequently the earlier eight-/ten-deletion and
+twelve-deletion/rank-four-anchor theorems do not themselves certify these
+shapes by this weight-only cover route. This is not a claim that all other
+possible proofs or geometric covers were excluded.
+
+Concurrent PR3169's five `(5,5)` exclusions and stronger six-vertex
+coordinate budget are outside this scope; its proof was not cold-replayed
+here. The six-vertex
+PR3164 inequality is a positive control, not another new result. No complete
+C5, `C(P112)>=64`, supplier, native/outer implementation or kappa improvement
+follows from these three exclusions. Independent human and proof-kernel
+review remain separate from this author-checked proof and exact replay.

research/p112-larger-root-simplices/README.md

@@ -0,0 +1,87 @@
+# Larger root simplices exclude three P112 weight shapes
+
+For `b=6,7,8`, independent P112 pieces of weights bounded by `2,5^3,6^b`
+cannot have code-intersection dimension at least `b`. This excludes one
+named shape in each pinned TWOSIDE cell `(6,4),(7,4),(8,4)`.
+
+The proof extends PR3164's six-vertex root-simplex argument to seven, eight
+and nine vertices. Each coordinate meets at most `12,16,20` edge supports.
+The three incidence contradictions have exact margins **9, 4 and 12**.
+The original source's relevant survivor counts are `69,154,251`; this package
+does not claim to close those entire cells.
+
+[PROOF.md](PROOF.md) gives the characteristic-zero argument and its exact
+hypotheses. [RESULT.json](RESULT.json) contains the replayed geometric
+quantities, three literal simplex controls, original 24-cell survivor table,
+three exclusion receipts and overlap audit. This is author-checked evidence,
+not independent human or proof-kernel review. No full C5, `C(P112)>=64`,
+decoder, supplier admission or new kappa is established. Selected frontier
+files are unchanged.
+
+## Reproduce
+
+From the repository root, with Python 3.12+ and no third-party dependencies:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/p112-larger-root-simplices --check-only
+python3.12 -B scripts/research_package.py --package research/p112-larger-root-simplices
+```
+
+The registered replay enumerates all 4,097,782 five-/six-flat kernels, checks
+7,140 root planes and 960 simple reflections, reruns the original survivor
+program and runs fifteen behavioral groups. It compares exact proof-relevant
+JSON fields rather than timing or compressed-container bytes. Set `TMPDIR`
+to an external session directory if your workspace policy requires it.
+A direct replay writes nothing in the checkout:
+
+```sh
+python3.12 -W error -B research/p112-larger-root-simplices/verify.py
+python3.12 -O -W error -B research/p112-larger-root-simplices/test_verify.py
+```
+
+`verify.py --output /NEW/EXTERNAL/RESULT.json` creates a fresh receipt and
+refuses an existing path or an output inside the checkout. A Git-free export
+needs only this package and its one declared data input. [CHECKS.json](CHECKS.json)
+records the environment, checks and verification limits.
+
+## Scope and source credit
+
+Nick Petalas. Apache-2.0. The original reduction, TWOSIDE piece hypotheses,
+weight filters and survivor program are DreamingOfClouds's PR3154 at
+`708f0ad8928c383de8294aea3c126e9461d2066d`, with the retained E8/P112 decoder
+lineage. The root-simplex predecessor is Nick Petalas's PR3164 at
+`857384079ab640a949fb7618b7909664d3e737e5`. Its geometry implementation and
+proof are copied unchanged into `vendor/`; the new work is the larger-simplex
+lemma, these three applications and their checks. The original notice and
+license are retained. [SOURCES.json](SOURCES.json) pins every retained file by
+source commit, Git blob and SHA256. Source equality is checked at replay;
+origin-byte equality was separately checked against those Git objects.
+Pending-PR Git history is not required for replay. The generic metadata pins
+resolve only at main; the vendored originals have their own explicit byte
+inventory, checked by `verify.py`.
+
+PR3167 at `c2c7508f2d731feea550f1628601aebd35c6e147` is an overlap control,
+not a new dependency of the theorem. Every weight-certified four-piece
+quotient cover here needs at least fourteen separate deletions, with no
+nonbasis rank-four anchor. Thus the earlier eight-/ten-deletion and
+rank-four/twelve-deletion bounds do not supply these exclusions by that
+weight-only route. Other geometric covers or proofs are not ruled out.
+Concurrent [PR3169](https://github.com/CrocSwap/integer-mult-bounds/pull/3169)
+at `b859f7791a6d2dad68652d5a54e266cb020a1302` reports five ten-piece
+`(5,5)` exclusions using a stronger six-vertex coordinate budget. Its PR
+was read at submission, not cold-replayed. Its scope is distinct from these
+seven-/eight-/nine-vertex results.
+
+The canonical investigation is [Discussion3156](https://github.com/CrocSwap/integer-mult-bounds/discussions/3156#discussioncomment-18999460).
+[Task, handoff choice and expansion decision](TASK.json). Development and local
+checking used substantial automated assistance.
+
+## Open next questions
+
+Pin one actual remaining TWOSIDE shape and check whether its small pieces
+again leave a one-dimensional quotient with all edge supports below 70.
+A positive complete incidence margin could justify another exclusion;
+a nonpositive margin is a stop test, not a construction. Refresh the live
+ledger first. The present package does not establish a complete remaining
+cell or authorize further supplier construction. Structured next steps and
+blockers are in [TASK.json](TASK.json).