From 3949cc17a4fa4f108a044f532a5d58323c6cb6d2 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Sat, 17 Oct 2026 17:44:05 +0100 Subject: [PATCH] feat(research): exclude P112 4^3,6^6,7 by deletion --- .../p112-weight-seven-deletion/CHECKS.json | 154 +++ .../p112-weight-seven-deletion/DECISIONS.tsv | 6 + .../p112-weight-seven-deletion/ENGINEERING.md | 59 + research/p112-weight-seven-deletion/PROOF.md | 205 ++++ research/p112-weight-seven-deletion/README.md | 73 ++ .../p112-weight-seven-deletion/RESULT.json | 1076 +++++++++++++++++ .../p112-weight-seven-deletion/SOURCES.json | 68 ++ research/p112-weight-seven-deletion/TASK.json | 60 + .../p112-weight-seven-deletion/VERIFY.json | 29 + .../p112-weight-seven-deletion/geometry.py | 188 +++ .../p112-weight-seven-deletion/obstruction.py | 126 ++ .../p112-weight-seven-deletion/test_verify.py | 194 +++ .../vendor/COORDINATE-PROOF.md | 203 ++++ .../vendor/NOTICE.md | 18 + .../vendor/TWOSIDE-NOTES.md | 65 + .../p112-weight-seven-deletion/vendor/bk2b.py | 29 + research/p112-weight-seven-deletion/verify.py | 127 ++ 17 files changed, 2680 insertions(+) create mode 100644 research/p112-weight-seven-deletion/CHECKS.json create mode 100644 research/p112-weight-seven-deletion/DECISIONS.tsv create mode 100644 research/p112-weight-seven-deletion/ENGINEERING.md create mode 100644 research/p112-weight-seven-deletion/PROOF.md create mode 100644 research/p112-weight-seven-deletion/README.md create mode 100644 research/p112-weight-seven-deletion/RESULT.json create mode 100644 research/p112-weight-seven-deletion/SOURCES.json create mode 100644 research/p112-weight-seven-deletion/TASK.json create mode 100644 research/p112-weight-seven-deletion/VERIFY.json create mode 100644 research/p112-weight-seven-deletion/geometry.py create mode 100644 research/p112-weight-seven-deletion/obstruction.py create mode 100644 research/p112-weight-seven-deletion/test_verify.py create mode 100644 research/p112-weight-seven-deletion/vendor/COORDINATE-PROOF.md create mode 100644 research/p112-weight-seven-deletion/vendor/NOTICE.md create mode 100644 research/p112-weight-seven-deletion/vendor/TWOSIDE-NOTES.md create mode 100644 research/p112-weight-seven-deletion/vendor/bk2b.py create mode 100644 research/p112-weight-seven-deletion/verify.py diff --git a/research/p112-weight-seven-deletion/CHECKS.json b/research/p112-weight-seven-deletion/CHECKS.json new file mode 100644 index 0000000000..8e6082aa39 --- /dev/null +++ b/research/p112-weight-seven-deletion/CHECKS.json @@ -0,0 +1,154 @@ +{ + "schema": "p112-weight-seven-deletion-checks/v1", + "environment": { + "primary_python": "3.12.15 (main, Oct 14 2026, 01:05:27) [Clang 23.1.3 ]", + "secondary_python": "Python 3.13.5", + "platform": "Linux-6.6.87.2-microsoft-standard-WSL2-x86_64-with-glibc2.41", + "ruff": "ruff 0.17.1" + }, + "scientific_source_sha256": { + "geometry.py": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021", + "obstruction.py": "6ab2507c39d46e21a168da7fb75778e40e3cf72a37480374243e69c75bae1909", + "verify.py": "7c370b618ca280bea29bc664b55529b57a656365d357267059bf8b19e95040c6", + "test_verify.py": "eb02cd02958e2fafbfe452c1d689b21522a424dcbdff3739afff87be4f2805a8", + "PROOF.md": "209512bc56c21a5621ab34bb1ffd4df82a093c63526bb6496730e8f66bddfe41", + "RESULT.json": "d0bc2126bd28187978aa17816e7a386579196fa305c87608beef3f35a96a2078", + "SOURCES.json": "793fd4a4428aeb146ede42e4c140e0415c80a2cf6d5df071630a139b6d81ac13", + "TASK.json": "aaeeef313bc9304bb3fcc6670a06765d42c6e0ee0e9f24824c0974de3d25627e", + "VERIFY.json": "6c120e1d288f96685cb945c4959861a321affff9bc1577065d14751789e3186f" + }, + "scope": { + "profile": [ + 4, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + "intersection_lower": 6, + "new_profile_exclusions": 1, + "concurrent_PR3195_profile_counted_as_new": false, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/3156#discussioncomment-19001119" + }, + "checks": [ + { + "command": [ + "python3.12", + "-B", + "scripts/research_package.py", + "--package", + "research/p112-weight-seven-deletion" + ], + "result": "PASS_REGISTERED_RESEARCH_PACKAGE outcome=partial; complete finite replay and all fifteen behavioral groups" + }, + { + "command": [ + "python3.12", + "-W", + "error", + "-B", + "research/p112-weight-seven-deletion/test_verify.py" + ], + "result": "PASS 15 tests" + }, + { + "command": [ + "ruff", + "check", + "--no-cache", + "--select", + "E,F,B,UP,C4", + "research/p112-weight-seven-deletion/geometry.py", + "research/p112-weight-seven-deletion/obstruction.py", + "research/p112-weight-seven-deletion/verify.py", + "research/p112-weight-seven-deletion/test_verify.py" + ], + "result": "All checks passed" + }, + { + "command": [ + "python3.12", + "-W", + "error", + "-m", + "py_compile", + "research/p112-weight-seven-deletion/geometry.py", + "research/p112-weight-seven-deletion/obstruction.py", + "research/p112-weight-seven-deletion/verify.py", + "research/p112-weight-seven-deletion/test_verify.py" + ], + "result": "PASS; bytecode redirected outside checkout" + } + ], + "read_only_source_export": { + "git_checkout": false, + "commands": [ + "python3.13 -O -W error -B research/p112-weight-seven-deletion/verify.py", + "python3.13 -O -W error -B research/p112-weight-seven-deletion/test_verify.py" + ], + "result": "PASS identical receipt and all fifteen tests from read-only package plus sole declared input; bytecode and temporary files external" + }, + "mutants": [ + { + "mutation": "free_dimension", + "test": "test_intersection_loss_is_sharp_not_free", + "rejected": true, + "exit": 1 + }, + { + "mutation": "wrong_coordinate", + "test": "test_new_bound_and_losing_old_bound", + "rejected": true, + "exit": 1 + }, + { + "mutation": "nonstrict_edge", + "test": "test_quotient_and_root_cutoffs_are_strict", + "rejected": true, + "exit": 1 + }, + { + "mutation": "nonstrict_budget", + "test": "test_original_profile_is_a_strict_budget_survivor", + "rejected": true, + "exit": 1 + } + ], + "retained_origin_checks": "All four exact retained source heads, Git blobs, SHA256 digests and raw byte comparisons pass. Concurrent PR3195 proof is pinned as historical overlap evidence, not imported at runtime.", + "internal_review": [ + "Dimension lens: codimension-one deletion guarantees five, not six, surviving code dimensions; nine retained pieces give quotient dimension four.", + "Geometry lens: all fifteen edges have support at most 64<70, so only the inherited root/A2 classification is used; no A5 orbit census or weight-seven endpoint tariff is assumed.", + "Artifact lens: fixed inventory, strict support boundaries, unchanged predecessor execution and mutated input/source/output controls pass." + ], + "freshness": { + "upstream_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "priority_revision": 6, + "checked_at": "2026-10-17T16:43:15.740266+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-17T16:42:45.083425+00:00", + "complete_pagination": true, + "records": 315 + }, + "discussions": { + "fetched_at": "2026-10-17T16:43:15.674823+00:00", + "complete_pagination": true, + "records": 1983 + } + }, + "warnings": [], + "scope": "No other exact ten-piece-profile match beyond the local package and its canonical claim; the helper does not search every code diff." + }, + "limits": [ + "Standard Weyl-chamber theorem is a written dependency, not proof-kernel verified.", + "Original decoder-level filters and full C1-C7 reduction are inherited, not re-proved.", + "No full supplier cold replay, physical construction, selected-frontier change or new kappa.", + "No independent human review or hosted CI result is claimed." + ], + "publication": "Post-commit raw-byte and exact committed source-export checks are reported with the PR; this record identifies the tested source bytes without a self-referential commit hash." +} diff --git a/research/p112-weight-seven-deletion/DECISIONS.tsv b/research/p112-weight-seven-deletion/DECISIONS.tsv new file mode 100644 index 0000000000..8d1fbff8eb --- /dev/null +++ b/research/p112-weight-seven-deletion/DECISIONS.tsv @@ -0,0 +1,6 @@ +timestamp phase decision reason evidence result +2026-10-17T16:28:10Z intake reuse worker no active owner or files git status, ignored inventory, process cwd clean; preexisting empty .ruff_cache preserved +2026-10-17T16:31:58Z selection narrow to 5^2,6^6,7 actual weight-seven handoff; other candidates already covered scope-probe.json; PR3169 coordinate inequality proposed 795<=784 contradiction +2026-10-17T16:32:38Z proof delete unrestricted ninth piece intersection drops by at most one; avoids a new weight-seven edge alphabet PR3169 inequality and quotient dimension eight pieces give margin 11 +2026-10-17T16:39:14Z overlap credit concurrent PR3195 and make one bounded pivot same original profile and deletion argument already published PR3195 22f1479; fresh 313 PR/1982 discussion corpus new target 4^3,6^6,7; no new count for old target +2026-10-17T16:43:15Z verification accept one ten-piece exclusion full replay and fifteen tests pass; strict and dimension mutants rejected RESULT.json; export and diagnostic logs 795<=784; no kappa change diff --git a/research/p112-weight-seven-deletion/ENGINEERING.md b/research/p112-weight-seven-deletion/ENGINEERING.md new file mode 100644 index 0000000000..92dc33a182 --- /dev/null +++ b/research/p112-weight-seven-deletion/ENGINEERING.md @@ -0,0 +1,59 @@ +# Implementation boundaries + +The new entry points are `verify.py` and `test_verify.py`. Only this package +and its declared immutable P112 input are read. A receipt may be created +only at an exclusive external path. No selected supplier, shared verifier, +frozen predecessor or global configuration is changed. + +Build the Lever shaped the choice to keep an exact rerunnable receipt rather +than just a numerical claim. Prove It Works shaped the complete capacity +replay, literal source binding and losing controls. The mathematical change +is dimension deletion before the existing coordinate inequality, not a new +abstraction or a larger search. + +## Power-of-ten inspection + +- No recursive calls, callbacks or unstructured control flow were introduced. + Exceptions propagate; the only output handle uses a context manager. +- Every search has fixed bounds. Geometry has 120 roots, 112 live lines and + nine binary coordinates. Flat enumeration covers 3,309,747 and 788,035 + subspaces. Endpoint checks cover `7^6` assignments. Historical profiles have + six weights and lengths six through ten; prior-cover tests use 210 index + quartets and at most 81 assignments per distinct basis. +- Functions remain below sixty physical lines. Internal assumptions use + always-enabled `require` checks; the replay also runs under optimized Python. +- State is local except fixed geometry/weight tables and package paths. + No code mutates those tables. Inputs have explicit size limits and + SHA256/semantic checks. CLI failures, + invalid dimensions, strict support cutoffs, changed inputs and output + conflicts are covered by tests. The CLI has no mutation other than optional + receipt creation, so no network or subprocess cleanup is needed there. +- The one test subprocess executes the retained original fixed checker with a + thirty-second timeout, captures its result and propagates failure. The + registered runner gives each command a 120-second limit. +- No generated code, reflection, runtime registration or indirect dispatch was + added to the proof path. The retained original checker is tested unchanged. +- Local diagnostics use Python warning mode and Ruff's applicable error, + undefined-name, bugbear, modernization and comprehension checks. No warnings + are suppressed. CI uses the registered standard-library replay and tests; + no repository-wide lint/build configuration is changed. + +## Managed-runtime deviation + +Rule: 3, fixed allocation after initialization. +Location: `geometry.py`, `obstruction.py`, `verify.py`, `test_verify.py`. +Reason: Python integers, exact rational elimination and collection iteration +allocate dynamically. Replacing them would expand this research contribution +into a different runtime implementation. +Scope: This finite standard-library replay only. +Compensating control: All combinatorial domains are fixed above; a flat mask +and histogram are processed at a time, not retained for millions of flats. +Source input is at most two million bytes and each retained source at most +100,000 bytes. Temporary test copies are context-managed and bounded to those +same files. No solver, native build, service or unbounded worklist is used. +Verification: Full replay, failure controls and a second-interpreter export. +Follow-up: Reassess allocation and capacity if any dimension or input limit is +made configurable. Current limits are not performance or memory benchmarks. + +The standard Weyl-chamber theorem, original decoder-level reduction and +independent human/proof-kernel review remain outside executable coverage. diff --git a/research/p112-weight-seven-deletion/PROOF.md b/research/p112-weight-seven-deletion/PROOF.md new file mode 100644 index 0000000000..88c96abdd7 --- /dev/null +++ b/research/p112-weight-seven-deletion/PROOF.md @@ -0,0 +1,205 @@ +# A ten-piece weight-seven residue closes after deletion + +## Statement + +Let `K` be any characteristic-zero field. Use the pinned 112 nonframe E8 +root lines `r_t` and their nine-bit labels `ell(t)`. Write + +``` +C = {c_h : c_h(t)=, h in K^8}, +w(q) = rank_F2 {ell(t) : q(t) != 0}. +``` + +**Nine-piece theorem.** If nine independent pieces span `T0` and have +weight upper bounds `4,4,4,6,6,6,6,6,6`, then + +``` +dim(T0 intersect C) <= 4. +``` + +**Ten-piece consequence.** Ten independent pieces spanning `T` with +`dim(T intersect C)>=6` cannot have weight upper bounds `4^3,6^6,7`. +In fact, the tenth piece can be unrestricted. + +This is one new application of Nick Petalas/PR3169's coordinate-budget +inequality, not a new inequality or a completed decoder-floor proof. +DreamingOfClouds/PR3154's historical TWOSIDE `(b,t)=(6,4)` filters retain +this exact ten-piece profile. Concurrent PR3195 already proves the distinct +eight-piece slice `5,5,6^6` and nine-piece caller `5,5,6^6,7`. That was our +initial target and is not counted as new here. The new profile has three +small pieces, nine retained pieces and a four-dimensional quotient. +No selected supplier or exponent changes here. + +## Finite geometric premises + +The retained `geometry.py` is byte-identical to PR3169's copy of PR3164's +geometry. The full replay reconstructs roots and labels and binds them to +`research/one-sided-six-multisets/data/data.txt`. Its finite checks support +the following premises from the retained predecessor proof. + +1. A weight-four support has at most eight live coordinates: all labels + have leading bit one, so the odd part of a four-dimensional binary + space has at most `2^3` points. A weight-six support has at most twenty. + Enumeration covers all 788,035 six-flats in `F2^9`. The replay also + retains the five-flat capacity twelve, over all 3,309,747 five-flats, + used in the historical filters and concurrent-source calibration. +2. A nonzero element of `C` has at least 53 nonzero coordinates. Every + codeword with support below seventy is proportional to a root codeword. +3. The P112 Gram sum is `112 I` in doubled root coordinates. Thus evaluation + `h -> c_h` is injective over `K`. +4. In the plane of two distinct E8 root lines, a third root line occurs only + in an A2 subsystem, with coefficient ratio `+1` or `-1`. + +For completeness, premise 2 uses the standard Weyl-chamber theorem, not a +finite short-vector search. At least 43 live root lines are perpendicular +to a direction of support below seventy. In a closed chamber, perpendicular +roots are generated by vanishing simple roots. All 28 six-node parabolics +contain at most 36 root lines. The eight seven-node face counts are +`42,28,22,14,16,23,37,63`; only the last reaches 43, and its normal is a +root. The 120 root directions have live support 53 or 56. This also gives +the distance 53. + +For a field-valued direction, its perpendicular rational roots have rational +rank at most seven. If their rank were at most six, a generic real normal +to their span would contradict the same rank-six root-subsystem bound. +Their rational kernel is therefore one-dimensional, so the direction is +proportional over `K` to a rational normal. Apply the real chamber argument +to that normal. This includes complex coefficients and does not assume a +positive-definite norm on `K`. + +The replay checks simple-root positivity, 960 simple reflections and all +7,140 root-line planes. The standard Weyl-chamber theorem is an explicit +written dependency. These checks do not formally prove that theorem. + +## Nine pieces give six affine vertices + +Assume for a contradiction that `dim(T0 intersect C)>=5`. Let `s1,s2,s3` +be the weight-four pieces and `q0,...,q5` the six weight-six pieces. Put + +``` +S = union_{j=1}^3 supp(s_j), s=|S|<=3*8=24, +U = sum_i |supp(q_i)|<=120, D0=T0 intersect C. +``` + +The quotient `T0/D0` has dimension at most four. The four images of +`s1,s2,s3,q_i` are independent for every `i`: any dependence would give a +nonzero codeword supported on at most `24+20=44<53` coordinates. The +combination is nonzero because the original pieces are independent. +Consequently the quotient dimension is exactly four and `dim D0=5`. + +Modulo the span of the three small images, all six `q_i` images are nonzero +in a one-dimensional space. Rescale the `q_i` so these images agree. This +changes neither their supports nor independence. There are small-piece +combinations `a_i` such that + +``` +c0=0, c_i=q_i-q0-a_i in D0, i=1,...,5. +``` + +The five codewords are independent by their distinct nonzero coefficients +on `q1,...,q5`. Every nonzero difference `c_i-c_j` has support at most + +``` +24+20+20=64<70. +``` + +Thus all fifteen edges are root directions. Injectivity gives five +independent `h_i` with `c_i=c_{h_i}`. + +## The inherited A5 coordinate budget + +Here is PR3169's argument with the same hypotheses. Normalize the real +roots to norm squared two. Write `h_i=b_i alpha_i`. A third root line in +the plane of `alpha_i,alpha_j` forces `b_i/b_j` to be `+1` or `-1`. +Absorb signs into the roots. Then `h_i=b alpha_i` with one common nonzero +field scalar, and `=1`. The six vertices +`0,alpha_1,...,alpha_5` form a root A5 simplex. The plane statement also +holds after scalar extension: a rational root in the field span of two +independent rational roots is in their rational span, using a nonsingular +rational coordinate minor. + +At any root coordinate, the six vertex evaluations have pairwise +differences in `{-2,-1,0,1,2}`. If a difference has absolute value two, +the coordinate is that edge root, and the equality multiplicities are +`1,1,4`. There are nine unequal pairs. Otherwise the values occupy at +most two consecutive integer levels, again giving at most nine unequal +pairs. The common field scalar changes no equalities. Hence every +coordinate lies in at most nine of the fifteen edge supports. + +Outside `S`, edge evaluations equal `q_i(t)-q_j(t)`. If exactly `k` endpoint +values are nonzero there, their unequal pairs number at most + +``` +k(6-k)+k(k-1)/2 = k(11-k)/2 <= 4k+1, +``` + +since `(k-1)(k-2)>=0` for integer `k=0,...,6`. This endpoint inequality +holds over any field. Summing it over the `112-s` outside coordinates, +and using the nine-incidence bound inside `S`, gives + +``` +15*53 <= 9s + 4U + 112-s = 112+8s+4U. +``` + +But `s<=24` and `U<=120`, so + +``` +795 <= 112+8*24+4*120 = 784, +``` + +a contradiction with margin eleven. This proves the nine-piece theorem. +The older `9s+5U` bound gives 816 and does not prove it. The replay retains +that losing control. At `s=26`, the new upper bound is 800, also insufficient; +the script must not report an exclusion at that boundary. + +## Delete one piece, not one code dimension for free + +For the ten-piece application let `T0` be the span after removing the +tenth piece. Independence gives `dim T0=9` and codimension one in `T`. +The map from `D=T intersect C` into `T/T0` has image of dimension at most +one and kernel `D intersect T0`. Therefore + +``` +dim(T0 intersect C) >= dim(T intersect C)-1 >= 5. +``` + +The remaining weights are `4^3,6^6`, contradicting the theorem. We do not +claim that all six original code dimensions survive, nor impose a free +weight-six tariff on the removed piece. Its support is never used. Thus +no weight-seven edge classification, rank-seven deletion census or new +consumer is needed for this particular profile. + +## Original residue, overlap and limits + +The independent transcription in `obstruction.py` reproduces all sixty-nine +historical `(6,4)` BK/BK7 survivors over all weight multisets of lengths six +through ten. The unmodified retained `vendor/bk2b.py` separately prints +`6 4 69 1`. The exact target has excess `35<36`, so it is a genuine original +strict-budget profile. Those historical filters are not a current count of +unresolved research, and their decoder-level derivation is inherited. + +The only support-certified four-piece quotient-basis type is `4,4,4,6`, +with support cap 44. Its best weight-certified cover by two six-flats needs +sixteen extra lines. Thus the earlier eight-, ten- and fourteen-cut rules +do not apply. Its six nonbasis weights are `6^5,7`, so the rank-four-anchor +rule also has no applicable nonbasis anchor. The audit checks all 210 index +quartets and every two-flat/paid assignment for each distinct basis. +These are checks of named sufficient routes, not a claim that every +conceivable earlier argument was unavailable. + +Concurrent PR3195 at `22f1479db213b1ed0de68cbc61ba15f6352d3276` proves +`5,5,6^6,7` by the same deletion idea and a stronger endpoint count. Our +initial independent derivation of that profile is corroboration, not a +new exclusion. The present ten-piece profile is not a componentwise +subprofile of its nine-piece caller: deleting two pieces would only +guarantee four surviving code dimensions, whereas that slice needs five. +The one bounded pivot retains three small rank-four pieces and applies the +already existing coordinate inequality with the correct quotient dimension +four. +PR3169's ten-piece argument uses four small pieces before normalization; +its coordinate inequality is fully credited, not counted as new here. + +No full C5, `C(P112)>=64`, supplier admission, physical realization, complete +multiplication theorem or new kappa is proved. This is an author-checked +written consequence with exact finite replay. Independent human review, +proof-kernel verification and hosted CI are separate. diff --git a/research/p112-weight-seven-deletion/README.md b/research/p112-weight-seven-deletion/README.md new file mode 100644 index 0000000000..a176432e82 --- /dev/null +++ b/research/p112-weight-seven-deletion/README.md @@ -0,0 +1,73 @@ +# A weight-seven P112 residue closes by deleting that piece + +Nine independent pieces of weights at most `4^3,6^6` have intersection +of dimension at most four with the P112 root code, over every +characteristic-zero field. Therefore ten pieces with code intersection +at least six cannot have the actual TWOSIDE `(6,4)` profile `4^3,6^6,7`. +The tenth piece can be unrestricted. + +Remove that piece first. At least five code dimensions survive, so Nick +Petalas/PR3169's existing root-A5 coordinate budget applies to the other +nine pieces, with three small supports and quotient dimension four. It +requires `795<=784`, a contradiction with margin eleven. The old incidence bound gives 816 and is insufficient. +See [the complete proof](PROOF.md). + +This continues [PR3192's weight-seven handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/3156#discussioncomment-19000918). +A concurrent [PR3195](https://github.com/CrocSwap/integer-mult-bounds/pull/3195) +proved the initial target `5,5,6^6,7`; that profile is not counted as new. +The one bounded pivot here is the distinct ten-piece caller above. +It does not prove full C5, `C(P112)>=64`, supplier admission or a new κ. +The selected frontier is unchanged. The proof uses the standard +Weyl-chamber theorem and the inherited original decoder reduction. +Evidence is author-checked, not independent human or proof-kernel review. + +## Evidence and reproduction + +[RESULT.json](RESULT.json) records all 4,097,782 five/six-flats, the exact +chamber and root-plane checks, all 117,649 six-endpoint patterns, the +historical sixty-nine-profile inventory and the single new application. +The retained unmodified TWOSIDE checker corroborates the inventory count. +Fifteen behavioral groups cover dimension loss, quotient normalization, +invalid hypotheses, a losing support boundary, source mutations and output +safety. [CHECKS.json](CHECKS.json) records commands and environment. + +From the repository root, with Python 3.12 and no third-party dependencies: + +```sh +python3.12 -B scripts/research_package.py --package research/p112-weight-seven-deletion +``` + +For direct replay, run `python3.12 -B research/p112-weight-seven-deletion/verify.py` +and then `test_verify.py` in the same directory. Neither writes results into +the checkout. An optional `--output /absolute/external/new-file.json` creates +an exclusive external receipt. Source-only exports must preserve the package +and the declared `research/one-sided-six-multisets/data/data.txt` input under +the same relative paths. Direct replay does not need pending PR Git objects. + +[TASK.json](TASK.json) declares the changed scope and stop rule. +[SOURCES.json](SOURCES.json) pins canonical main, exact predecessor heads, +Git blobs and source hashes. [ENGINEERING.md](ENGINEERING.md) records the +bounded implementation and verification limits. The geometry and retained +predecessor files are unchanged copies, not edits to frozen source packages. + +## Open next questions + +Before another geometric census, bind an actual still-open weight-seven +profile to its quotient and support hypotheses. A first step is to refresh +Discussion3156 and audit the historical `(6,4)` profiles against existing +dimension-deletion and rank-six bounds. The blocker is that a historical +survivor list is not a current scientific disposition ledger. The structured +question and stop rule are in [TASK.json](TASK.json). + +## Credit + +DreamingOfClouds/PR3154 supplied TWOSIDE and the original decoder-floor +reduction. Nick Petalas/PR3169 supplied the coordinate inequality; PR3164 +and PR3161/3162 supplied its root geometry and retained exact label checks. +PR3192 supplied the weight-seven handoff and distinct no-seven profile +application. Concurrent PR3195 supplied the earlier deletion application +for `5,5,6^6,7`, which was independently derived here before the overlap +refresh and is not claimed as a new result. The E8/P112 lineage, including +joaqcoo's model, remains credited in the predecessor sources. See [the retained-source notice](vendor/NOTICE.md). +New work is Apache-2.0. Development and local checks used substantial +automated assistance. diff --git a/research/p112-weight-seven-deletion/RESULT.json b/research/p112-weight-seven-deletion/RESULT.json new file mode 100644 index 0000000000..e802724368 --- /dev/null +++ b/research/p112-weight-seven-deletion/RESULT.json @@ -0,0 +1,1076 @@ +{ + "schema": "p112-weight-seven-deletion/v1", + "retained_sources": { + "geometry.py": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021", + "vendor/COORDINATE-PROOF.md": "21cd2f726865241c65641fb3e966c5ab3ae51694e47169d491b077ca73f547a2", + "vendor/bk2b.py": "dff16eff255c883db372a587cf3f34e6f35c08f75c60af9d11952be5a5838807", + "vendor/TWOSIDE-NOTES.md": "226cd59ccc6bc065319e5e4c4768c889206169ff58f74ef4053eeadc5b2e03c8" + }, + "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 + }, + "flat_capacities": [ + { + "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 + } + }, + { + "dimension": 6, + "subspaces": 788035, + "maximum": 20, + "histogram": { + "0": 10796, + "4": 56, + "6": 896, + "7": 4096, + "8": 8148, + "10": 56448, + "11": 86016, + "12": 124040, + "14": 131712, + "15": 143360, + "16": 141491, + "18": 33152, + "19": 28672, + "20": 19152 + } + } + ], + "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 + ] + ], + "live_edge_histogram": { + "0": 2, + "5": 36, + "8": 42, + "9": 32 + } + }, + "endpoint_controls": { + "value_assignments": 117649, + "nonzero_histogram": { + "0": 1, + "1": 36, + "2": 540, + "3": 4320, + "4": 19440, + "5": 46656, + "6": 46656 + }, + "losing_small_support_26": { + "small_support_cap": 26, + "endpoint_sum_cap": 120, + "quotient_support_cap": 46, + "edge_support_cap": 66, + "edge_incidence_lower": 795, + "old_incidence_upper": 834, + "coordinate_incidence_upper": 800, + "old_margin": -39, + "margin": -5, + "excluded": false + } + }, + "application": { + "historical_cell": [ + 6, + 4 + ], + "multisets_examined": 7546, + "historical_survivors": [ + [ + 2, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 2, + 2, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 2, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 6, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 2, + 6, + 6, + 6, + 6, + 6, + 7, + 7, + 7 + ], + [ + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 2, + 2, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 2, + 2, + 3, + 6, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 2, + 2, + 4, + 5, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 2, + 2, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 2, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 2, + 6, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 2, + 2, + 6, + 6, + 6, + 6, + 6, + 7, + 7, + 7 + ], + [ + 2, + 3, + 3, + 5, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 2, + 3, + 4, + 4, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 2, + 3, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 3, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 3, + 5, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 2, + 3, + 5, + 6, + 6, + 6, + 6, + 7, + 7, + 7 + ], + [ + 2, + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 2, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 2, + 4, + 4, + 6, + 6, + 6, + 6, + 7, + 7, + 7 + ], + [ + 2, + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 2, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 2, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 3, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 3, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 3, + 3, + 5, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 3, + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 3, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 3, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 3, + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 3, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 3, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 4, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 4, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 4, + 4, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 4, + 4, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 4, + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 4, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 5, + 5, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6 + ] + ], + "target": [ + 4, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + "retained_weights": [ + 4, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "original_intersection_lower": 6, + "removed_pieces": 1, + "retained_intersection_lower": 5, + "retained_quotient_dimension": 4, + "new_profile_exclusions": 1, + "concurrent_PR3195_profile_counted_as_new": false, + "prior_cover_audit": [ + { + "basis": [ + 4, + 4, + 4, + 6 + ], + "complement": [ + 6, + 6, + 6, + 6, + 6, + 7 + ], + "support_cap": 44, + "minimum_two_flat_cuts": 16, + "rank_four_anchor": false + } + ], + "small_support_cap": 24, + "endpoint_sum_cap": 120, + "quotient_support_cap": 44, + "edge_support_cap": 64, + "edge_incidence_lower": 795, + "old_incidence_upper": 816, + "coordinate_incidence_upper": 784, + "old_margin": -21, + "margin": 11, + "excluded": true + } +} diff --git a/research/p112-weight-seven-deletion/SOURCES.json b/research/p112-weight-seven-deletion/SOURCES.json new file mode 100644 index 0000000000..a24cceecf4 --- /dev/null +++ b/research/p112-weight-seven-deletion/SOURCES.json @@ -0,0 +1,68 @@ +{ + "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" + } + ], + "retained_sources": [ + { + "local_path": "geometry.py", + "source_head": "2dbbd3004b70772cef200e341037c7c05b094fbc", + "source_path": "research/p112-ten-piece-simplex/geometry.py", + "git_blob": "222ea556faf2b275f73815c4e7d0d5f1e3294f2f", + "sha256": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021" + }, + { + "local_path": "vendor/COORDINATE-PROOF.md", + "source_head": "2dbbd3004b70772cef200e341037c7c05b094fbc", + "source_path": "research/p112-ten-piece-simplex/PROOF.md", + "git_blob": "278072bdaf6e0f067655491a61317f115f38160f", + "sha256": "21cd2f726865241c65641fb3e966c5ab3ae51694e47169d491b077ca73f547a2" + }, + { + "local_path": "vendor/bk2b.py", + "source_head": "708f0ad8928c383de8294aea3c126e9461d2066d", + "source_path": "research/p112-reduction-to-conjectures/checks/TWOSIDE/bk2b.py", + "git_blob": "3394029014bb13f16225587a153fa7b70016de6d", + "sha256": "dff16eff255c883db372a587cf3f34e6f35c08f75c60af9d11952be5a5838807" + }, + { + "local_path": "vendor/TWOSIDE-NOTES.md", + "source_head": "708f0ad8928c383de8294aea3c126e9461d2066d", + "source_path": "research/p112-reduction-to-conjectures/checks/TWOSIDE/NOTES.md", + "git_blob": "e3fd3f2b1dfd77b597f000b38ec2dbec3dbca931", + "sha256": "226cd59ccc6bc065319e5e4c4768c889206169ff58f74ef4053eeadc5b2e03c8" + } + ], + "historical_source_contract": "Retained source bytes are authenticated by the standalone replay. Git heads and blobs were independently checked locally before publication; pending heads are historical citations, not required Git objects for a fresh checkout replay.", + "code_origins": { + "geometry.py": "Byte-identical to Nick Petalas/PR3169, inherited from PR3164 and PR3161/3162.", + "obstruction.py": "New dimension-deletion and nine-piece application of PR3169 coordinate inequality; TWOSIDE necessary filters independently transcribed from DreamingOfClouds/PR3154.", + "verify.py": "Input binding and A5 fixture adapted from Nick Petalas/PR3169; new rejection and quotient-rank controls." + }, + "concurrent_overlap": { + "pr": 3195, + "head": "22f1479db213b1ed0de68cbc61ba15f6352d3276", + "path": "research/p112-five-five-slice/PROOF.md", + "git_blob": "98c800a61d6e721945a8e75134ff13f163448066", + "sha256": "e7a7e4df499db263c830b28c23298882b00326746dc2938c3b79fba60bf2541d", + "scope": "Prior eight-piece 5^2,6^6 slice and nine-piece 5^2,6^6,7 application; independently derived initially here, not counted as new. New contribution changes the retained slice to 4^3,6^6 and the original caller to ten pieces." + } +} diff --git a/research/p112-weight-seven-deletion/TASK.json b/research/p112-weight-seven-deletion/TASK.json new file mode 100644 index 0000000000..51383bcf29 --- /dev/null +++ b/research/p112-weight-seven-deletion/TASK.json @@ -0,0 +1,60 @@ +{ + "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 the nine-piece P112 4^3,6^6 intersection bound and exclude the actual TWOSIDE (6,4) weight-seven profile 4^3,6^6,7 by deleting its unrestricted tenth piece.", + "scope_change_reason": "Took PR3192's live weight-seven handoff instead of the catalogue's hyperplane/Lean starting point. The submission refresh found concurrent PR3195 had proved our initial 5^2,6^6,7 target. That target is credited and not counted as new. One bounded pivot changes to the actual ten-piece 4^3,6^6,7 profile. This is a written quotient-dimension consequence of PR3169 with exact finite replay, not proof-kernel formalization.", + "bottleneck_link": "Closes one missing implication in the P112 decoder-floor reduction on the binding complex side. No full C5, decoder floor, supplier or exponent improvement is claimed.", + "budget_minutes": 60, + "stop_rule": "Stop after this one source-bound exclusion, a failed support/quotient premise or the sixty-minute session; do not expand the geometry census without another actual caller.", + "outcome": "partial", + "evidence": "PROOF.md proves the nine-piece theorem over every characteristic-zero field and the codimension-one transfer. RESULT.json replays all 4,097,782 five/six-flats, root/chamber premises, 117,649 endpoint patterns and exact historical-profile inclusion. CHECKS.json records controls and environment.", + "author": "Nick Petalas", + "ai_assistance": "Substantial automated assistance in derivation, implementation and local checks; no independent human review or proof-kernel verification is claimed.", + "open_questions": [ + { + "question": "Which actual remaining weight-seven beta profile survives dimension deletion together with the already published rank-six span and root-simplex bounds?", + "why_it_matters": "A named surviving caller is needed before another local geometric optimization; this result does not justify a larger census.", + "first_step": "Refresh Discussion3156 and exact PR heads, enumerate the historical (6,4) profiles and attach existing sufficient rules before selecting one target.", + "blocked_by": "The historical filter ledger is not a current scientific disposition ledger; pending source archives and the rest of C5 remain unreviewed dependencies." + } + ] +} diff --git a/research/p112-weight-seven-deletion/VERIFY.json b/research/p112-weight-seven-deletion/VERIFY.json new file mode 100644 index 0000000000..dd45529d1e --- /dev/null +++ b/research/p112-weight-seven-deletion/VERIFY.json @@ -0,0 +1,29 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/one-sided-six-multisets/data/data.txt" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact retained-source and live-data binding; complete five/six-flat capacities; chamber and root-plane premises; A5 fixture, endpoint patterns, historical profile and dimension/support invoice." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Fifteen behavioral groups, sharp dimension-loss and quotient fixtures, invalid support/cutoff controls, separate prior-cover oracle, unmodified predecessor count, source mutations and external-output safety." + } + ] +} diff --git a/research/p112-weight-seven-deletion/geometry.py b/research/p112-weight-seven-deletion/geometry.py new file mode 100644 index 0000000000..222ea556fa --- /dev/null +++ b/research/p112-weight-seven-deletion/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 in (5, 6), "only five/six-flat capacities are supported") + 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 = {5: (3309747, 12), 6: (788035, 20)}[dimension] + 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-weight-seven-deletion/obstruction.py b/research/p112-weight-seven-deletion/obstruction.py new file mode 100644 index 0000000000..175cad80d6 --- /dev/null +++ b/research/p112-weight-seven-deletion/obstruction.py @@ -0,0 +1,126 @@ +"""Delete one unrestricted piece before applying the P112 A5 coordinate bound. + +The inequality is Nick Petalas/PR3169's. Historical necessary filters below +follow DreamingOfClouds/PR3154 TWOSIDE, not a new decoder reduction. +Apache-2.0. Exact source pins and retained text are in SOURCES.json. +""" + +from itertools import combinations, combinations_with_replacement, product + +from geometry import require + +CAP = {2: 2, 3: 4, 4: 8, 5: 12, 6: 20, 7: 36} +TARGET_CAP = {**CAP, 7: 32} +DISTANCE = (0, 53, 78, 92, 100, 106, 109) +TARGET = (4, 4, 4, 6, 6, 6, 6, 6, 6, 7) +RETAINED = TARGET[:-1] + + +def intersection_after_deletion(dimension, intersection, removed): + """A codimension-r restriction loses at most r intersection dimensions.""" + require(all(type(x) is int for x in (dimension, intersection, removed)) + and 0 <= intersection <= dimension <= 16 + and 0 <= removed <= dimension, "invalid dimension ledger") + return max(0, intersection - removed) + + +def coordinate_bound(small_cap, endpoint_caps): + """PR3169's bound, after independently certifying the support hypotheses.""" + require(type(small_cap) is int and 0 <= small_cap <= 112 + and len(endpoint_caps) == 6 + and all(type(x) is int and 0 <= x <= 112 for x in endpoint_caps), + "invalid support ledger") + ordered = sorted(endpoint_caps, reverse=True) + quotient_cap = small_cap + ordered[0] + edge_cap = small_cap + sum(ordered[:2]) + require(quotient_cap < 53, "quotient independence is uncertified") + require(edge_cap < 70, "root-edge classification is uncertified") + total = sum(endpoint_caps) + old_upper = 9 * small_cap + 5 * total + upper = 112 + 8 * small_cap + 4 * total + return {"small_support_cap": small_cap, "endpoint_sum_cap": total, + "quotient_support_cap": quotient_cap, "edge_support_cap": edge_cap, + "edge_incidence_lower": 795, "old_incidence_upper": old_upper, + "coordinate_incidence_upper": upper, "old_margin": 795 - old_upper, + "margin": 795 - upper, "excluded": 795 > upper} + + +def original_survivor(weights): + """Pinned BK/BK7 filters at b=6, t=4; finite historical inclusion only.""" + require(6 <= len(weights) <= 10 and tuple(sorted(weights)) == tuple(weights) + and all(type(w) is int and w in CAP for w in weights), + "invalid historical weight multiset") + if sum(w - 2 for w in weights) >= 36: + return False + for level in range(1, 7): + retained = weights[:len(weights) - (6 - level)] + global_cap = sum(CAP[w] for w in retained) + target_cap = sum(TARGET_CAP[w] for w in retained) + if level == 1 and target_cap < 53 and global_cap < 73: + return False + if level == 2 and target_cap < 78 and global_cap < 82: + return False + if level >= 3 and global_cap < DISTANCE[level]: + return False + basis = weights[:len(weights) - 6] + if sum(CAP[w] for w in basis) >= 53: + return True + if sum(basis) <= 7: + return False + for assignment in product((0, 1), repeat=len(basis)): + if all(sum(w for w, a in zip(basis, assignment, strict=True) if a == group) + <= 6 for group in (0, 1)): + return False + return True + + +def prior_cover_audit(): + """Check all 210 weight-certified quotient bases and their two-flat covers.""" + bases = {} + for indices in combinations(range(10), 4): + basis = tuple(TARGET[i] for i in indices) + if basis in bases or sum(CAP[w] for w in basis) >= 53: + continue + complement = tuple(w for i, w in enumerate(TARGET) if i not in indices) + minimum = sum(CAP[w] for w in basis) + for assignment in product(range(3), repeat=4): + if any(sum(w for w, a in zip(basis, assignment, strict=True) if a == k) + > 6 for k in (0, 1)): + continue + cuts = sum(CAP[w] for w, a in zip(basis, assignment, strict=True) if a == 2) + minimum = min(minimum, cuts) + bases[basis] = {"basis": list(basis), "complement": list(complement), + "support_cap": sum(CAP[w] for w in basis), + "minimum_two_flat_cuts": minimum, + "rank_four_anchor": any(w <= 4 for w in complement)} + rows = [bases[basis] for basis in sorted(bases)] + require(len(rows) == 1 + and all(row["minimum_two_flat_cuts"] == 16 + and not row["rank_four_anchor"] for row in rows), + "prior weight-cover audit") + return rows + + +def application(): + survivors = [] + examined = 0 + for size in range(6, 11): + for weights in combinations_with_replacement(range(2, 8), size): + examined += 1 + if original_survivor(weights): + survivors.append(weights) + require(len(survivors) == 69 and TARGET in survivors, "historical inclusion") + retained_intersection = intersection_after_deletion(10, 6, 1) + require(retained_intersection == 5 and len(RETAINED) == 9, + "nine-piece intersection hypothesis") + bound = coordinate_bound(3 * CAP[4], [CAP[6]] * 6) + require(bound["excluded"] and bound["margin"] == 11 + and bound["old_margin"] == -21, "coordinate-bound gain") + return {"historical_cell": [6, 4], "multisets_examined": examined, + "historical_survivors": [list(w) for w in survivors], + "target": list(TARGET), "retained_weights": list(RETAINED), + "original_intersection_lower": 6, "removed_pieces": 1, + "retained_intersection_lower": retained_intersection, + "retained_quotient_dimension": 4, "new_profile_exclusions": 1, + "concurrent_PR3195_profile_counted_as_new": False, + "prior_cover_audit": prior_cover_audit(), **bound} diff --git a/research/p112-weight-seven-deletion/test_verify.py b/research/p112-weight-seven-deletion/test_verify.py new file mode 100644 index 0000000000..e079d30024 --- /dev/null +++ b/research/p112-weight-seven-deletion/test_verify.py @@ -0,0 +1,194 @@ +"""Behavioral, source-binding and losing-bound controls for the obstruction.""" + +import hashlib +import json +import shutil +import subprocess +import sys +import tempfile +import unittest +from fractions import Fraction +from itertools import combinations, product +from pathlib import Path +from unittest.mock import patch + +import verify +from geometry import root_data +from obstruction import (RETAINED, TARGET, application, coordinate_bound, + intersection_after_deletion, original_survivor, + prior_cover_audit) + + +class ObstructionTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.roots, cls.points, cls.labels, _ = root_data() + + def test_actual_profile_and_dimension_ledger(self): + result = application() + self.assertEqual(result["target"], list(TARGET)) + self.assertEqual(result["retained_weights"], list(RETAINED)) + self.assertEqual(result["retained_intersection_lower"], 5) + self.assertEqual(result["retained_quotient_dimension"], 4) + self.assertEqual(result["new_profile_exclusions"], 1) + self.assertEqual(result["margin"], 11) + + def test_intersection_loss_is_sharp_not_free(self): + # Coordinate subspaces give literal sharp cases for every dimension. + for dimension in range(1, 10): + for code_dimension in range(dimension + 1): + for removed in range(dimension + 1): + retained = set(range(removed, dimension)) + code = set(range(code_dimension)) + actual = len(retained & code) + self.assertEqual(actual, intersection_after_deletion( + dimension, code_dimension, removed)) + self.assertEqual(intersection_after_deletion(9, 6, 2), 4) + self.assertNotEqual(intersection_after_deletion(9, 6, 1), 6) + + def test_invalid_dimension_inputs(self): + for values in ((9, 10, 1), (9, 6, -1), (9, 6, 10), + (17, 6, 1), (9, True, 1), (9, 6, 1.0)): + with self.subTest(values=values), self.assertRaises(ValueError): + intersection_after_deletion(*values) + + def test_quotient_normalization_on_exact_linear_fixture(self): + # This is a linear-algebra fixture, not an impossible P112 realization. + images = [(1, 0, 0, 0), (0, 1, 0, 0), (0, 0, 1, 0)] + images += [(i, i * i, i ** 3, i + 1) for i in range(6)] + circuits = [] + for i in range(1, 6): + row = [Fraction(0)] * 9 + row[i + 3], row[3] = Fraction(1, i + 1), -1 + row[0], row[1] = -Fraction(i, i + 1), -Fraction(i * i, i + 1) + row[2] = -Fraction(i ** 3, i + 1) + image = tuple(sum(row[j] * images[j][k] for j in range(9)) + for k in range(4)) + self.assertEqual(image, (0, 0, 0, 0)) + circuits.append(row) + # A diagonal five-by-five minor certifies all five circuits independent. + for i, row in enumerate(circuits): + for j in range(5): + self.assertEqual(row[j + 4], Fraction(1, i + 2) if i == j else 0) + + def test_new_bound_and_losing_old_bound(self): + row = coordinate_bound(24, [20] * 6) + self.assertEqual(row["quotient_support_cap"], 44) + self.assertEqual(row["edge_support_cap"], 64) + self.assertEqual(row["coordinate_incidence_upper"], 784) + self.assertEqual(row["old_incidence_upper"], 816) + self.assertEqual(row["old_margin"], -21) + + def test_support_boundary_must_not_be_excluded(self): + self.assertEqual(coordinate_bound(25, [20] * 6)["margin"], 3) + row = coordinate_bound(26, [20] * 6) + self.assertEqual(row["margin"], -5) + self.assertFalse(row["excluded"]) + + def test_quotient_and_root_cutoffs_are_strict(self): + for small, caps in ((33, [20] * 6), (30, [20] * 6), + (24, [36] + [20] * 5)): + with self.subTest(small=small, caps=caps), self.assertRaises(ValueError): + coordinate_bound(small, caps) + + def test_invalid_support_inputs(self): + for small, caps in ((-1, [20] * 6), (True, [20] * 6), + (24, [20] * 5), (24, [20] * 5 + [-1]), + (24, [20] * 5 + [20.0])): + with self.subTest(small=small, caps=caps), self.assertRaises(ValueError): + coordinate_bound(small, caps) + + def test_original_profile_is_a_strict_budget_survivor(self): + self.assertTrue(original_survivor(TARGET)) + self.assertEqual(sum(w - 2 for w in TARGET), 35) + self.assertFalse(original_survivor((6,) * 9)) # excess 36 is not strict + for weights in (TARGET[::-1], TARGET[:-1] + (8,), (2,) * 11): + with self.assertRaises(ValueError): + original_survivor(weights) + + def test_unmodified_predecessor_count(self): + result = subprocess.run( + [sys.executable, "-B", str(verify.PACKAGE / "vendor/bk2b.py")], + check=True, capture_output=True, text=True, timeout=30) + rows = [tuple(map(int, line.split())) for line in result.stdout.splitlines()] + self.assertEqual(len(rows), 24) + self.assertEqual([row for row in rows if row[:2] == (6, 4)], [(6, 4, 69, 1)]) + self.assertEqual(result.stderr, "") + + def test_all_prior_covers_with_a_separate_subset_oracle(self): + rows = prior_cover_audit() + self.assertEqual([row["basis"] for row in rows], [[4, 4, 4, 6]]) + cap = {4: 8, 6: 20} + for row in rows: + weights = row["basis"] + candidates = [] + for paid in product((False, True), repeat=len(weights)): + remaining = [w for w, cut in zip(weights, paid, strict=True) if not cut] + for left in product((False, True), repeat=len(remaining)): + left_sum = sum(w for w, side in + zip(remaining, left, strict=True) if side) + right_sum = sum(w for w, side in + zip(remaining, left, strict=True) if not side) + if left_sum <= 6 and right_sum <= 6: + candidates.append(sum(cap[w] for w, cut in + zip(weights, paid, strict=True) if cut)) + self.assertEqual(min(candidates), row["minimum_two_flat_cuts"]) + self.assertFalse(row["rank_four_anchor"]) + + def test_endpoint_patterns_and_literal_root_fixture(self): + self.assertEqual(verify.endpoint_controls()["value_assignments"], 7 ** 6) + fixture = verify.simplex_control(self.roots, self.points) + self.assertEqual(max(map(int, fixture["live_edge_histogram"])), 9) + self.assertEqual(sum(fixture["live_edge_histogram"].values()), 112) + # A six-value endpoint pattern can have fifteen unequal pairs. The + # nine-incidence assertion needs the root-simplex hypothesis. + self.assertEqual(sum(a != b for a, b in combinations(range(6), 2)), 15) + + def test_retained_source_mutation_is_rejected(self): + self.assertEqual(len(verify.bound_sources()), 4) + with tempfile.TemporaryDirectory() as directory: + package = Path(directory) + shutil.copyfile(verify.PACKAGE / "SOURCES.json", package / "SOURCES.json") + for name in verify.RETAINED_PATHS: + target = package / name + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(verify.PACKAGE / name, target) + with (package / "geometry.py").open("a", encoding="utf-8") as stream: + stream.write("\n# mutation\n") + with patch.object(verify, "PACKAGE", package), self.assertRaisesRegex( + ValueError, "changed retained source"): + verify.bound_sources() + + def test_input_bytes_and_semantic_binding_are_both_checked(self): + source = verify.ROOT / verify.DATA + self.assertEqual(len(verify.bind_data(source, self.points, self.labels)), 64) + with tempfile.TemporaryDirectory() as directory: + package = Path(directory) + raw = source.read_bytes() + b"\n" + changed = package / "changed.txt" + changed.write_bytes(raw) + with self.assertRaisesRegex(ValueError, "changed P112 input"): + verify.bind_data(changed, self.points, self.labels) + pins = json.loads((verify.PACKAGE / "SOURCES.json").read_text()) + for row in pins["files"]: + if row["usage"] == "input": + row["sha256"] = hashlib.sha256(raw).hexdigest() + (package / "SOURCES.json").write_text(json.dumps(pins)) + wrong_labels = (0,) + self.labels[1:] + with patch.object(verify, "PACKAGE", package), self.assertRaisesRegex( + ValueError, "P112 label binding"): + verify.bind_data(changed, self.points, wrong_labels) + + def test_receipt_outputs_are_external_and_exclusive(self): + with tempfile.TemporaryDirectory() as directory: + output = Path(directory) / "receipt.json" + verify.publish_receipt({"control": True}, output) + self.assertEqual(json.loads(output.read_text()), {"control": True}) + with self.assertRaises(FileExistsError): + verify.publish_receipt({}, output) + with self.assertRaisesRegex(ValueError, "outside checkout"): + verify.publish_receipt({}, verify.PACKAGE / "forbidden-output.json") + + +if __name__ == "__main__": + unittest.main() diff --git a/research/p112-weight-seven-deletion/vendor/COORDINATE-PROOF.md b/research/p112-weight-seven-deletion/vendor/COORDINATE-PROOF.md new file mode 100644 index 0000000000..278072bdaf --- /dev/null +++ b/research/p112-weight-seven-deletion/vendor/COORDINATE-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) = , 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 =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. diff --git a/research/p112-weight-seven-deletion/vendor/NOTICE.md b/research/p112-weight-seven-deletion/vendor/NOTICE.md new file mode 100644 index 0000000000..1d7d628f00 --- /dev/null +++ b/research/p112-weight-seven-deletion/vendor/NOTICE.md @@ -0,0 +1,18 @@ +# Retained source attribution + +`bk2b.py` and `TWOSIDE-NOTES.md` are unchanged copies of DreamingOfClouds's +PR3154 TWOSIDE sources at +`708f0ad8928c383de8294aea3c126e9461d2066d`. + +`COORDINATE-PROOF.md` and the package's `geometry.py` are unchanged copies +from Nick Petalas/PR3169 at +`2dbbd3004b70772cef200e341037c7c05b094fbc`. The coordinate inequality is +that predecessor's result. Its geometry follows PR3164 at +`857384079ab640a949fb7618b7909664d3e737e5` and PR3161/3162's retained +E8/P112 reconstruction. The new application does not claim that inequality +or the original decoder reduction as new work. + +The source lineage includes joaqcoo's E8/P112 model and the contributors +credited by the original packages. Their existing attribution remains in +the retained texts. Exact source paths, heads, Git blobs and SHA256 digests +are in `../SOURCES.json`. Repository Apache-2.0 terms apply; see `../../../LICENSE`. diff --git a/research/p112-weight-seven-deletion/vendor/TWOSIDE-NOTES.md b/research/p112-weight-seven-deletion/vendor/TWOSIDE-NOTES.md new file mode 100644 index 0000000000..e3fd3f2b1d --- /dev/null +++ b/research/p112-weight-seven-deletion/vendor/TWOSIDE-NOTES.md @@ -0,0 +1,65 @@ +# TWOSIDE — K1 two-sided residues R-b (b_Q>=5), R-dep, CONJ-G cost-64 residue (Oct 16) +Labels PROVEN / CHECKED (two implementations) / CHECKED-1 (single implementation) / OPEN. python = W/venv/bin/python. +## STATE +- TWOSIDE: read #3029 README, CONJ-G, R-B, SIX §1-3 (Lemma B, S66, Basis-kill), SMALL2 §4. +- TWOSIDE: bk1.py (impl 1): Basis-kill (Lemma B + S66) applied to all size/cap-feasible σ-multisets for b=5..8. Closes (5,1),(5,2) [ (b,1) already vacuous by WALL 8.3 b_Q<=1 ]. + +- TWOSIDE: F7 lemma CHECKED (f7.py/f7r.py, rank + explicit-cover impls agree). bk1b/bk2b (BK + F7) survivor counts agree in all 24 cells. R-dep reformulated exactly (§2, PROVEN). CONJ-G residue restated (§3). Card DONE at ~115k. + +## §1 R-b (b_Q >= 5): Basis-kill transfer (PROVEN mod S66, which is CHECKED twice in SIX) +**Lemma BK.** Let B be a basis of span q(Lo) (|B| = ρ + b, b = b_Q), all pieces low (w <= 7). If some ρ pieces X0 ⊆ B have +Σ_{X0} g(w) < 53 and their weights pack into two groups of total weight <= 6 (+ at most one 1-piece), then b <= 3. +*Proof.* |∪_{X0} A_k| < 53 = d_1, so span q(X0) ∩ 𝒞 = 0: X0 is λ-independent for λ: span q(B) → span q(B)/(span ∩ 𝒞) ≅ K^ρ, hence a λ-basis. +SIX Lemma B (valid for every d; it uses only that B is a basis) gives b independent h_y (y ∉ X0) with Off(h_y) ⊆ U_{X0} ∪ Λ(F_y), w_y <= 7, so +rank ℓ(Off(h_y) ∖ X) <= 7 with X = Λ(V_1) ∪ Λ(V_2) [∪ t] ⊇ U_{X0}. S66 / S66+t: such h span <= 3. ∎ +bk1.py table (impl 1; σ=0 pieces treated as weight 2, X0 = ρ smallest; level 1/2 caps (32,20,12) on |Off|<=72 / E6 targets, global otherwise): +| b \ t | 1 | 2 | 3 | 4 | 5 | 6 | (min-Σσ survivor deficit; #survivors) +| 5 | 0 | 0 | 2 (4) | 2 (15) | 3 (38) | 3 (77) | +| 6 | 1 (1) | 1 (2) | 4 | 4 | 5 | 5 | +| 7 | 2 | 2 | 6 | 6 | 7 | 7 | +| 8 | 3 | 3 | 8 | 8 | 10 | 10 | +These are single-implementation survivor lists, NOT bounds on anything beyond "BX can fail only on these multisets". +- TWOSIDE: bk2.py (impl 2, own caps/brute packing) agrees: (5,1),(5,2) no survivors; (5,3) same 4 survivors. (5,2) CHECKED. ~75k tokens used. + +**Lemma F7 (CHECKED, two implementations: f7r.py rank = Gaussian elimination; f7r.py cover = explicit 7-flat pair search).** For every +7-dim label space V (all 43435), the directions h with rank ℓ(Off(h) ∖ Λ(V)) <= 7 are at most 2, and they are frame directions. +Completeness: such h has Off(h) ⊆ Λ(V) ∪ Λ(G), G 7-dim; |Off| >= 73 is impossible (36+36), |Off| <= 72 gives |Off| <= 32+32 = 64 (C11), +so h is one of the 120 root/frame directions (SIX §3 list), all tested. Histogram: 0:41431, 1:1976, 2:28 (roots never qualify). +**Corollary BK7 (PROVEN mod F7).** If some ρ pieces X0 with Σ_{X0} g < 53 have Σ_{X0} w <= 7, then b <= 2 (Lemma B gives b independent h_y). +bk1b.py (impl 1) / bk2b.py (impl 2): BK + BK7. Survivor counts agree in all 24 cells (CHECKED; full lists cross-checked only at (5,3), bk2): +| b \ t | 1 | 2 | 3 | 4 | 5 | 6 | (max deficit of a survivor; #survivors) | +| 5 | closed | closed | 2 (4) | 2 (15) | 3 (38) | 3 (77) | +| 6 | closed | 1 (1: 5^7,0) | 4 (17) | 4 (69) | 5 (174) | 5 (364) | +| 7 | closed | 2 (2: 5^8,0/1) | 6 (37) | 6 (154) | 7 (403) | 7 (885) | +| 8 | closed | 3 (3: 5^9,0/1/2) | 8 (60) | 8 (251) | 10 (684) | 10 (1556) | +So **BX holds at (5,1),(5,2) and every (b,1)** (CHECKED; (b,1) also by WALL 8.3). +**Exact residue R-b (OPEN).** Every survivor has a λ-basis X0 = ρ smallest pieces with |U_X0| < 53 that fails both packings. The two shapes: +(α) t = 2, b >= 6: all pieces weight 7 plus one piece of weight <= 4 (X0 = {small, 7}). Needed lemma F7+P: for V 7-dim and a set P of <= 4 lines + (a weight-<=4 piece: <= 8 lines, P ⊆ a 4-flat), the h with rank ℓ(Off(h) ∖ (Λ(V) ∪ P)) <= 7 span <= 5. +(β) t >= 3: weight-6 majority, X0 = {6,6,small...} (e.g. (5,3): [6^7,2], [7,6^6,2], [6^7,3], [6^6,5,4]). Needed lemma S66+P: for V1,V2 6-dim and P a + common set of <= 2 (resp. <= 4) lines, the h with rank ℓ(Off(h) ∖ X) <= w_y (w_y = 6 for the weight-6 non-basis pieces) span <= b − 1. + Both are kill46-shaped finite computations (orbit reps of V1 + all V2 + P), not attempted here (S66 mode t took 7 min in C; +2 lines ~ x50). + +## §2 R-dep, exactly (PROVEN algebra) +cost_k = ρ(R_k,A_k) = rank of Ω on U_{R_k} × U_{A_k} = w(A_k) − dim(U_{A_k} ∩ Z_{R_k}) (rank of a bilinear pairing is symmetric), so +**ε^row_k = w(A_k) − cost_k** exactly. The R-dep condition "for every k0 ∈ J: Σ_{k≠k0} ε^row_k >= cost_k0 + 1" becomes +Σ_J ε − (w_k0 − cost_k0) >= cost_k0 + 1 ⇔ **Σ_{k∈J} ε^row_k >= w(A_k0) + 1 for all k0 ⇔ Σ_J ε^row_k >= max_J w(A_k) + 1.** +(The "every k0" quantifier collapses to the heaviest column.) With ε^row_k <= min(w(A_k), 9 − w(R_k)): +rows of weight 9 give 0, weight 8 give <= 1 (Z_R = , corrected iff z ∈ U_A), weight 7 <= 2. +s = 1 (J = J_P ⊆ Lo_Q): row-side WALL Lemma 8.2 (transposed; PROVEN there from kpr15 CHECKED cover facts) gives two cases: + (i) no row of weight <= 6: Σ ε <= 2 n_7 + n_8^corr with all weight-7 rows on one frame line ⇒ **#corrected rows >= ⌈(w_max+1)/2⌉**; + (ii) exactly one row k1 of weight r <= 6 (the only low row), the rest weight >= 8: **n_8^corr >= w_max + 1 − min(w_{k1}, 9 − r)**. +Exact residue (OPEN): a low column circuit J at tight m meeting (i) or (ii) together with the cost-63 budget (N2). Not closed: the +circuit structure of the columns (A_k0 ⊆ ∪_{k≠k0} A_k) carries no codeword, so the cover tables bite only on the row side (pair lemma). +For s >= 2 the transposed Lemma 8.2 is not available (rows of J_P are a coset of an s-dim outside space): residue stated only via the boxed condition. + +## §3 CONJ-G residue (exact restatement; not closed) +D′: one-sided, 8+t terms (t = 2,3), corrected cost 64, n_c >= 4 (>= 3 unconditionally), so raw/ε-free cost Σw = 64 + n_c >= 67. +(a) #2816 uniqueness (Theorem U) is about ε-free cost 64 (δ = 0); D′ has ε-free cost >= 67, outside its scope: it gives nothing. +(b) #3074 padding sends D′ to a one-sided P120 decoder of cost exactly 64 + 8 = 72 = the L120 floor (equality case). L120 is not + unique at 72: the padded k = 4 root-swap family (t = 4) also attains it. So padding + uniqueness cannot kill D′ unless the L120 + equality case is classified; that classification (for 16 + t <= 19 terms) is the exact open statement. +(c) Branch d = 0, x = 0, m_T = 0 and no D7-type weight-8 member (|supp T| <= 4 suffices; SIX §7(b)) (NOT forced by peeling here, since slack = n_c >= 3): Δ_D = n_c gives cost_w(T) + c_9 = n_c <= |R| + c_9', + so |R| >= cost_w(T); the (k,g) mechanism of CONJ-G (A)/(B) yields a further swap line v ∉ R, so |R ∪ {v}| > cost_w(T), contradicting the + Swap Conjecture (SIX §7: #swap lines <= cost_w(T); PROVEN for κ <= 3, dim T = 1, or A nonsingular). This only re-derives CONJ-G's remark. + Open branches, exactly: m_T >= 1 (carriers in T), x >= 1, a D7-type weight-8 member, or d >= 1 with cost(T) − 8d + 8x + c_8 <= n_c (DP: d <= 5 ⇒ cost(T) − 8d >= 2). diff --git a/research/p112-weight-seven-deletion/vendor/bk2b.py b/research/p112-weight-seven-deletion/vendor/bk2b.py new file mode 100644 index 0000000000..3394029014 --- /dev/null +++ b/research/p112-weight-seven-deletion/vendor/bk2b.py @@ -0,0 +1,29 @@ +# TWOSIDE bk2: independent re-implementation of bk1 on cells (5,1),(5,2) (and prints (5,3) survivors for comparison). +# Works with weights w in {2..7} directly; own cap tables; brute-force packing over all bin assignments. +from itertools import product, combinations_with_replacement as cwr +CAPG={2:2,3:4,4:8,5:12,6:20,7:36}; CAPT={2:2,3:4,4:8,5:12,6:20,7:32} +DH=[None,53,78,92,100,106,109,111,112] +def feasible(W,b): + W=sorted(W) # ascending + for lev in range(1,b+1): # keep the len-(b-lev) smallest... i.e. drop the b-lev largest + X=W[:len(W)-(b-lev)] + sg=sum(CAPG[w] for w in X); st=sum(CAPT[w] for w in X) + if lev==1 and not (st>=53 or sg>=73): return False + if lev==2 and not (st>=78 or sg>=82): return False + if lev>=3 and sg=53: return False + if sum(X)<=7: return True + for asg in product((0,1),repeat=rho): + if all(sum(w for w,a in zip(X,asg) if a==k)<=6 for k in (0,1)): return True + return False +import sys +for b in range(5,9): + for t in range(1,7): + S=[] + for n in range(b,b+t+1): + for W in cwr(range(2,8),n): + if sum(w-2 for w in W)<6*b and feasible(W,b) and not killed(W,b): S.append(tuple(sorted((w-2 for w in W),reverse=True))) + print(b,t,len(S),min((6*b-sum(x) for x in S),default=0),flush=True) diff --git a/research/p112-weight-seven-deletion/verify.py b/research/p112-weight-seven-deletion/verify.py new file mode 100644 index 0000000000..57eae72ceb --- /dev/null +++ b/research/p112-weight-seven-deletion/verify.py @@ -0,0 +1,127 @@ +#!/usr/bin/env python3 +"""Replay the P112 nine-piece obstruction and its weight-seven application.""" + +import argparse +import hashlib +import json +from collections import Counter +from itertools import combinations +from pathlib import Path + +from geometry import (canonical, chamber_receipt, dot, flat_capacity, require, + root_data, root_plane_receipt) +from obstruction import application, coordinate_bound + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +DATA = "research/one-sided-six-multisets/data/data.txt" +RETAINED_PATHS = ("geometry.py", "vendor/COORDINATE-PROOF.md", "vendor/bk2b.py", + "vendor/TWOSIDE-NOTES.md") + + +def bound_sources(): + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + rows = sources["retained_sources"] + require(tuple(row["local_path"] for row in rows) == RETAINED_PATHS, + "retained-source inventory") + for row in rows: + path = PACKAGE / row["local_path"] + require(path.is_file() and not path.is_symlink() + and path.stat().st_size <= 100_000, "missing/large retained source") + digest = hashlib.sha256(path.read_bytes()).hexdigest() + require(digest == row["sha256"], "changed retained source") + return {row["local_path"]: row["sha256"] for row in rows} + + +def bind_data(path, points, labels): + require(path.is_file() and not path.is_symlink() + and path.stat().st_size <= 2_000_000, "missing/large P112 input") + raw = path.read_bytes() + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + pins = [row for row in sources["files"] if row["usage"] == "input"] + require(len(pins) == 1 and pins[0]["path"] == DATA, "live-input inventory") + digest = hashlib.sha256(raw).hexdigest() + require(digest == pins[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, "P112 label binding") + require(tuple(tuple(map(int, row.split())) for row in rows[2:114]) == points, + "P112 root binding") + return digest + + +def simplex_control(roots, points): + """A literal A5 fixture, not an enumeration of every root simplex.""" + 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(edge in roots for edge in edges), + "A5 fixture edges") + histogram = Counter() + 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(histogram) == 9, "nine-edge sharpness") + return {"vertices": vertices, + "live_edge_histogram": {str(k): v for k, v in sorted(histogram.items())}} + + +def endpoint_controls(): + """Exhaust every equality pattern on six endpoints, with zero distinguished.""" + from itertools import product + + histogram = Counter() + for values in product(range(7), repeat=6): + nonzero = sum(value != 0 for value in values) + unequal = sum(a != b for a, b in combinations(values, 2)) + require(unequal <= 4 * nonzero + 1, "coordinate inequality") + histogram[nonzero] += 1 + boundary = coordinate_bound(26, [20] * 6) + require(not boundary["excluded"] and boundary["margin"] == -5, + "losing support boundary") + return {"value_assignments": sum(histogram.values()), + "nonzero_histogram": {str(k): v for k, v in sorted(histogram.items())}, + "losing_small_support_26": boundary} + + +def receipt(): + retained = bound_sources() + roots, points, labels, coordinates = root_data() + return {"schema": "p112-weight-seven-deletion/v1", "retained_sources": retained, + "input_sha256": bind_data(ROOT / DATA, points, labels), + "chamber": chamber_receipt(roots, points, coordinates), + "root_planes": root_plane_receipt(roots), + "flat_capacities": [flat_capacity(labels, d) for d in (5, 6)], + "simplex_control": simplex_control(roots, points), + "endpoint_controls": endpoint_controls(), "application": application()} + + +def publish_receipt(result, output): + serialized = json.dumps(result, indent=2) + "\n" + if output is None: + expected = json.loads((PACKAGE / "RESULT.json").read_text(encoding="utf-8")) + require(json.loads(serialized) == expected, "committed receipt differs") + return + output = 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(serialized) + + +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() + publish_receipt(result, args.output) + flats = sum(row["subspaces"] for row in result["flat_capacities"]) + print("PASS_P112_WEIGHT_SEVEN_DELETION new_profiles=1 margin=11 " + f"flats={flats} errors=0") + + +if __name__ == "__main__": + main()