research: exclude two P112 profiles with unequal endpoints

research/p112-unequal-endpoint-deletion/CHECKS.json

@@ -0,0 +1,101 @@
+{
+  "schema": "p112-unequal-endpoint-checks/v1",
+  "environment": {
+    "os": "Linux-6.6.87.2-microsoft-standard-WSL2-x86_64-with-glibc2.41",
+    "python": [
+      "3.12.15",
+      "3.13.5"
+    ],
+    "dependencies": "standard library only",
+    "ruff": "0.17.1"
+  },
+  "checks": [
+    {
+      "command": "python3.12 -B scripts/research_package.py --package research/p112-unequal-endpoint-deletion",
+      "result": "PASS_REGISTERED_RESEARCH_PACKAGE outcome=partial; exact replay and 12 optimized behavioral groups pass"
+    },
+    {
+      "command": "python3.13 -W error -OO -B research/p112-unequal-endpoint-deletion/verify.py",
+      "result": "PASS_P112_UNEQUAL_ENDPOINT_DELETION profiles=2 margin=11 errors=0"
+    },
+    {
+      "command": "python3.13 -W error -OO -B research/p112-unequal-endpoint-deletion/test_verify.py",
+      "result": "12 tests pass"
+    },
+    {
+      "command": "same Python 3.13 commands from a read-only source-only export with exactly the four declared inputs",
+      "result": "both pass; no Git metadata or extra predecessor imports"
+    },
+    {
+      "command": "ruff check --no-cache --select E4,E7,E9,F,B,C4,ICN,PIE,PGH,RUF,UP,SIM,I research/p112-unequal-endpoint-deletion/*.py",
+      "result": "all checks pass"
+    },
+    {
+      "command": "in-memory compile plus AST inspection of all three new Python files",
+      "result": "26 functions; longest 24 physical lines; no bytecode emitted"
+    }
+  ],
+  "semantic_mutants": [
+    {
+      "mutant": "dimension-loss",
+      "result": "rejected",
+      "observed_test": "test_sharp_dimension_loss"
+    },
+    {
+      "mutant": "small-support-charge",
+      "result": "rejected",
+      "observed_test": "test_both_actual_profiles"
+    },
+    {
+      "mutant": "strict-root-boundary",
+      "result": "rejected",
+      "observed_test": "test_strict_support_cutoffs"
+    },
+    {
+      "mutant": "rank-five-capacity",
+      "result": "rejected",
+      "observed_test": "test_both_actual_profiles"
+    }
+  ],
+  "failure_controls": [
+    "uniform endpoint charge does not exclude",
+    "old incidence upper bound does not exclude",
+    "strict 53/70 cutoffs",
+    "dimension deletion is not free",
+    "invalid support/weight/dimension inputs",
+    "each of four changed input files is rejected",
+    "wrong expected receipt is rejected",
+    "relative/in-checkout/overwrite output is rejected"
+  ],
+  "scope": {
+    "geometric_premises": "re-executed retained engine, not independent reimplementation",
+    "independent_components": "subset-cover oracle, sharp coordinate-subspace dimension examples, rational quotient fixture and elementary endpoint count",
+    "unrun": [
+      "proof-kernel formalization",
+      "independent human review",
+      "hosted CI",
+      "native or complete supplier replay"
+    ]
+  },
+  "upstream_checkpoint": {
+    "commit": "463113d675af7410ac91d53a4fed51ec6494eb9a",
+    "priority_revision": 6,
+    "relevant_guidance_changed": false,
+    "overlap_checked_at": "2026-10-17T17:10:54.688803+00:00",
+    "coverage": {
+      "open_prs": {
+        "fetched_at": "2026-10-17T17:10:26.456052+00:00",
+        "complete_pagination": true,
+        "records": 245
+      },
+      "discussions": {
+        "fetched_at": "2026-10-17T17:10:54.622748+00:00",
+        "complete_pagination": true,
+        "records": 1987
+      }
+    },
+    "warnings": [],
+    "exact_profile_hits": "own claim and local package only; not a novelty guarantee"
+  },
+  "publication_checks": "Exact committed export and raw Git-byte preflight are performed after committing; their receipts will be linked in the PR/Discussion."
+}

research/p112-unequal-endpoint-deletion/ENGINEERING.md

@@ -0,0 +1,71 @@
+# Bounded implementation and checks
+
+The kept change is one isolated research package. It calls an unchanged,
+SHA256-bound geometry module rather than copying or editing predecessor code.
+The real result is the written characteristic-zero implication in PROOF.md;
+the finite replay checks its declared premises and arithmetic, not the whole
+multiplication theorem. No subagent or independent human review was available.
+
+## Power-of-ten inspection
+
+1. All new paths use structured loops, exceptions and context-managed files.
+   There is no recursion. Input/proof failures propagate as nonzero exits;
+   output files are closed on success or failure.
+2. Weights have length at most ten, support invoices have exactly six
+   endpoints, and dimensions are at most sixteen. Historical enumeration
+   checks 7,546 multisets. Prior covers inspect at most 210 index quartets
+   and 81 assignments per quartet. Endpoint enumeration has `7^6` assignments.
+   The inherited geometry has fixed dimensions and exactly 4,097,782 flat
+   iterations. Each registered command has a 120-second bound; the historical
+   subprocess has a 30-second bound. The test subprocess emits 24 lines.
+3. Python allocates managed objects during execution. Direct fixed-memory
+   compliance is unavailable in this runtime. Live state is bounded by those
+   input sizes: the geometry keeps small histograms and at most 120 roots,
+   not a stored list of millions of flats; the historical list has 69 rows.
+   Each input is limited to two megabytes before reading. The interpreter and
+   standard-library internals were not allocation-instrumented.
+4. AST inspection finds maximum new function lengths of 24, 19 and 15 lines
+   in ledger.py, test_verify.py and verify.py, respectively.
+5. Explicit `require` contracts remain active with `-OO`. They check dimensions,
+   strict support cutoffs, exact input inventories/hashes, profile inclusion,
+   arithmetic margins and receipt equality. Tests use unittest checks rather
+   than removable Python assertions. No density-only assertions were added.
+6. Mutable evidence is function-local. The only import-path change is scoped
+   with `finally` and undone immediately. No shared cache or frontier record
+   is modified. Test patches are scoped and disposable copies are private.
+7. Source reads, exclusive writes and the historical child process either
+   return checked results or raise. The child is SHA-bound, uses no shell,
+   has a timeout and checks its exit code, stderr and exact row count.
+8. No generated code, decorators or evaluation of input text is introduced.
+   The one late ordinary module import is necessary to authenticate the
+   retained source first. The registered runner supplies private bytecode
+   isolation. Direct execution assumes a trusted interpreter/import cache.
+9. Calls are direct and data access is shallow. unittest dispatch and scoped
+   mock patches are bounded standard-library test mechanisms, not production
+   plug-ins. The input module name and location are fixed in the driver.
+10. The registered interpreter uses `-W error`; tests also use `-OO`. Applicable
+    Ruff checks cover E4,E7,E9,F,B,C4,ICN,PIE,PGH,RUF,UP,SIM,I. Compilation uses
+    `compile` in memory and AST function-length inspection, leaving no bytecode.
+    CHECKS.json records the exact commands. The replay manifest makes behavior
+    and warning checks recur when the package or a declared input changes.
+
+Rules 3 and 9 use managed-runtime/framework deviations. Their scope is this
+bounded one-shot Python replay and unittest suite; collection bounds, timeout
+checks, cross-version execution and disposable-copy cleanup are the compensating
+controls. A future port to a fixed-memory runtime must implement fixed-capacity
+buffers before claiming direct compliance. No such port is needed for this
+mathematical contribution.
+
+An exploratory Ruff ALL scan also suggested converting unittest to pytest,
+adding namespace-package markers and forbidding CLI output/late imports, plus
+project-wide annotation/docstring style. Those policies do not apply to this
+standard-library standalone verifier. Applicable complexity, import ordering,
+tuple construction and comparison findings were resolved. No suppression is
+added to source. The applicable check set above passes; a clean ALL result is
+not claimed.
+
+The registered replay, independent subset oracle, failure controls, mutation
+checks and source-only export are verification evidence. The geometric engine
+is re-executed, not independently reimplemented. Standard Weyl theory and the
+original decoder reduction remain written dependencies. No Lean, Docker,
+physical implementation, native supplier or full selected replay was run.

research/p112-unequal-endpoint-deletion/PROOF.md

@@ -0,0 +1,183 @@
+# Two unequal-endpoint P112 exclusions
+
+## Statement and exact change
+
+Use the fixed 112 nonframe E8 root lines `r_t`, their nine-bit binary labels
+`ell(t)`, and the code
+
+```
+C = {c_h : c_h(t)=<r_t,h>, h in K^8},
+w(q) = rank_F2 {ell(t) : q(t) != 0}.
+```
+
+The field `K` has characteristic zero. All intersections and independence
+below are over `K`; only support weights use binary rank.
+
+**Nine-piece theorem.** Nine independent pieces with weight bounds either
+`3,5,5,5,6,6,6,6,6` or `4,4,5,5,6,6,6,6,6` span a space `T0` with
+`dim(T0 intersect C)<=4`.
+
+**Ten-piece consequence.** Ten independent pieces with code intersection
+of dimension at least six cannot have either TWOSIDE profile
+`3,5^3,6^5,7` or `4^2,5^2,6^5,7`. The last piece can actually be unrestricted.
+
+This applies Nick Petalas/PR3169's existing A5 coordinate inequality after
+the dimension-deletion step of PR3197. The new callers have six unequal
+endpoint capacities `12,20,20,20,20,20`, rather than six twenties. No new
+geometric inequality, full C5 result, decoder floor, supplier or exponent
+is claimed.
+
+## Replayed geometric premises and written dependency
+
+The unchanged, declared `geometry.py` input reconstructs the roots and
+labels and binds them to the declared P112 data. It checks the following
+finite premises, inherited from PR3164/3169 and PR3161/3162.
+
+* Weight-three and weight-four supports have at most four and eight
+  coordinates. The labels are distinct and odd, so a binary `d`-space
+  contains at most `2^(d-1)` of them. Weight-five and weight-six supports
+  have capacities twelve and twenty. The replay enumerates all 3,309,747
+  five-flats and 788,035 six-flats in the nine-dimensional label space.
+* A nonzero codeword has at least 53 live coordinates. A codeword supported
+  on fewer than seventy coordinates is proportional to a root codeword.
+* The Gram sum in doubled root coordinates is `112 I`, so evaluation from
+  `K^8` into `C` is injective.
+* A plane containing three distinct E8 root lines is A2. Relative to the
+  first two roots, the third has coefficient ratio `+1` or `-1`.
+
+The support classification uses the standard Weyl-chamber theorem, not a
+short-vector enumeration. In a closed chamber, perpendicular roots are
+generated by vanishing simple roots. The 28 six-node parabolics have at
+most 36 root lines. The eight seven-node faces have counts
+`42,28,22,14,16,23,37,63`; only the last admits 43 perpendicular live lines,
+and its normal is a root. Root directions have live support 53 or 56.
+This proves the distance and the below-seventy classification over the
+reals. Reflection closure, simple-root positivity, the face counts and
+all 7,140 root-line planes are replayed exactly.
+
+For an arbitrary characteristic-zero field, the rational roots perpendicular
+to a field-valued direction have rational rank at most seven. If their rank
+were at most six while there were at least 43 of them, a generic real normal
+to their span would contradict the rank-six parabolic bound. Their rational
+kernel is therefore one-dimensional. The field-valued direction is a field
+scalar times its rational generator, to which the real classification
+applies. This includes complex coefficients without a positive-definite
+field-valued norm. The standard Weyl-chamber theorem and the original
+decoder reduction remain written dependencies, not proof-kernel results.
+
+## Nine pieces and six root-simplex vertices
+
+Suppose `dim(T0 intersect C)>=5`. In either weight profile take the first
+three pieces as `s1,s2,s3`, and call the other six `q0,...,q5`. Put
+
+```
+S = supp(s1) union supp(s2) union supp(s3),    s=|S|<=28,
+U = sum_i |supp(q_i)| <= 12+5*20 = 112,
+D0 = T0 intersect C.
+```
+
+For the first profile, the small-support bound is `4+12+12=28`. For the
+second it is `8+8+12=28`. Their endpoint capacities are identical.
+
+The quotient `T0/D0` has dimension at most four. For every `i`, the four
+images of `s1,s2,s3,q_i` are independent: a dependence would give a nonzero
+codeword supported on at most `28+20=48<53` coordinates. Nonzero follows
+from independence of the original pieces. Consequently the quotient has
+exact dimension four, and `dim D0=5`.
+
+After quotienting by the three small images, all six endpoint images are
+nonzero in one dimension. Rescale them to agree. Their supports and
+independence do not change. For suitable small-piece combinations `a_i`,
+
+```
+c0=0,    c_i=q_i-q0-a_i in D0,    i=1,...,5.
+```
+
+The five codewords are independent, as witnessed by their distinct nonzero
+coefficients on `q1,...,q5`. Every nonzero edge `c_i-c_j` has support at most
+`28+20+20=68<70`, and hence is a root direction. Injectivity gives five
+independent direction vectors.
+
+Normalize real E8 roots to squared norm two. Write those vectors as
+`h_i=b_i alpha_i`. Every difference is also a root direction, so the A2
+plane fact forces `b_i/b_j` to be `+1` or `-1`. Absorb signs into the roots.
+There is one common nonzero scalar `b`, and all distinct
+`<alpha_i,alpha_j>=1`. Thus the six vertices `0,alpha_1,...,alpha_5` form
+an affine root A5 simplex. This argument remains valid over `K`: a rational
+root in the field span of two independent rational roots lies in their
+rational span, by a nonsingular rational coordinate minor.
+
+## The inherited coordinate inequality, with the correct endpoint bill
+
+At any root coordinate the six simplex values lie on at most two adjacent
+integer levels, except when that coordinate is an edge root. In the latter
+case their equality multiplicities are `1,1,4`. In either case at most nine
+of the fifteen pairs have unequal values. The common field scalar changes
+no equalities.
+
+Outside `S`, edge values are exactly `q_i(t)-q_j(t)`. If `k` of the six
+endpoint values are nonzero, their number of unequal pairs is at most
+
+```
+k(6-k) + k(k-1)/2 = k(11-k)/2 <= 4k+1,    0<=k<=6.
+```
+
+This last inequality follows from `(k-1)(k-2)>=0` for integer `k`. It needs
+no restrictions on the nonzero field values. Summing inside and outside
+`S`, and using the distance 53 on all fifteen edges, gives PR3169's bound
+
+```
+795 = 15*53 <= 9s + 4U + (112-s) = 112+8s+4U.
+```
+
+The present endpoints give
+
+```
+795 <= 112+8*28+4*112 = 784,
+```
+
+a contradiction of eleven. This proves both nine-piece statements. The
+older `9s+5U` bound gives 812 and is insufficient. Charging six twenties
+instead gives 816 even in the coordinate bound. Both losing controls are
+retained; neither is an exclusion. The replay also enumerates all `7^6`
+assignments of six values with zero distinguished, representing every
+possible equality pattern.
+
+## Delete the unrestricted piece
+
+Let `T` be the span of ten independent pieces and `T0` the span after
+removing the last one. Its codimension is one. Restricting the map
+`T intersect C -> T/T0` shows
+
+```
+dim(T0 intersect C) >= dim(T intersect C)-1 >= 5.
+```
+
+Either retained profile contradicts the nine-piece theorem. No weight or
+support assumption on the removed piece is used. Removing two pieces
+would guarantee only four code dimensions, not five.
+
+## Original residue and prior coverage
+
+Both targets pass DreamingOfClouds/PR3154's original TWOSIDE `(6,4)`
+filters, with excess `35<36`. A direct transcription reproduces all 69
+historical survivors; the unchanged declared `bk2b.py` corroborates the
+count. This is not a claim that 69 profiles remain open today.
+
+All 210 four-piece index subsets and all `3^4` assignments to two six-flat
+groups plus paid cuts are checked. For `3,5^3,6^5,7`, support-certified basis
+types are `3,5,5,5` and `3,5,5,6`, each needing at least sixteen paid cuts.
+For `4^2,5^2,6^5,7`, the basis types are `4,4,5,5`, `4,4,5,6` and
+`4,5,5,6`, with minima sixteen, sixteen and twenty. Thus none of the
+weight-certified covers reaches the earlier fourteen-cut rule, or the
+smaller eight/ten-cut rules. The only nonbasis weight-four anchor occurs
+in the twenty-cut case, outside the twelve-cut anchor theorem.
+These are comparisons of named sufficient routes, not exclusions of
+unknown actual support overlaps or every possible earlier proof.
+
+The targets are not componentwise consequences of PR3197's
+`4^3,6^6,7` caller, nor PR3195's shorter `5^2,6^6,7` caller. The unequal
+endpoint bill is essential for this particular application. No full C5,
+`C(P112)>=64`, physical realization, supplier admission, multiplication
+theorem or new kappa is established. Evidence is author-checked; independent
+human review, hosted CI and proof-kernel verification are separate.