Research: exclude P112 4,5^9 with quotient parity

research/p112-quotient-parity/CHECKS.json

@@ -0,0 +1,57 @@
+{
+  "status": "local_checks_passed",
+  "checked_utc": "2026-10-17T14:21:14.401632+00:00",
+  "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a",
+  "priority_revision": 6,
+  "environment": {
+    "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O",
+    "python_versions": [
+      "3.12.15",
+      "3.13.16"
+    ],
+    "dependencies": "standard library only"
+  },
+  "commands": [
+    {
+      "command": "TMPDIR=$RUN uv run --python 3.12 --no-project python -W error -B scripts/research_package.py --package research/p112-quotient-parity",
+      "result": "PASS; complete geometry and fourteen optimized behavioral groups"
+    },
+    {
+      "command": "TMPDIR=$RUN uv run --python 3.13 --no-project python -W error -B export/research/p112-quotient-parity/verify.py",
+      "result": "PASS; read-only Git-free Python 3.13 export"
+    },
+    {
+      "command": "TMPDIR=$RUN uv run --python 3.13 --no-project python -O -W error -B export/research/p112-quotient-parity/test_verify.py",
+      "result": "PASS; read-only Git-free Python 3.13 export"
+    },
+    {
+      "command": "RUFF_CACHE_DIR=$RUN/ruff-cache uv tool run ruff check research/p112-quotient-parity --select E,F,B,I,UP,SIM,RUF",
+      "result": "PASS"
+    },
+    {
+      "command": "warnings-as-errors source compilation with compile(), no bytecode writes",
+      "result": "PASS"
+    }
+  ],
+  "coverage": {
+    "five_flats": 3309747,
+    "root_plane_pairs": 7140,
+    "simple_reflections": 960,
+    "seven_vertex_matchings": 232,
+    "behavioral_groups": 14,
+    "new_named_exclusions": 1,
+    "contradiction_margin": 39
+  },
+  "review": "Two internal read-only mathematical reviews and one final artifact review found no objection. The artifact review separately replayed Python 3.12 verification and fourteen optimized controls and checked all seven source pins. No independent human or proof-kernel verification is claimed.",
+  "limits": [
+    "Standard Weyl-chamber theorem is used.",
+    "No full C5/decoder-floor/supplier replay or selected-frontier update.",
+    "Hosted CI is separate.",
+    "Root-restricted capacity probes rejected an initial approach; they are not proof dependencies."
+  ],
+  "upstream_refresh": {
+    "utc": "2026-10-17T14:21:28.857609+00:00",
+    "canonical_main": "997e6a9ca7b4f95d50e366f61412fd640d72a88a",
+    "guidance_change": "none"
+  }
+}

research/p112-quotient-parity/ENGINEERING.md

@@ -0,0 +1,70 @@
+# Implementation bounds and decisions
+
+The checkable predicate is one new exclusion for the literal TWOSIDE profile
+`4,5^9`, with all finite geometric dependencies replayed and a complete
+characteristic-zero proof. The outcome meets that predicate. No broader
+census, supplier replay or selected-frontier change was attempted.
+
+Build the Lever changed the deliverable from a prose argument to a registered
+standard-library replay. Prove It Works changed verification to exact source
+binding, full five-flat/root-plane enumeration, a rational circuit fixture,
+optimized failure controls and publication-byte comparison. Unslop shaped the
+scope and limitations in the proof and README. The retained code is assessed
+against Power of Ten as follows.
+
+- All control flow is structured and nonrecursive. Each function is below
+  sixty physical lines. Command failures propagate; external receipt output
+  is created exclusively and cannot overwrite a file or write inside the
+  checkout. Source input size is bounded before reading.
+- Loops use fixed E8 dimensions or validated bounded collections. The five-flat
+  census has exactly 3,309,747 states. Root-plane checking uses 7,140 pairs
+  times 120 possible lines. Reflection checking uses 120 times eight states.
+  The largest matching enumerator visits 24,158 edge subsets at size eight
+  and retains at most 764 matchings. The application uses exactly ten pieces.
+- Runtime contracts remain active with optimization; mathematical validity
+  does not rely on Python `assert`. Imported geometry validates its fixed
+  root/label inventories. No shared mutable state, network calls, recursion,
+  dynamic evaluation or plugin dispatch occurs in the production replay.
+- Rule 3 deviation: Python integers, Fraction and containers allocate during
+  operation. Scope is this finite standard-library verifier; fixed dimensions,
+  bounded input size and sequential 120-second command limits constrain it.
+  The census streams masks into a 113-bin histogram rather than retaining
+  millions of spaces. Revisit allocation only if the domain is expanded.
+- Rules 8 and 9 deviation: unittest discovers fourteen local test methods and
+  uses runtime dispatch. The production verifier uses explicit calls. The
+  fixed test module runs under optimization and returns failure status.
+  No additional discovery paths or registrations are admitted by VERIFY.json.
+- Rule 10: warnings-as-errors execution, source compilation and Ruff's
+  E,F,B,I,UP,SIM,RUF checks cover the retained Python paths. An exploratory
+  Ruff ALL scan also reported annotation/docstring/copyright conventions,
+  pytest-only suggestions and magic-number style rules. Those conventions
+  do not match this standard-library executable proof package; replacing
+  unittest assertions would disable the optimized controls. Applicable import,
+  line-length and collection-expression findings were corrected. No lint
+  suppressions were added. Further type-checking would require an explicit
+  typed interface for inherited geometry, outside this proof's change.
+
+## Decision trail
+
+1. Reused the clean sparse worker from a fresh canonical-main baseline and
+   preserved all prior branches. Live overlap and the released PR3169 handoff
+   selected the quotient-independence question before implementation.
+2. Rejected the individual root-restricted flat-capacity idea. Complete probes
+   for representative support-53/support-56 roots retained maxima eight and
+   twelve, so that approach did not improve the failed support estimate.
+3. Used the six-circuit/root-plane restriction and odd proportionality classes
+   to select a valid four-piece quotient set. The older endpoint inequality
+   already gives margin 39; the stronger PR3169 count was unnecessary.
+4. A first test wrongly assumed the first eight ordered live roots span eight
+   dimensions. Their measured rank is four. The corrected independent control
+   computes the full live-root Gram matrix and verifies rank eight.
+5. The first receipt equality check compared tuples with parsed JSON lists.
+   Canonical JSON conversion fixes the representation comparison without
+   changing any proof-relevant value. Cross-version replay checks it directly.
+6. Exact environments, source pins, complete receipts and commands are retained
+   in CHECKS.json, SOURCES.json, RESULT.json and VERIFY.json. Disposable probes,
+   logs and exports are removed after publication.
+
+Internal read-only mathematical reviews corroborated the six-circuit,
+odd-class and characteristic-zero arguments. They do not substitute for
+independent human review or proof-kernel verification.

research/p112-quotient-parity/PROOF.md

@@ -0,0 +1,152 @@
+# A quotient-parity argument excludes the P112 profile `4,5^9`
+
+Let K have characteristic zero. For the pinned 112 live E8 root lines,
+write C={c_h : c_h(t)=<r_t,h>, h in K^8}. A piece q has weight equal to the
+binary rank of the labels on its support. Ten independent pieces spanning
+T with dim(T intersect C)>=5 cannot have weight bounds `4,5^9`.
+
+This theorem closes that explicit piece configuration. Its use in the
+TWOSIDE decoder reduction inherits the other hypotheses of that reduction.
+It does not establish full C5, the decoder floor, a supplier or a new kappa.
+
+## Exact geometric dependencies
+
+The proof uses these facts about the pinned P112 set:
+
+1. Weight at most four gives support size at most eight; weight at most
+   five gives support size at most twelve.
+2. A nonzero codeword has support at least 53. If its support is below 70,
+   its direction is a scalar multiple of an E8 root.
+3. Evaluation h -> c_h is injective, and a plane contains at most three
+   root lines. If three distinct root lines lie in a plane generated by
+   two roots, the third has coefficient ratio +1 or -1 in those roots.
+
+Fact 1 in dimension four follows from the leading-one binary label bit:
+a d-flat meets that affine hyperplane in at most 2^(d-1) points. The
+five-flat bound is a complete enumeration of all 3,309,747 annihilator
+spaces, in unique reverse row-echelon form, with maximum twelve.
+
+For fact 2, the standard Weyl-chamber theorem moves a real direction to a
+closed chamber. Its perpendicular roots are generated by the simple roots
+on which it vanishes. Every parabolic on at most six simple roots has at
+most 36 root lines. The eight seven-node parabolics have line counts
+42,28,22,14,16,23,37,63. Only the final one can contain at least 43
+perpendicular live lines, which a support below 70 requires. Its normal
+is a root direction. Root live supports are 53 or 56. This also rules out
+nonzero support below 53.
+
+For K-valued directions, their perpendicular rational roots span dimension
+at most seven. If that span had dimension at most six, a generic real
+normal to it would have exactly those perpendicular roots. The preceding
+parabolic bound would allow at most 36 lines, contradicting 43. Thus at
+support below 70 the perpendicular span has dimension seven, and its
+rational one-dimensional normal supplies the same root classification.
+
+The live-root Gram sum is 112 times the identity in the doubled coordinates
+used by the verifier, giving injectivity over K. All 7,140 pairs of E8
+root lines have only two or three root lines in their rational plane, and
+every third is the A2 sum or difference. These finite facts are replayed.
+A rational root in the K-span of two independent rational roots has
+rational coefficients, by an invertible rational coordinate minor. The
+same plane inventory and coefficient ratios therefore hold over K.
+
+These arguments and the retained geometry code follow PR3164/PR3169.
+The Weyl-chamber theorem itself is a mathematical dependency, not a
+program-proved theorem. SOURCES.json pins the exact predecessor bytes.
+
+## Six points in a four-flat would force six roots in a plane
+
+Set D=T intersect C and Q=T/D. Let v_i be the ten piece images in Q.
+Every four are independent. Otherwise a nonzero linear combination of
+at most four independent pieces would be a codeword supported on at
+most 4*12=48<53 coordinates. The quotient has dimension at most five.
+
+Suppose a four-dimensional subspace of Q contained six v_i. Their original
+pieces span a six-dimensional space E. Their quotient rank is exactly
+four, so E intersect D has dimension two. Delete each of the six pieces
+in turn. The remaining five have quotient rank four, hence have a
+one-dimensional kernel L_i in E intersect D.
+
+The six L_i are distinct. If L_i=L_j, their common nonzero vector is
+supported on at most the four pieces other than i and j, contradicting
+four-image independence. Each L_i gives a nonzero codeword supported on
+at most 5*12=60<70 coordinates, hence a root direction. Evaluation
+injectivity maps the two-dimensional kernel back to a two-dimensional
+direction space containing six distinct root lines. Fact 3 forbids this.
+
+Consequently every four-flat contains at most five piece images. Also
+dim Q=5: the ten images span Q, and dimension at most four would place
+six of them in one four-flat.
+
+## An odd number of remaining points supplies a good four-set
+
+Fix any three pieces B including the piece assigned the weight-four bound.
+Their images are independent. In the two-dimensional space Q/span(v_B), the other seven
+images are nonzero. Each projective proportionality class has size at
+most two: three such images together with B would give six images in
+one four-flat.
+
+Seven is odd, so at least one class has size one. Adjoin its piece x to B.
+The resulting four images are independent, and their span contains none
+of the six remaining piece images. The four selected supports have union
+S with s=|S|<=8+3*12=44. This proves the independence step that the
+earlier support-only estimate 44+12=56 could not establish.
+
+The finite matching control enumerates all 232 partitions of seven
+vertices into singletons and pairs. It checks the parity consequence,
+not every possible quotient configuration. The preceding linear algebra
+is the universal proof that this control applies.
+
+## The six remaining pieces form an affine root A5 simplex
+
+Write the remaining pieces q_0,...,q_5. Modulo the selected four images,
+each has a nonzero class in one dimension. Rescale them to have equal
+classes. Supports do not change. For i=1,...,5 there is a unique selected
+piece combination a_i such that c_i=q_i-q_0-a_i belongs to D. Set c_0=0.
+
+The five c_i are independent: their coefficients on q_1,...,q_5 in the
+original ten-piece basis are distinct unit vectors. Every difference
+c_i-c_j is nonzero and has support in S union supp(q_i) union supp(q_j),
+of size at most 44+12+12=68<70. Thus c_i=c_{h_i} for independent h_i,
+and all differences among 0,h_1,...,h_5 are scalar root directions.
+
+Normalize roots to norm squared two. Write h_i=b_i alpha_i. Each
+h_i-h_j is a third root line in the plane of alpha_i and alpha_j, so
+b_i/b_j is +1 or -1. Absorb signs into the roots. All b_i then equal one
+nonzero scalar b, and alpha_i-alpha_j is a root, so <alpha_i,alpha_j>=1.
+This is an affine root A5 simplex.
+
+At a live coordinate r, its six integer endpoint levels have pairwise
+differences in {-2,-1,0,1,2}. If a difference has absolute value two,
+Cauchy-Schwarz makes r the corresponding edge root. The multiplicities
+are then 1,1,4, giving nine unequal endpoint pairs. Otherwise there are
+at most two consecutive levels, giving at most 3*3=9 unequal pairs.
+The common field scalar changes no zeros. Each coordinate therefore
+belongs to at most nine of the fifteen edge supports.
+
+Outside S, the edge values are q_i(t)-q_j(t). If k of the six endpoints
+are nonzero, at most k(6-k)+k(k-1)/2 <=5k pairs differ. Thus, writing
+U=sum_i |supp(q_i)|<=72 and summing edge supports, we obtain
+
+```
+15*53 <= 9s+5U <= 9*44+5*72 = 756 < 795 = 15*53.
+```
+
+The contradiction has margin 39. The stronger coordinate-budget inequality
+of PR3169 is unnecessary.
+
+## Binding and limits
+
+The literal profile `4,5^9` passes the original TWOSIDE `(5,5)` BK/BK7
+weight filters in DreamingOfClouds's PR3154. Here the five retained prefix
+support caps at levels one through five are 68,80,92,104,116, meeting
+the relevant thresholds. Its total sum(w-2)=29 is below 30. The five
+smallest support caps sum to 56, so the original support-certified
+quotient-basis test does not apply. PR3169 explicitly leaves this profile
+as an open next question. We close it by replacing that test with the
+six-circuit and odd-class arguments above. No claim about the total number
+of currently remaining beta shapes is made.
+
+The proof is over every characteristic-zero field. Exact finite geometry
+and meaningful failure controls support it; no proof-kernel verification
+or independent human review is claimed. The selected frontier is unchanged.

research/p112-quotient-parity/README.md

@@ -0,0 +1,75 @@
+# An odd-class quotient argument excludes P112 `4,5^9`
+
+Ten independent P112 pieces with code intersection dimension at least five
+cannot have binary support-rank bounds `4,5^9`, over any characteristic-zero
+field. This is the explicit TWOSIDE `(5,5)` profile left as an open next
+question by [PR3169](https://github.com/CrocSwap/integer-mult-bounds/pull/3169).
+
+The earlier support estimate gave 56 where quotient independence required
+less than 53. The new proof selects a different quotient basis. Six piece
+images in a four-flat would force six distinct E8 root lines into a plane,
+which has at most three. Contracting a triple containing the distinguished
+weight-four piece leaves seven points in classes of size at most two.
+An odd number guarantees a singleton and hence the required four-piece set.
+The resulting root-simplex incidence count gives `795 <= 756`, a contradiction
+with margin 39. [PROOF.md](PROOF.md) states every hypothesis and implication.
+
+[RESULT.json](RESULT.json) records the complete 3,309,747-flat census,
+all 7,140 root-plane pairs, 960 reflections, all 232 seven-vertex matchings,
+and the literal profile's original weight-filter binding. Fourteen behavioral
+groups include an independently calculated rational six-circuit fixture,
+even-parity and malformed-partner failures, strict support cutoffs, exact
+endpoint counts and changed-input rejection.
+
+This closes one finite decoder-floor configuration. Full C5, `C(P112)>=64`,
+supplier admission and an improved kappa remain open. The selected conditional
+kappa is unchanged at `0.001672660197076918`.
+
+## Reproduce
+
+Python 3.12 or later, standard library only. From the repository root:
+
+```sh
+RUN="$HOME/.cache/integer-mult-bounds-runs/p112-quotient-parity-replay"
+mkdir -p "$RUN"
+TMPDIR="$RUN" uv run --python 3.12 --no-project python -W error -B \
+  scripts/research_package.py --package research/p112-quotient-parity
+```
+
+An existing Python 3.12 executable can replace the `uv run` prefix. The two
+registered commands run sequentially with 120-second limits. The first checks
+inputs and reconstructs the mathematical receipt; the second runs the controls
+with optimization enabled. `verify.py --output NEW_PATH` writes a new external
+receipt and refuses to overwrite an existing file. Git-free direct replay uses
+`verify.py` and `test_verify.py`, with this package and its single declared
+P112 input at the same repository-relative path. [CHECKS.json](CHECKS.json)
+records actual environments, commands and verification limits.
+
+## Open next questions
+
+Does the six-circuit restriction help another actual remaining beta profile?
+Pin the live cell and check its four-piece and five-circuit support bounds
+before expanding. The all-weight-five case already fails this proof's edge
+cutoff, so no extension is claimed. Separately, the quotient-selection lemma
+could be kernel-verified with the four-flat restriction as an abstract premise.
+Structured questions and blockers are in [TASK.json](TASK.json).
+
+## Credit and scope
+
+Nick Petalas contributed the quotient-parity proof and this named exclusion.
+DreamingOfClouds's [PR3154](https://github.com/CrocSwap/integer-mult-bounds/pull/3154)
+provides TWOSIDE, its necessary weight filters and the C5 handoff.
+Nick Petalas's [PR3164](https://github.com/CrocSwap/integer-mult-bounds/pull/3164)
+provides the root-simplex proof and geometry code; [PR3169](https://github.com/CrocSwap/integer-mult-bounds/pull/3169)
+identifies the specific failed independence step. The retained E8/P112 and
+decoder lineage includes DreamingOfClouds's packages and joaqcoo's original
+model. [SOURCES.json](SOURCES.json) records exact heads, paths, Git blobs,
+SHA256 hashes and code origins. Historical sources were checked locally;
+fresh CI needs canonical-base provenance and the sole declared live input.
+All new and reused code is Apache-2.0. Frozen predecessors remain unchanged.
+
+Development and local checks used substantial automated assistance. Internal
+read-only mathematical reviews are not independent human review. The standard
+Weyl-chamber theorem is an explicit dependency; no proof-kernel verification or
+complete supplier replay is claimed. [ENGINEERING.md](ENGINEERING.md) records
+bounded implementation decisions and the retained decision trail.