Research: exclude five P112 beta shapes with a coordinate budget

research/p112-ten-piece-simplex/CHECKS.json

@@ -0,0 +1,70 @@
+{
+  "schema": "p112-ten-piece-simplex-checks/v1",
+  "checked_at_utc": "2026-10-17T14:10:01.656746+00:00",
+  "upstream_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a",
+  "priority_revision": 6,
+  "environments": {
+    "3.12": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]\nmacOS-27.0.1-arm64-arm-64bit",
+    "3.13": "3.13.16 (main, Oct 14 2026, 00:55:38) [Clang 23.1.3 ]\nmacOS-27.0.1-arm64-arm-64bit-Mach-O"
+  },
+  "checks": [
+    {
+      "command": "TMPDIR=SESSION uv run --python 3.12 --no-project python -W error -B scripts/research_package.py --package research/p112-ten-piece-simplex",
+      "result": "PASS_REGISTERED_RESEARCH_PACKAGE; full receipt equality; sixteen optimized behavioral groups"
+    },
+    {
+      "command": "TMPDIR=SESSION uv run --python 3.13 --no-project python -O -W error -B EXPORT/research/p112-ten-piece-simplex/verify.py",
+      "result": "PASS; identical receipt from read-only Git-free source export"
+    },
+    {
+      "command": "TMPDIR=SESSION uv run --python 3.13 --no-project python -O -W error -B EXPORT/research/p112-ten-piece-simplex/test_verify.py",
+      "result": "sixteen groups pass from read-only Git-free source export"
+    },
+    {
+      "command": "Run both exact pinned PR3154 TWOSIDE bk1b.py and bk2b.py sources",
+      "result": "both reproduce 38 survivors for (5,5); interpretation of their deficit columns differs, so no deficit statistic is used"
+    },
+    {
+      "command": "Compile all four package Python sources in memory with warnings as errors; inspect every function via ast",
+      "result": "syntax passes; all functions below 60 physical lines; Ruff/Mypy/Pyright unavailable"
+    },
+    {
+      "command": "Compare geometry.py bytes with pinned PR3164 Git blob",
+      "result": "identical"
+    },
+    {
+      "command": "Invoke verify.py --output on an in-checkout path and an existing external path",
+      "result": "both reject; no in-checkout file created; existing receipt is not overwritten"
+    },
+    {
+      "command": "Validate all historical source heads with the initial registered replay; retain their exact heads/blobs/hashes as historical citations, outside required replay pins",
+      "result": "historical source records verified locally; required replay provenance uses canonical main only and does not depend on unrelated PR commits or the contribution merge strategy"
+    }
+  ],
+  "coverage": {
+    "label_flat_kernels": 4097782,
+    "root_line_pairs": 7140,
+    "simple_reflections": 960,
+    "behavioral_groups": 16,
+    "all_endpoint_patterns": 117649,
+    "new_exclusion_margins": [
+      11,
+      11,
+      27,
+      27,
+      27
+    ]
+  },
+  "review": {
+    "mathematics": "Read-only internal review independently corroborated the endpoint inequality, quotient argument and five support budgets.",
+    "overlap": "Separate exhaustive enumeration corroborated all five prior-cover minima and the rank-four-anchor control.",
+    "limits": "Internal review is not independent human or proof-kernel review. Weyl-chamber theorem, full TWOSIDE reduction, all other decoder cases and supplier admission remain separate obligations."
+  },
+  "publication": "Run scripts/check_research_commit.py after committing and inspect GitHub head before final handoff.",
+  "not_run": [
+    "Lean/proof-assistant build",
+    "full supplier cold replay",
+    "historical long predecessor suites",
+    "hosted CI"
+  ]
+}

research/p112-ten-piece-simplex/DECISIONS.tsv

@@ -0,0 +1,4 @@
+timestamp	attempt	hypothesis	change	before	after	correctness_check	verdict	note
+2026-10-17T14:08:22.379991+00:00	1	four small pieces preserve the six-vertex simplex	ten-piece quotient in dimension five	0 new exclusions	2 new exclusions	full geometry and prior-cover checks	keep	original count margins one and one
+2026-10-17T14:08:22.379991+00:00	2	3^3,4,6^6 is another new application	alternative quotient basis audit	claimed new candidate	covered by PR3167	all quotient bases and independent covers	reject novelty	retained as an overlap control
+2026-10-17T14:08:22.379991+00:00	3	finite coordinate count strengthens the endpoint charge	unequal pairs at most 4k+1	2 new exclusions	5 new exclusions	complete endpoint patterns; full geometry; internal proof review	keep	exact margins 11,11,27,27,27; no runtime metric

research/p112-ten-piece-simplex/ENGINEERING.md

@@ -0,0 +1,62 @@
+# Verification bounds and decisions
+
+Build the Lever changed the work from a larger deletion census to a reusable
+checker for one counting lemma and its actual weight applications. Prove It
+Works required complete receipt equality, losing controls, a separately coded
+cover oracle and publication-byte checks. Power of Ten kept loops finite,
+checks active under optimization, and generated output outside the checkout.
+
+The code is isolated in this package. `geometry.py` is byte-identical to the
+pinned PR3164 source. `beta.py` contains the new inequality, application and
+overlap logic. `verify.py` reconstructs data and compares the receipt.
+`test_verify.py` tests mathematical inequalities and failure conditions.
+No selected result, shared verifier or frozen predecessor changes.
+
+All control flow is structured and nonrecursive. Flat enumeration has exactly
+3,309,747 and 788,035 kernels. There are 7,140 root pairs and 120 third-root
+candidates per pair; 960 reflection checks; eight-dimensional elimination;
+and weight multisets of lengths five through ten over six possible weights.
+Quotient covers have at most C(10,5)=252 index choices and 3^5=243 bin
+assignments. The independent cover oracle uses at most 2^5 * 2^5 pairs of
+subsets. The endpoint-pattern control uses 7^6=117,649 patterns. Registered
+commands run sequentially with 120-second bounds. There is no recursive
+search, retry loop or background process.
+
+Rule 3 deviation, managed-runtime allocation. Python creates integers, tuples
+and Fraction objects during these bounded computations. Avoiding allocation
+would require replacing the standard-library implementation. Live geometry is
+bounded by 120 eight-dimensional roots, a 120-by-120 Gram table, 512 masks of
+112 bits, at most four collections of at most 64 row masks, and 113 histogram
+counters. Kernels are processed and discarded. The input has a 2 MB size cap;
+the pinned input is 971,985 bytes. New live application data are at most 38
+weight tuples of length ten, five result rows and 252 quotient-index choices
+streamed from an iterator. Tests use scoped temporary directories. Full replay
+and mutation tests exercise the bounds and cleanup. Reconsider a fixed-memory
+native implementation only if the fixed problem dimensions grow.
+
+Functions stay below 60 physical lines. Meaningful guards check dimensions,
+source bytes, rank inventories, kernel counts, quotient and root thresholds,
+original survivors and prior coverage. They use `require` rather than Python
+assertions, so optimization does not disable them. Test assertions use unittest.
+State is local except read-only module lookup tables. No dynamic evaluation or runtime
+code generation is used. Every subprocess used for development is checked;
+the retained verifier launches none. Output creation uses exclusive mode.
+
+Rule 9 runtime limitation. Python exposes no C pointer-dereference discipline.
+The nearest inspected mechanisms are bounded tuple/list access and direct
+function calls; there is no application callback chain or dynamic dispatch.
+The unittest framework has a fixed set of sixteen local test methods.
+
+Rule 10 diagnostics limitation. Mathematical and behavioral commands run with
+`-W error`; optimization controls retain their guards. Bytecode compilation
+checks syntax without writing into the checkout. The registered manifest makes
+the real replay recurring. No Ruff, Mypy or Pyright executable is installed;
+adding a repository-wide lint policy would exceed this isolated research task.
+The follow-up is to include these files in such a policy when adopted.
+CHECKS.json records the exact supported diagnostics and environments.
+
+The metric is the number of additional pinned beta shapes excluded, rather
+than runtime. All acceptance values are exact integers. DECISIONS.tsv records
+the rejected overlap and the original-count versus coordinate-budget attempts.
+No noisy timing result or benchmark speedup is claimed. The best remaining
+question requires a different quotient-independence argument for `4,5^9`.

research/p112-ten-piece-simplex/PROOF.md

@@ -0,0 +1,203 @@
+# A coordinate budget strengthens the P112 root-simplex obstruction
+
+## Statement
+
+Let K be a characteristic-zero field. Use the 112 live E8 root lines and
+their binary labels ell(t) from the pinned P112 input. Put
+
+```
+C = {c_h : c_h(t) = <r_t,h>, h in K^8},
+w(q) = rank_F2 {ell(t) : q(t) != 0}.
+```
+
+The root representatives r_t in the replay are doubled roots. Scaling the
+representatives does not change supports. Ten linearly independent pieces
+spanning T with dim(T intersect C) >= 5 cannot have weights bounded by any
+of these five multisets:
+
+```
+2,2,4,5,6,6,6,6,6,6
+2,2,5,5,5,6,6,6,6,6
+2,3,4,4,6,6,6,6,6,6
+2,3,4,5,5,6,6,6,6,6
+2,4,4,4,5,6,6,6,6,6.
+```
+
+All five are actual survivors of the pinned TWOSIDE `(b,t)=(5,5)` BK/BK7
+weight filters. This is a theorem about these explicit piece hypotheses.
+Its application to the decoder reduction inherits that reduction's other
+conditions. It does not settle C5, the decoder floor or a supplier.
+
+## Geometry and finite dependencies
+
+We use the following P112 facts, replayed rather than assumed from a receipt:
+
+1. Supports of weight d=2,3,4,5,6 have cardinality at most 2,4,8,12,20.
+2. Every nonzero element of C has support at least 53.
+3. A nonzero element of C with support below 70 is a root direction.
+4. The evaluation map h -> c_h is injective.
+
+The first three dimensions follow from the labels' leading-one coordinate:
+a binary d-flat meets that affine hyperplane in at most 2^(d-1) points.
+For dimensions five and six, `geometry.py` enumerates every annihilator in
+unique reverse row-echelon form: 3,309,747 and 788,035 subspaces. Their
+kernel intersections with the 112 distinct labels have maxima 12 and 20.
+A support of smaller rank extends to a flat of the stated dimension.
+
+For facts 2 and 3, use the standard Weyl-chamber theorem for the real E8
+root system. A real direction with support below 70 is perpendicular to at
+least 43 live root lines. In a closed chamber the perpendicular root system
+is generated by the simple roots that vanish on the direction. The replay
+checks that all six-node parabolics have at most 36 root lines. The eight
+seven-node parabolics have counts `42,28,22,14,16,23,37,63`; only the last
+can contain 43 perpendicular lines, and its normal is a root direction.
+Root directions have live supports 53 or 56, so the same argument also
+rules out support below 53. The replay checks all 960 simple reflections,
+simple-system positivity, parabolic counts and root supports. The chamber
+theorem itself is a mathematical dependency, not a program-proved result.
+
+These facts extend to K. Rational roots perpendicular to a nonzero
+K-valued direction span a rational subspace of dimension at most seven.
+If this dimension were at most six, choose a generic real normal to that
+span. Its perpendicular roots are exactly the roots in that span; the
+six-node parabolic bound allows at most 36 lines, contradicting 43.
+Consequently, at support below 70 the perpendicular span has dimension
+seven. Its rational kernel is one-dimensional, and the K-valued direction
+is proportional to its rational generator. Apply the real argument to
+that generator. Finally, the live-root Gram sum is 112 times the identity
+in doubled coordinates, proving injectivity over K.
+
+The geometry code is unchanged from Nick Petalas's PR3164. Its exact
+source pin and the preceding E8/P112 lineage are in SOURCES.json.
+
+## Four small pieces leave a root A5 simplex
+
+Choose the four smallest pieces s_1,...,s_4. Write S for the union of their
+supports and s=|S|. The remaining pieces are q_0,...,q_5; put
+U=sum_i |supp(q_i)|. For every proposed shape, the support-cap sum for S
+plus any one q_i is at most 48, strictly below 53.
+
+Let D=T intersect C and lambda:T -> T/D. Since dim T=10 and dim D>=5,
+the quotient has dimension at most five. The four small images together
+with each q_i image are independent. A dependence would give a nonzero
+codeword supported on fewer than 53 coordinates, contrary to fact 2.
+Thus dim(T/D)=5, dim D=5, and the four small images are independent.
+
+Modulo their span, the six q_i images are nonzero in one dimension.
+Rescale each q_i to give it the same image there. The supports do not change.
+For i=1,...,5 there is a unique small-piece combination a_i with
+
+```
+c_i = q_i - q_0 - a_i in D.
+```
+
+Set c_0=a_0=0. The five c_i are independent, since their coefficients on
+q_1,...,q_5 in the original piece basis are distinct unit vectors. Every
+edge c_i-c_j is nonzero and supported on S union supp(q_i) union supp(q_j).
+The largest edge-support cap in the five applications is 68, below 70.
+By facts 3 and 4, c_i=c_{h_i} for five independent directions, and every
+difference among 0,h_1,...,h_5 is a scalar root direction.
+
+Here is the root-simplex argument from PR3164 with its hypotheses retained.
+Normalize roots to norm squared two. In the plane of two independent
+rational E8 roots, a third root line exists only in an A2 subsystem, with
+coefficient ratio +1 or -1. The replay verifies this for all 7,140 root-line
+pairs and all 120 possible third roots. The same statement holds over K:
+a rational vector in the K-span of two rational independent vectors is
+already in their rational span, by an invertible rational coordinate minor.
+
+Write h_i=b_i alpha_i for roots alpha_i. Every h_i-h_j is a third root line,
+so b_i/b_j is +1 or -1. Absorb these signs to write h_i=b alpha_i with one
+common b!=0. Then <alpha_i,alpha_j>=1 and alpha_i-alpha_j is a root. Thus
+0,alpha_1,...,alpha_5 form a root A5 simplex.
+
+Each live coordinate r evaluates on its vertices in six integer levels,
+all pairwise differences in {-2,-1,0,1,2}. If a difference has absolute
+value two, equality in Cauchy-Schwarz makes r the corresponding edge root.
+The value multiplicities are 1,1,4, with nine unequal pairs. Otherwise the
+levels occupy at most two consecutive integers, with at most 3*3=9 unequal
+pairs. Therefore each coordinate lies in at most nine of the fifteen edge
+supports. The common nonzero field scalar changes no zeros. This is a
+universal proof; the replay's sharp A5 fixture is a calibration only.
+
+## The new coordinate-budget inequality
+
+At a coordinate outside S, the edge values are exactly q_i(t)-q_j(t).
+Suppose k of the six endpoint values are nonzero. There are at most
+
+```
+k(6-k) + k(k-1)/2 = k(11-k)/2
+```
+
+unequal pairs. For every integer k=0,...,6, this is at most 4k+1, since
+(k-1)(k-2)>=0. It is also at most 5k. This statement works for arbitrary
+field-valued endpoints and needs no root-system assumption.
+
+There are exactly 112-s coordinates outside S. Summing the new bound gives
+
+```
+outside edge incidences <= 4 U_outside + 112-s <= 4U + 112-s.
+```
+
+Using the nine-incidence bound inside S, and the distance 53 on all fifteen
+edges, yields
+
+```
+795 = 15*53 <= 9s + 4U + 112-s = 112 + 8s + 4U.       (*)
+```
+
+The original endpoint count gives the additional bound `795 <= 9s+5U`.
+Both right sides increase with s and U, so replacing them with their
+support-cap sums is valid even when small supports overlap, when some
+q_i support lies in S, or when the actual supports are smaller.
+
+| Ten-piece weights | Four small weights | s cap | U cap | New upper | Margin | Old margin |
+|---|---|---:|---:|---:|---:|---:|
+| `2,2,4,5,6^6` | `2,2,4,5` | 24 | 120 | 784 | 11 | -21 |
+| `2,2,5^3,6^5` | `2,2,5,5` | 28 | 112 | 784 | 11 | -17 |
+| `2,3,4^2,6^6` | `2,3,4,4` | 22 | 120 | 768 | 27 | -3 |
+| `2,3,4,5^2,6^5` | `2,3,4,5` | 26 | 112 | 768 | 27 | 1 |
+| `2,4^3,5,6^5` | `2,4,4,4` | 26 | 112 | 768 | 27 | 1 |
+
+Each row contradicts (*). The first three exclusions specifically require
+the stronger coordinate budget; the original count cannot establish them.
+
+## Bind the applications and distinguish earlier coverage
+
+`beta.py` reproduces all 38 original `(5,5)` BK/BK7 survivors over all
+weight multisets of lengths five through ten with weights two through seven.
+The filters follow the two pinned TWOSIDE implementations. Their full
+decoder-level derivation and generalized distances are inherited; the five
+new exclusions themselves only need the explicit hypotheses stated above.
+Replacing weights zero or one by two is conservative for support bounds.
+
+For every proposed shape, the replay examines every support-certified
+five-piece quotient basis and every weight-certified cover by two six-flats
+plus individual deleted supports. It checks the earlier eight-cut span-three,
+ten-cut span-four and twelve-cut rank-four-anchor theorems. A nonbasis
+weight-seven piece is conservatively charged one extra independent direction.
+Minimum cut allowances in the five rows are `12,16,12,14,16`, all above ten.
+The first three rows admit no weight-four anchor in a support-certified
+quotient cover. The last two need at least eighteen cuts with such an anchor.
+
+This is an audit of those weight-certified rules. It does not exclude better
+covers exploiting overlaps in actual supports, or prove that every other
+research route was tried. A separate subset-cover oracle corroborates the
+enumeration without its ternary-assignment implementation.
+
+The superficially similar shape `3,3,3,4,6^6` is deliberately excluded from
+the new-result count. PR3167 already excludes it: use quotient basis
+`3,3,3,6,6`, support cap 52, and twelve common extra lines. The nonbasis
+weight-four piece supplies the rank-four anchor. This overlap control is
+checked on every replay. A nine-piece PR3164 exclusion does not directly
+cover a ten-piece configuration: deleting one piece only guarantees an
+intersection of dimension four, rather than the required five.
+
+## Verification limits
+
+The proof uses the standard Weyl-chamber theorem and exact finite label/root
+facts. It is not proof-kernel verified. Internal mathematical review and
+separate enumeration methods are not independent human review. Other beta
+shapes, full C5, the C1-C7 reduction and supplier admission remain separate
+obligations. The selected exponent is unchanged. No full supplier replay,
+Lean build or historical long suite is required or claimed for this result.