From 95b683196950efea6f3d7ac66745e00dba73425e Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Sat, 17 Oct 2026 15:22:23 +0100 Subject: [PATCH] feat(research): exclude P112 4,5^9 by quotient parity --- research/p112-quotient-parity/CHECKS.json | 57 +++++ research/p112-quotient-parity/ENGINEERING.md | 70 +++++++ research/p112-quotient-parity/PROOF.md | 152 ++++++++++++++ research/p112-quotient-parity/README.md | 75 +++++++ research/p112-quotient-parity/RESULT.json | 206 +++++++++++++++++++ research/p112-quotient-parity/SOURCES.json | 57 +++++ research/p112-quotient-parity/TASK.json | 66 ++++++ research/p112-quotient-parity/VERIFY.json | 34 +++ research/p112-quotient-parity/geometry.py | 188 +++++++++++++++++ research/p112-quotient-parity/quotient.py | 85 ++++++++ research/p112-quotient-parity/test_verify.py | 153 ++++++++++++++ research/p112-quotient-parity/verify.py | 89 ++++++++ 12 files changed, 1232 insertions(+) create mode 100644 research/p112-quotient-parity/CHECKS.json create mode 100644 research/p112-quotient-parity/ENGINEERING.md create mode 100644 research/p112-quotient-parity/PROOF.md create mode 100644 research/p112-quotient-parity/README.md create mode 100644 research/p112-quotient-parity/RESULT.json create mode 100644 research/p112-quotient-parity/SOURCES.json create mode 100644 research/p112-quotient-parity/TASK.json create mode 100644 research/p112-quotient-parity/VERIFY.json create mode 100644 research/p112-quotient-parity/geometry.py create mode 100644 research/p112-quotient-parity/quotient.py create mode 100644 research/p112-quotient-parity/test_verify.py create mode 100644 research/p112-quotient-parity/verify.py diff --git a/research/p112-quotient-parity/CHECKS.json b/research/p112-quotient-parity/CHECKS.json new file mode 100644 index 0000000000..9113976e18 --- /dev/null +++ b/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" + } +} diff --git a/research/p112-quotient-parity/ENGINEERING.md b/research/p112-quotient-parity/ENGINEERING.md new file mode 100644 index 0000000000..59fabfa27b --- /dev/null +++ b/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. diff --git a/research/p112-quotient-parity/PROOF.md b/research/p112-quotient-parity/PROOF.md new file mode 100644 index 0000000000..1d69dbd345 --- /dev/null +++ b/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)=, 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 =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. diff --git a/research/p112-quotient-parity/README.md b/research/p112-quotient-parity/README.md new file mode 100644 index 0000000000..4fb2dbf482 --- /dev/null +++ b/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. diff --git a/research/p112-quotient-parity/RESULT.json b/research/p112-quotient-parity/RESULT.json new file mode 100644 index 0000000000..c53177b43c --- /dev/null +++ b/research/p112-quotient-parity/RESULT.json @@ -0,0 +1,206 @@ +{ + "schema": "p112-quotient-parity/v1", + "input_sha256": "ac4a48851b922f2a433684b60c74768ae3bb4fc5e8990ffe63e3942bb3c2ea34", + "chamber": { + "simple_reflection_checks": 960, + "rank_six_parabolic_counts": [ + 21, + 21, + 12, + 12, + 15, + 21, + 30, + 16, + 13, + 12, + 13, + 16, + 21, + 12, + 10, + 10, + 12, + 16, + 10, + 8, + 8, + 10, + 13, + 12, + 13, + 21, + 21, + 36 + ], + "ray_zero_counts": [ + 42, + 28, + 22, + 14, + 16, + 23, + 37, + 63 + ], + "root_support_histogram": { + "53": 112, + "56": 8 + } + }, + "root_planes": { + "2": 3780, + "3": 3360 + }, + "five_flat_capacity": { + "dimension": 5, + "subspaces": 3309747, + "maximum": 12, + "histogram": { + "0": 99593, + "2": 6720, + "3": 71680, + "4": 300076, + "5": 258048, + "6": 729344, + "7": 442368, + "8": 826770, + "9": 200704, + "10": 287168, + "11": 43008, + "12": 44268 + } + }, + "simplex_control": { + "vertices": [ + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -2, + 2, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -2, + 0, + 2, + 0, + 0, + 0, + 0, + 0 + ], + [ + -2, + 0, + 0, + 2, + 0, + 0, + 0, + 0 + ], + [ + -2, + 0, + 0, + 0, + 2, + 0, + 0, + 0 + ], + [ + -2, + 0, + 0, + 0, + 0, + 2, + 0, + 0 + ] + ], + "incidence_histogram": [ + 2, + 0, + 0, + 0, + 0, + 36, + 0, + 0, + 42, + 32, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "odd_matching": { + "matchings": 232, + "unmatched_histogram": [ + 0, + 105, + 0, + 105, + 0, + 21, + 0, + 1 + ] + }, + "application": { + "weights": [ + 4, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5 + ], + "four_piece_support_cap": 48, + "five_circuit_support_cap": 60, + "small_union_cap": 44, + "remaining_support_sum_cap": 72, + "edge_support_cap": 68, + "edge_incidence_lower": 795, + "edge_incidence_upper": 756, + "contradiction_margin": 39, + "failed_old_quotient_support_cap": 56 + }, + "original_filter_control": { + "b": 5, + "t": 5, + "prefix_caps": [ + 68, + 80, + 92, + 104, + 116 + ], + "sum_weight_minus_two": 29, + "smallest_five_support_cap": 56, + "original_BK_BK7_survivor": true + } +} diff --git a/research/p112-quotient-parity/SOURCES.json b/research/p112-quotient-parity/SOURCES.json new file mode 100644 index 0000000000..83fe070dd5 --- /dev/null +++ b/research/p112-quotient-parity/SOURCES.json @@ -0,0 +1,57 @@ +{ + "schema_version": 1, + "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/one-sided-six-multisets/data/data.txt", + "usage": "input", + "git_blob": "dc591a4e0252bac096e6c63c51058f6caee66bfe", + "sha256": "ac4a48851b922f2a433684b60c74768ae3bb4fc5e8990ffe63e3942bb3c2ea34" + } + ], + "historical_sources": [ + { + "head": "708f0ad8928c383de8294aea3c126e9461d2066d", + "path": "research/p112-reduction-to-conjectures/checks/TWOSIDE/NOTES.md", + "git_blob": "e3fd3f2b1dfd77b597f000b38ec2dbec3dbca931", + "sha256": "226cd59ccc6bc065319e5e4c4768c889206169ff58f74ef4053eeadc5b2e03c8" + }, + { + "head": "708f0ad8928c383de8294aea3c126e9461d2066d", + "path": "research/p112-reduction-to-conjectures/checks/TWOSIDE/bk2b.py", + "git_blob": "3394029014bb13f16225587a153fa7b70016de6d", + "sha256": "dff16eff255c883db372a587cf3f34e6f35c08f75c60af9d11952be5a5838807" + }, + { + "head": "857384079ab640a949fb7618b7909664d3e737e5", + "path": "research/p112-root-simplex-exclusion/geometry.py", + "git_blob": "222ea556faf2b275f73815c4e7d0d5f1e3294f2f", + "sha256": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021" + }, + { + "head": "2dbbd3004b70772cef200e341037c7c05b094fbc", + "path": "research/p112-ten-piece-simplex/PROOF.md", + "git_blob": "278072bdaf6e0f067655491a61317f115f38160f", + "sha256": "21cd2f726865241c65641fb3e966c5ab3ae51694e47169d491b077ca73f547a2" + } + ], + "historical_source_contract": "Exact heads, blobs and SHA256 were checked locally. These are historical citations, not replay dependencies. Replay uses package code/proof and the declared canonical-main P112 input.", + "code_origins": { + "geometry.py": "Nick Petalas/PR3164 via PR3169, narrowed to the rank-five capacity needed here; root/label reconstruction retains DreamingOfClouds and E8/P112 lineage.", + "quotient.py": "New odd-matching lemma controls and application arithmetic.", + "verify.py": "P112 byte binding and A5 fixture adapted from PR3169; new matching and application replay bindings.", + "test_verify.py": "New rational six-circuit oracle and behavioral controls." + } +} diff --git a/research/p112-quotient-parity/TASK.json b/research/p112-quotient-parity/TASK.json new file mode 100644 index 0000000000..95d97979e0 --- /dev/null +++ b/research/p112-quotient-parity/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 6, + "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?", + "starting_points": [ + "certificates/selected-result.json", + "research/hyperplane-end-lean/PROOF.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove an odd-class quotient-basis lemma and exclude the actual P112 TWOSIDE (5,5) profile 4,5^9 over characteristic-zero fields.", + "scope_change_reason": "Taking the live C5 handoff in Discussion3156/PR3169. This is a mathematical boundary proof with exact finite dependencies, not a proof-assistant formalization.", + "bottleneck_link": "Closes one explicit decoder-floor configuration by repairing the quotient-independence gap. It does not admit a supplier or change kappa.", + "budget_minutes": 60, + "stop_rule": "Stop once the named profile is excluded with a complete proof and replayed geometric dependencies, or a falsifying witness is found. Do not expand to full C5.", + "outcome": "completed", + "evidence": "PROOF.md, RESULT.json and test_verify.py; exact flat/root replay and separate internal read-only mathematical reviews.", + "author": "Nick Petalas", + "ai_assistance": "Development and local checks used substantial automated assistance; no independent human or proof-kernel review is claimed.", + "open_questions": [ + { + "question": "Does the six-circuit root-plane restriction exclude another actual remaining beta profile?", + "why_it_matters": "It changes quotient-basis selection rather than weakening a failed support test.", + "first_step": "Pin a remaining live cell, check four-image independence and five-circuit root support, then check the complete edge-incidence bill.", + "blocked_by": "No other cell or profile is claimed here; the edge cutoff can fail when all ten weights are five." + }, + { + "question": "Can the quotient selection lemma be kernel-verified independently of E8?", + "why_it_matters": "The general linear algebra and odd-class step can be separated from finite root geometry.", + "first_step": "Formalize ten vectors, independence of every four, and the at-most-five-points four-flat hypothesis; derive a four-set through a prescribed triple with no extra image.", + "blocked_by": "No proof-assistant environment or verified geometry import is supplied." + } + ] +} diff --git a/research/p112-quotient-parity/VERIFY.json b/research/p112-quotient-parity/VERIFY.json new file mode 100644 index 0000000000..a6deb11db2 --- /dev/null +++ b/research/p112-quotient-parity/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/one-sided-six-multisets/data/data.txt" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact input binding, all rank-five flats, Weyl/parabolic facts, all root planes, odd partitions, named profile and committed receipt equality." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Fourteen behavioral groups: rational circuit kernels, parity failure, malformed inputs, strict support cutoffs, root planes, endpoint counts and input mutations." + } + ] +} diff --git a/research/p112-quotient-parity/geometry.py b/research/p112-quotient-parity/geometry.py new file mode 100644 index 0000000000..e7c6cbf6c5 --- /dev/null +++ b/research/p112-quotient-parity/geometry.py @@ -0,0 +1,188 @@ +"""Exact E8/P112 geometry; coordinates follow PR3162's retained convention. + +Root and label reconstruction derive from Nick Petalas's PR3161/PR3162, +with the E8/P112 lineage retained in SOURCES.json. Apache-2.0. +""" + +from fractions import Fraction +from itertools import combinations, product +from math import gcd, lcm + +SIMPLE = ( + (1, -1, -1, -1, -1, -1, -1, 1), + (2, 2, 0, 0, 0, 0, 0, 0), + (-2, 2, 0, 0, 0, 0, 0, 0), + (0, -2, 2, 0, 0, 0, 0, 0), + (0, 0, -2, 2, 0, 0, 0, 0), + (0, 0, 0, -2, 2, 0, 0, 0), + (0, 0, 0, 0, -2, 2, 0, 0), + (0, 0, 0, 0, 0, -2, 2, 0), +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b, strict=True)) + + +def canonical(row): + return max(tuple(row), tuple(-x for x in row)) + + +def primitive(row): + denominator = lcm(*(x.denominator for x in row)) + integers = tuple(int(x * denominator) for x in row) + divisor = gcd(*integers) + require(divisor != 0, "zero projective direction") + return canonical(tuple(x // divisor for x in integers)) + + +def root_lines(): + roots = set() + for i, j in combinations(range(8), 2): + for sign in (-2, 2): + row = [0] * 8 + row[i], row[j] = 2, sign + roots.add(canonical(row)) + for row in product((-1, 1), repeat=8): + if sum(x == -1 for x in row) % 2 == 0: + roots.add(canonical(row)) + require(len(roots) == 120, "E8 root-line count") + return tuple(sorted(roots)) + + +def frame_lines(): + frame = [] + for i in range(0, 8, 2): + for sign in (-2, 2): + row = [0] * 8 + row[i], row[i + 1] = 2, sign + frame.append(canonical(row)) + return tuple(frame) + + +def solve(matrix, rhs): + """Exact eight-dimensional elimination, also used by the chamber check.""" + require(len(matrix) == len(rhs) == 8, "linear-system dimension") + rows = [[Fraction(x) for x in row] + [Fraction(y)] + for row, y in zip(matrix, rhs, strict=True)] + require(all(len(row) == 9 for row in rows), "linear-system row dimension") + for col in range(8): + pivot = next((i for i in range(col, 8) if rows[i][col]), None) + require(pivot is not None, "singular linear system") + rows[col], rows[pivot] = rows[pivot], rows[col] + scale = rows[col][col] + rows[col] = [x / scale for x in rows[col]] + for i in range(8): + if i != col: + scale = rows[i][col] + rows[i] = [x - scale * y + for x, y in zip(rows[i], rows[col], strict=True)] + return tuple(row[8] for row in rows) + + +def root_data(): + roots, frame = root_lines(), frame_lines() + points = tuple(row for row in roots if row not in frame) + matrix = tuple(zip(*SIMPLE, strict=True)) + coordinates = tuple(solve(matrix, row) for row in roots) + require(all(x.denominator == 1 for row in coordinates for x in row), + "nonintegral simple-root coordinates") + by_root = dict(zip(roots, coordinates, strict=True)) + labels = tuple(1 | sum((int(x) % 2) << (i + 1) + for i, x in enumerate(by_root[row])) for row in points) + require(len(points) == len(set(labels)) == 112, "P112 inventory") + require(all(0 < x < 512 and x & 1 for x in labels), "odd binary labels") + require(all(sum(r[i] * r[j] for r in points) == 112 * (i == j) + for i in range(8) for j in range(8)), "P112 spans eight dimensions") + return roots, points, labels, coordinates + + +def chamber_receipt(roots, points, coordinates): + for root in roots: + for simple in SIMPLE: + pairing = dot(root, simple) + require(dot(simple, simple) == 8 and pairing % 4 == 0, + "simple reflection normalization") + reflected = canonical(tuple(x - (pairing // 4) * y + for x, y in zip(root, simple, strict=True))) + require(reflected in roots, "root system is not reflection closed") + require(all(all(x >= 0 for x in c) or all(x <= 0 for x in c) + for c in coordinates), "simple system positivity") + six_counts = [sum(all(c[i] == 0 for i in omitted) for c in coordinates) + for omitted in combinations(range(8), 2)] + rays = [primitive(solve(SIMPLE, [int(i == j) for i in range(8)])) + for j in range(8)] + ray_zeros = [sum(dot(h, r) == 0 for r in roots) for h in rays] + require(max(six_counts) == 36, "rank-six parabolic cap") + require(ray_zeros == [42, 28, 22, 14, 16, 23, 37, 63], "chamber rays") + root_directions = {primitive(tuple(map(Fraction, r))) for r in roots} + require(rays[7] in root_directions, "qualifying ray is not a root") + support_sizes = [sum(dot(r, t) != 0 for t in points) for r in roots] + require(sorted(support_sizes) == [53] * 112 + [56] * 8, "root support sizes") + # These finite facts support the Weyl-chamber proof in PROOF.md. + return {"simple_reflection_checks": 960, + "rank_six_parabolic_counts": six_counts, "ray_zero_counts": ray_zeros, + "root_support_histogram": {"53": 112, "56": 8}} + + +def root_plane_receipt(roots): + """Every third root line in a root plane is the A2 sum/difference.""" + require(len(roots) == len(set(roots)) == 120 + and all(len(r) == 8 and dot(r, r) == 8 for r in roots), + "normalized root-plane input") + gram = tuple(tuple(dot(a, b) for b in roots) for a in roots) + histogram = {2: 0, 3: 0} + for i, j in combinations(range(120), 2): + d = gram[i][j] + require(d in (-4, 0, 4), "nonparallel root inner product") + in_plane = [] + for k in range(120): + x, y = gram[i][k], gram[j][k] + determinant = 512 + 2 * d * x * y - 8 * (d*d + x*x + y*y) + if determinant == 0: + in_plane.append(k) + expected = {i, j} + if d: + third = canonical(tuple(a - (d // 4) * b + for a, b in zip(roots[i], roots[j], strict=True))) + require(third in roots, "missing A2 root") + expected.add(roots.index(third)) + require(set(in_plane) == expected, "unexpected third root line") + histogram[len(in_plane)] += 1 + return {str(k): v for k, v in histogram.items()} + + +def flat_capacity(labels, dimension): + require(dimension == 5, "only five-flat capacity is used") + require(len(labels) == len(set(labels)) == 112 + and all(type(x) is int and 0 < x < 512 and x & 1 for x in labels), + "invalid P112 labels") + all_lines = (1 << 112) - 1 + kernels = tuple(all_lines ^ sum(1 << i for i, label in enumerate(labels) + if (label & x).bit_count() & 1) for x in range(512)) + histogram = [0] * 113 + annihilator_dimension = 9 - dimension + for pivots in combinations(range(9), annihilator_dimension): + row_kernels = [] + for pivot in pivots: + free = tuple(c for c in range(pivot) if c not in pivots) + rows = tuple((1 << pivot) | sum(((code >> i) & 1) << col + for i, col in enumerate(free)) + for code in range(1 << len(free))) + row_kernels.append(tuple(kernels[row] for row in rows)) + for chosen in product(*row_kernels): + mask = all_lines + for row in chosen: + mask &= row + histogram[mask.bit_count()] += 1 + expected = (3309747, 12) + require(sum(histogram) == expected[0], "incomplete annihilator census") + maximum = max(i for i, n in enumerate(histogram) if n) + require(maximum == expected[1], "flat capacity changed") + return {"dimension": dimension, "subspaces": sum(histogram), "maximum": maximum, + "histogram": {str(i): n for i, n in enumerate(histogram) if n}} diff --git a/research/p112-quotient-parity/quotient.py b/research/p112-quotient-parity/quotient.py new file mode 100644 index 0000000000..94cffb7a87 --- /dev/null +++ b/research/p112-quotient-parity/quotient.py @@ -0,0 +1,85 @@ +"""Finite controls for the quotient-parity proof. Apache-2.0. + +The universal linear-algebra proof is in PROOF.md. Matchings encode its +rank-four-flat restriction; they do not enumerate every quotient matroid. +""" + +from itertools import combinations + +from geometry import require + + +def partial_matchings(size): + """Enumerate all matchings on at most eight vertices without recursion.""" + require(type(size) is int and 0 <= size <= 8, "matching size outside 0..8") + edges = tuple(combinations(range(size), 2)) + result = [] + for count in range(size // 2 + 1): + for chosen in combinations(edges, count): + used = [v for edge in chosen for v in edge] + if len(set(used)) == len(used): + result.append(chosen) + return result + + +def good_extension(partners): + """Return an unmatched vertex; reject a malformed or perfect matching.""" + require(isinstance(partners, tuple) and len(partners) <= 8, "partner shape") + for i, j in enumerate(partners): + require(j is None or (type(j) is int and 0 <= j < len(partners) + and j != i and partners[j] == i), + "partners must form an involution without fixed points") + free = [i for i, j in enumerate(partners) if j is None] + require(bool(free), "perfect matching has no good extension") + return free[0] + + +def matching_receipt(): + histogram = [0] * 8 + matchings = partial_matchings(7) + for edges in matchings: + partners = [None] * 7 + for i, j in edges: + partners[i], partners[j] = j, i + chosen = good_extension(tuple(partners)) + require(partners[chosen] is None, "selected extension is matched") + histogram[sum(x is None for x in partners)] += 1 + require(len(matchings) == 232, "incomplete seven-vertex matching census") + require(histogram == [0, 105, 0, 105, 0, 21, 0, 1], "matching counts") + return {"matchings": len(matchings), "unmatched_histogram": histogram} + + +def application(): + """The named weight profile and strict thresholds, not a feasibility search.""" + small = 8 + 3 * 12 + remaining = 6 * 12 + edge_cap = small + 2 * 12 + lower = 15 * 53 + upper = 9 * small + 5 * remaining + require(4 * 12 < 53 and 5 * 12 < 70, "four-independence/circuit cutoffs") + require(edge_cap < 70 and lower > upper, "root-edge/incidence cutoffs") + return {"weights": [4] + [5] * 9, "four_piece_support_cap": 48, + "five_circuit_support_cap": 60, "small_union_cap": small, + "remaining_support_sum_cap": remaining, "edge_support_cap": edge_cap, + "edge_incidence_lower": lower, "edge_incidence_upper": upper, + "contradiction_margin": lower - upper, + "failed_old_quotient_support_cap": small + 12} + + +def original_filter_control(): + """Bind this literal profile to the pinned TWOSIDE necessary filters.""" + weights = (4,) + (5,) * 9 + caps = {4: 8, 5: 12} + prefixes = [sum(caps[w] for w in weights[:10 - (5 - level)]) + for level in range(1, 6)] + require(prefixes == [68, 80, 92, 104, 116], "TWOSIDE prefix caps") + require(prefixes[0] >= 53 and prefixes[1] >= 78 + and all(x >= y for x, y in zip(prefixes[2:], (92, 100, 106), strict=True)), + "profile fails original feasibility filters") + excess = sum(w - 2 for w in weights) + basis_cap = sum(caps[w] for w in weights[:5]) + require(excess == 29 and excess < 30 and basis_cap == 56, + "profile fails original budget or is support-basis certified") + return {"b": 5, "t": 5, "prefix_caps": prefixes, + "sum_weight_minus_two": excess, "smallest_five_support_cap": basis_cap, + "original_BK_BK7_survivor": True} diff --git a/research/p112-quotient-parity/test_verify.py b/research/p112-quotient-parity/test_verify.py new file mode 100644 index 0000000000..da8bd868d8 --- /dev/null +++ b/research/p112-quotient-parity/test_verify.py @@ -0,0 +1,153 @@ +"""Behavioral and failure controls, including separate rational circuit checks.""" + +import tempfile +import unittest +from fractions import Fraction +from itertools import combinations, product +from math import comb +from pathlib import Path + +from geometry import ( + canonical, + dot, + flat_capacity, + require, + root_data, + root_plane_receipt, +) +from quotient import ( + application, + good_extension, + matching_receipt, + original_filter_control, + partial_matchings, +) +from verify import DATA, ROOT, bind_data, simplex_control + + +def rational_rank(matrix): + """Small independent oracle; fixed bounds cover only the fixtures below.""" + require(len(matrix) <= 8 and all(len(row) <= 10 for row in matrix), "rank bounds") + rows = [list(map(Fraction, row)) for row in matrix] + require(bool(rows) and len({len(row) for row in rows}) == 1, "rank shape") + rank = 0 + for col in range(len(rows[0])): + pivot = next((i for i in range(rank, len(rows)) if rows[i][col]), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + scale = rows[rank][col] + rows[rank] = [x / scale for x in rows[rank]] + for i in range(rank + 1, len(rows)): + factor = rows[i][col] + rows[i] = [x - factor * y + for x, y in zip(rows[i], rows[rank], strict=True)] + rank += 1 + if rank == len(rows): + break + return rank + + +class QuotientControls(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.roots, cls.points, cls.labels, _ = root_data() + + def test_all_odd_matchings(self): + self.assertEqual(matching_receipt()["matchings"], 232) + # Independent telephone-number recurrence. + counts = [1, 1] + for n in range(2, 8): + counts.append(counts[-1] + (n - 1) * counts[-2]) + self.assertEqual(counts[7], len(partial_matchings(7))) + + def test_even_parity_is_required(self): + with self.assertRaisesRegex(ValueError, "perfect matching"): + good_extension((1, 0, 3, 2, 5, 4)) + self.assertTrue(any(len(edges) == 3 for edges in partial_matchings(6))) + + def test_bad_partner_contracts(self): + for partners in ((0,), (1, None), (2, 0), (True, 0), [None] * 7): + with self.subTest(partners=partners), self.assertRaises(ValueError): + good_extension(partners) + + def test_matching_capacity(self): + for size in (-1, 9, True): + with self.assertRaises(ValueError): + partial_matchings(size) + + def test_six_distinct_five_piece_circuit_lines(self): + # Six rational moment-curve columns in dimension four. This realizes + # the forbidden abstract restriction before imposing E8 root geometry. + columns = [tuple(t ** k for k in range(4)) for t in range(6)] + for indices in combinations(range(6), 4): + self.assertEqual(rational_rank([columns[i] for i in indices]), 4) + w = [(-1) ** i * comb(5, i) for i in range(6)] + circuits = [[w[i] * (i - j) for i in range(6)] for j in range(6)] + for j, circuit in enumerate(circuits): + self.assertEqual([i for i, x in enumerate(circuit) if not x], [j]) + self.assertEqual([sum(circuit[i] * columns[i][k] for i in range(6)) + for k in range(4)], [0] * 4) + self.assertEqual(rational_rank(circuits), 2) + self.assertEqual(len({canonical(row) for row in circuits}), 6) + + def test_generic_quotient_has_good_extension(self): + columns = [tuple(t ** k for k in range(5)) for t in range(10)] + chosen = columns[:4] + self.assertEqual(rational_rank(chosen), 4) + for column in columns[4:]: + self.assertEqual(rational_rank([*chosen, column]), 5) + + def test_root_plane_inventory(self): + self.assertEqual(root_plane_receipt(self.roots), {"2": 3780, "3": 3360}) + + def test_mutated_root_plane_input(self): + with self.assertRaisesRegex(ValueError, "root-plane input"): + root_plane_receipt(self.roots[:-1]) + + def test_root_supports_and_injective_gram(self): + self.assertEqual({sum(dot(r, p) != 0 for p in self.points) + for r in self.roots}, {53, 56}) + gram = [[sum(p[i] * p[j] for p in self.points) for j in range(8)] + for i in range(8)] + self.assertEqual(rational_rank(gram), 8) + + def test_simplex_and_endpoint_counts(self): + control = simplex_control(self.roots, self.points) + maximum = max(i for i, n in enumerate(control["incidence_histogram"]) if n) + self.assertEqual(maximum, 9) + # Exhaust all six endpoint assignments from a four-level alphabet. + for values in product(range(4), repeat=6): + k = sum(x != 0 for x in values) + self.assertLessEqual(sum(a != b for a, b in combinations(values, 2)), 5 * k) + + def test_input_binding_and_mutation(self): + bind_data(ROOT / DATA, self.points, self.labels) + with tempfile.TemporaryDirectory() as directory: + path = Path(directory) / "data.txt" + path.write_bytes((ROOT / DATA).read_bytes() + b"\n") + with self.assertRaisesRegex(ValueError, "changed P112 input"): + bind_data(path, self.points, self.labels) + with self.assertRaisesRegex(ValueError, "label binding"): + bind_data(ROOT / DATA, self.points, tuple(reversed(self.labels))) + + def test_unused_capacity_and_label_mutants(self): + with self.assertRaises(ValueError): + flat_capacity(self.labels, 6) + with self.assertRaisesRegex(ValueError, "invalid P112 labels"): + flat_capacity((0, *self.labels[1:]), 5) + + def test_exact_application_and_old_failure(self): + row = application() + self.assertEqual(row["contradiction_margin"], 39) + self.assertEqual(row["edge_support_cap"], 68) + self.assertGreaterEqual(row["failed_old_quotient_support_cap"], 53) + # Losing the cap-eight piece makes the root-edge test fail. + self.assertGreaterEqual(4 * 12 + 2 * 12, 70) + + def test_original_filter_binding(self): + self.assertTrue(original_filter_control()["original_BK_BK7_survivor"]) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/p112-quotient-parity/verify.py b/research/p112-quotient-parity/verify.py new file mode 100644 index 0000000000..3fc81600ba --- /dev/null +++ b/research/p112-quotient-parity/verify.py @@ -0,0 +1,89 @@ +"""Replay exact dependencies and controls for the P112 quotient-parity theorem.""" + +import argparse +import hashlib +import json +from itertools import combinations +from pathlib import Path + +from geometry import ( + canonical, + chamber_receipt, + dot, + flat_capacity, + require, + root_data, + root_plane_receipt, +) +from quotient import application, matching_receipt, original_filter_control + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +DATA = "research/one-sided-six-multisets/data/data.txt" + + +def bind_data(path, points, labels): + require(path.is_file() and path.stat().st_size <= 2_000_000, "missing/large input") + raw = path.read_bytes() + pins = json.loads((PACKAGE / "SOURCES.json").read_text())["files"] + live = [row for row in pins if row["usage"] == "input"] + require(len(live) == 1 and live[0]["path"] == DATA, "live-input inventory") + digest = hashlib.sha256(raw).hexdigest() + require(digest == live[0]["sha256"], "changed P112 input") + rows = raw.decode("utf-8").splitlines() + require(len(rows) >= 114, "truncated P112 input") + require(tuple(map(int, rows[0].split())) == labels, "label binding") + require(tuple(tuple(map(int, row.split())) for row in rows[2:114]) == points, + "root binding") + return digest + + +def simplex_control(roots, points): + vertices = [(0,) * 8] + for i in range(1, 6): + vertex = [0] * 8 + vertex[0], vertex[i] = -2, 2 + vertices.append(tuple(vertex)) + edges = [canonical(tuple(x - y for x, y in zip(a, b, strict=True))) + for a, b in combinations(vertices, 2)] + require(len(set(edges)) == 15 and all(e in roots for e in edges), "A5 fixture") + histogram = [0] * 16 + for point in points: + values = [dot(point, vertex) for vertex in vertices] + histogram[sum(a != b for a, b in combinations(values, 2))] += 1 + require(max(i for i, n in enumerate(histogram) if n) == 9, "A5 incidence cap") + return {"vertices": vertices, "incidence_histogram": histogram} + + +def receipt(): + roots, points, labels, coordinates = root_data() + return {"schema": "p112-quotient-parity/v1", + "input_sha256": bind_data(ROOT / DATA, points, labels), + "chamber": chamber_receipt(roots, points, coordinates), + "root_planes": root_plane_receipt(roots), + "five_flat_capacity": flat_capacity(labels, 5), + "simplex_control": simplex_control(roots, points), + "odd_matching": matching_receipt(), "application": application(), + "original_filter_control": original_filter_control()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="write a new external receipt") + args = parser.parse_args() + result = receipt() + if args.output is None: + require(json.loads(json.dumps(result)) + == json.loads((PACKAGE / "RESULT.json").read_text()), + "committed receipt differs") + else: + output = args.output.expanduser().resolve() + require(not output.is_relative_to(ROOT), "output must be outside checkout") + with output.open("x", encoding="utf-8") as stream: + stream.write(json.dumps(result, indent=2) + "\n") + print("PASS_P112_QUOTIENT_PARITY exclusions=1 margin=39 " + "flats=3309747 root_planes=7140 matchings=232 errors=0") + + +if __name__ == "__main__": + main()