diff --git a/research/p112-larger-root-simplices/CHECKS.json b/research/p112-larger-root-simplices/CHECKS.json new file mode 100644 index 0000000000..7f366a9757 --- /dev/null +++ b/research/p112-larger-root-simplices/CHECKS.json @@ -0,0 +1,67 @@ +{ + "status": "local checks passed", + "baseline_main": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "priority_revision": 6, + "environment": { + "python": "3.12.15", + "second_python": "3.13.5", + "platform": "Linux 6.6.87.2, WSL2, x86_64, glibc 2.41", + "dependencies": "Python standard library only" + }, + "executed": [ + {"command": "python3 -B scripts/research_baseline.py", "result": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY; not a selected cold replay"}, + {"command": "python3.12 -W error -B research/p112-larger-root-simplices/verify.py --output SESSION/RESULT.json", "result": "PASS_LARGER_ROOT_SIMPLICES; exact margins 9,4,12; all 4,097,782 flat kernels, 7,140 root planes, 960 reflections and original 24-cell table recomputed"}, + {"command": "python3.13 -O -W error -B research/p112-larger-root-simplices/verify.py", "result": "PASS; exact committed-receipt equality on a second interpreter"}, + {"command": "python3.12 -O -W error -B research/p112-larger-root-simplices/test_verify.py", "result": "PASS; 15 behavioral groups, including losing support budgets, strict geometric cutoffs, source/input/receipt mutants and rational fixture ranks"}, + {"command": "python3.12 -B scripts/research_package.py --package research/p112-larger-root-simplices --check-only", "result": "PASS_PACKAGE_METADATA_AND_PINS"}, + {"command": "TMPDIR=SESSION python3.12 -B scripts/research_package.py --package research/p112-larger-root-simplices", "result": "PASS_REGISTERED_RESEARCH_PACKAGE outcome=completed; both commands run sequentially"}, + {"command": "TMPDIR=SESSION python3.13 -O -W error -B SESSION/source-export/research/p112-larger-root-simplices/verify.py", "result": "PASS; read-only Git-free source export with only this package and its declared data input"}, + {"command": "ruff check --no-cache research/p112-larger-root-simplices/{simplex,verify,test_verify}.py research/p112-larger-root-simplices/vendor/__init__.py", "result": "All checks passed; immutable predecessor sources are not reformatted"}, + {"command": "PYTHONPYCACHEPREFIX=SESSION/bytecode python3.12 -W error -m compileall -q research/p112-larger-root-simplices", "result": "PASS; compiled output kept outside the checkout"}, + {"command": "Compare retained source bytes with git show SOURCE_HEAD:SOURCE_PATH", "result": "All six retained original files match their stated Git objects exactly"} + ], + "mathematical_review": { + "method": "Local proof review separate from executable inspection; no independent reviewer is claimed", + "checked": ["quotient dimension and nonzero normalization", "characteristic-zero rational-kernel argument", "A2 coefficient signs and common root scale", "both incidence cases for seven through nine vertices", "outside endpoint charging", "actual original weight-filter membership", "four-piece cover and rank-four-anchor overlap limits"], + "result": "No unresolved local objection; all exact controls pass" + }, + "engineering": { + "principles": { + "Build the lever": "The retained deterministic checker reconstructs geometric quantities and the three named applications.", + "Prove it works": "Full mathematical replay, negative controls, a second interpreter and a read-only Git-free export check the actual package.", + "Power of Ten": "New code has no recursion, bounded domains, narrow state, checked source and subprocess boundaries, explicit exceptions and warning-clean validation." + }, + "bounds": [ + "New incidence/fixture loops have at most nine vertices, 36 edges and 120 root lines; exact fixture elimination uses eight columns.", + "The three production survivor cells enumerate at most 5*C(17,5)=30,940 raw rows per cell; the public helper's larger supported t<=6 domain is bounded by 7*C(19,5)=81,396 raw rows.", + "Basis packing has at most 2^6 assignments. The cover audit has at most C(12,4)=495 indexed bases and 3^4=81 assignments per distinct weight multiset.", + "The original source program has fixed b=5..8, t=1..6 and a 120-second subprocess timeout; output is exactly 24 short integer rows.", + "Input files are capped at 2,000,000 bytes. Source inventory has at most ten entries. All new functions are below 60 physical lines." + ], + "deviations": [ + {"rule": "3: fixed memory allocation", "location": "new Python checker and immutable geometry module", "reason": "Managed Python arithmetic and iteration allocate at runtime.", "scope": "Finite proof replay only", "compensating_control": "Fixed 112-label/120-root domains; flat census streams one kernel at a time; supported weight bounds and file-size limits bound live state.", "verification": "Complete normal/optimized replays, fixture and invalid-input tests pass.", "follow_up": "Use fixed arrays only if this proof replay is moved to a constrained runtime."}, + {"rule": "9: indirect calls", "location": "test_verify.py unittest discovery", "reason": "The standard unittest framework dispatches named tests.", "scope": "Fifteen local behavioral tests only", "compensating_control": "One fixed Controls class and explicit unittest.main entry point.", "verification": "The optimized test run reports all fifteen tests.", "follow_up": "Retain framework dispatch unless the test framework changes."}, + {"rule": "10: immutable-source diagnostics", "location": "vendor/bk2b.py and vendor/geometry.py", "reason": "These are authenticated frozen scientific source bytes; restyling them would break provenance.", "scope": "Unchanged retained originals only", "compensating_control": "SHA256/Git-blob equality, warnings-as-errors compilation and complete source-bound execution; new code passes Ruff.", "verification": "Full replay and origin-byte comparison pass.", "follow_up": "Any source cleanup belongs in a separately pinned successor, never this frozen copy."} + ] + }, + "upstream_checkpoint": { + "checked_at": "2026-10-17T14:12:25Z", + "main": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "priority_revision": 6, + "guidance_changed": false, + "open_pr_snapshot": "2026-10-17T14:11:57.624241+00:00", + "discussion_snapshot": "2026-10-17T14:12:25.361600+00:00", + "complete_pagination": true, + "warnings": [], + "subsequent_live_check": "PR3169 at b859f7791a6d2dad68652d5a54e266cb020a1302 has distinct (5,5) scope; body read, not cold-replayed." + }, + "limits": [ + "The standard Weyl-chamber theorem is used, not formally proved.", + "One literal simplex per size does not prove the universal incidence bound; the written argument does.", + "No independent human/proof-kernel review or hosted CI result is claimed.", + "No complete C5 cell, C(P112)>=64, native/outer replay, supplier admission or new kappa is claimed.", + "The generic selected-frontier cold replay was not run because no selected construction or input was changed.", + "The cover audit excludes only weight-certified predecessor applications, not all possible geometric covers.", + "Generic Git provenance pins resolve only at main. Pending source heads are authenticated through the retained-file byte inventory and the separately executed origin comparison, avoiding dependence on unmerged Git objects in hosted CI." + ] +} diff --git a/research/p112-larger-root-simplices/PROOF.md b/research/p112-larger-root-simplices/PROOF.md new file mode 100644 index 0000000000..4dc3350756 --- /dev/null +++ b/research/p112-larger-root-simplices/PROOF.md @@ -0,0 +1,168 @@ +# Three larger-simplex exclusions + +## Proposition + +Let `K` be a characteristic-zero field. Let `r_t` and `ell(t)` be the pinned +P112 root representatives and binary labels. On its 112 coordinates put + +``` +C = {c_h : c_h(t) = , h in K^8}, +w(q) = rank_F2 {ell(t) : q(t) != 0}. +``` + +For each `b in {6,7,8}`, there do not exist `b+4` independent pieces spanning +`T` such that `dim(T intersect C) >= b` and their weights are bounded by + +``` +2,5,5,5, followed by b copies of 6. +``` + +Thus the proposition excludes the named `2,5^3,6^b` weight shape in each +pinned TWOSIDE cell `(b,t)=(6,4),(7,4),(8,4)`. It is a theorem about these +piece configurations, not the whole C5 conjecture or a decoder lower bound. + +## Replayed geometric premises + +The unchanged geometry implementation from PR3164 reconstructs the 120 E8 +root lines, removes the eight frame lines and reconstructs all 112 labels. +The data match the exact main-branch input. The labels have a leading one, +so `g(2)<=2`, where `g(d)` is the maximum number of live labels in a +`d`-dimensional binary linear space. Complete unique reverse-echelon +annihilator enumeration gives `g(5)=12` and `g(6)=20`. It covers 3,309,747 +five-flats and 788,035 six-flats. Every lower-dimensional support can be +extended to a flat of the stated dimension. + +Every nonzero codeword in `C` has support at least 53. Every codeword with +support below 70 is proportional to a root codeword. For completeness, the +argument behind the retained finite quantities is as follows. Below 70 +means at least 43 perpendicular live root lines. Move a real direction into +a closed Weyl chamber. The perpendicular roots are generated by vanishing +simple nodes. Every six-node subsystem has at most 36 root lines. The eight +seven-node subsystems have `42,28,22,14,16,23,37,63` root lines. Only the last +can contain 43; its normal is a root direction. Root directions have live +supports 53 or 56, which also proves the distance 53. The replay checks all +960 simple reflections, simple-system positivity and these subsystem counts. +The standard finite-root-system Weyl-chamber theorem is used, not proved by +the executable. + +The statement extends to `K`. The rational roots perpendicular to a nonzero +field-valued direction have rational rank at most seven. If the rank were +at most six, a generic real normal to their span would contradict the +36-line bound. Hence a direction with at least 43 perpendicular roots is in +a one-dimensional rational kernel, and is proportional over `K` to a real +rational direction. Apply the real argument. The replay also checks that +the P112 root matrix has full rank eight, making `h -> c_h` injective. + +## A quotient with seven through nine vertices + +Choose three small pieces of weights `2,5,5`, and let `S` be the union of +their supports. Write the other pieces as `q_0,...,q_b`, with weights +`5,6,...,6`. Let `D=T intersect C` and `lambda:T -> T/D`. Then + +``` +|S| <= 2+12+12 = 26, +dim(T/D) <= (b+4)-b = 4. +``` + +The small pieces together with any one `q_i` have support at most +`26+20=46<53`. Their quotient images must be independent. Otherwise a +nonzero combination of four independent pieces would be a nonzero +codeword supported on fewer than 53 coordinates. Consequently the quotient +has dimension exactly four, the three small images are independent and +every `q_i` has nonzero image after quotienting by their span. + +This last quotient is one-dimensional. Rescale the `q_i` so that they have +the same nonzero image. Supports and piece independence are unchanged. +There are unique small-piece combinations `a_i` for which + +``` +c_0=0, +c_i=q_i-q_0-a_i belongs to D, i=1,...,b. +``` + +The `b` codewords `c_i` are independent, since their coefficients on the +independent pieces `q_1,...,q_b` are distinct unit vectors. Each nonzero edge +`c_i-c_j` is supported on `S union supp(q_i) union supp(q_j)`, hence has +support at most `26+20+20=66<70`. All edges are root directions. +Injectivity supplies `b` independent directions `h_i` with `c_i=c_{h_i}`. + +## The larger root-simplex incidence lemma + +Normalize roots to squared norm two. In the plane of two independent E8 +roots, any third root line is an A2 sum or difference, with coefficients of +absolute value one. All 7,140 root-plane checks are replayed exactly. This +fact holds over `K` too: a rational root in the `K`-span of two rational +roots is already in their rational span, by solving a nonsingular rational +coordinate minor. + +Write `h_i=z_i alpha_i` for roots `alpha_i`. Every `h_i-h_j` is a third +root line, so `z_i/z_j` is `+1` or `-1`. Absorb signs into the roots. There +is a common nonzero `z` such that `h_i=z alpha_i`; moreover +`=1` for distinct indices. Thus +`0,alpha_1,...,alpha_b` is a root A_b simplex with `n=b+1` vertices. + +For any E8 root `r`, its evaluations on these vertices are integers and all +pair differences lie in `{-2,-1,0,1,2}`. If a difference has absolute value +two, equality in Cauchy-Schwarz makes `r` that edge root. The evaluation +multiplicities are then `1,1,n-2`, so there are `2n-3` unequal pairs. If no +difference has absolute value two, there are at most two consecutive integer +levels, giving at most `floor(n^2/4)` unequal pairs. Therefore each live +coordinate occurs in at most + +``` +M_n = max(2n-3, floor(n^2/4)) +``` + +edge supports. For `n=7,8,9`, these bounds are `12,16,20`. They are universal +upper bounds; sharpness in E8 is not asserted for every size. In particular, +the literal nine-vertex fixture has maximum 18, not 20. Multiplication by +the common field scalar `z` does not change which evaluations vanish. + +## Incidence contradiction + +There are `E=n(n-1)/2` edges, each with at least 53 support coordinates. +At most `M_n |S|` edge incidences occur in `S`. Outside `S` each edge is +exactly `q_i(t)-q_j(t)`. Every unequal pair has a nonzero endpoint, and one +nonzero endpoint can meet only `n-1=b` pairs. Set +`U=sum_i |supp(q_i)| <= 12+20b`. It follows that + +``` +E*53 - M_n*|S| <= outside edge incidences <= b*U. +``` + +Substituting upper bounds only weakens the contradiction: + +| b | n | E | M_n | S cap | U cap | Required inequality | Margin | +|---|---|---|---|---|---|---|---| +| 6 | 7 | 21 | 12 | 26 | 132 | 801 <= 792 | 9 | +| 7 | 8 | 28 | 16 | 26 | 152 | 1068 <= 1064 | 4 | +| 8 | 9 | 36 | 20 | 26 | 172 | 1388 <= 1376 | 12 | + +All three are impossible. Smaller supports or overlaps strengthen the bound. +Increasing the allowed small-support union by just one removes each of these +contradictions; the checker retains this failure control. + +## Actual residue and overlap boundary + +The unchanged original `bk2b.py` reproduces all 24 pinned survivor counts. +A separate implementation reproduces the three relevant counts +`69,154,251`, and retains each target shape. The original filters are source +context, not new universal proof obligations established by this computation. + +There are exactly two four-piece weight multisets whose support capacities +are below 53 in each target: `(2,5,5,5)` and `(2,5,5,6)`. Exhaustively assigning +each to two groups of total weight at most six, with the rest paid as line +deletions, gives minimum deletion budget fourteen. The nonbasis pieces have +weight at least five, so this weight-certified calculation cannot invoke +PR3167's rank-four anchor. Consequently the earlier eight-/ten-deletion and +twelve-deletion/rank-four-anchor theorems do not themselves certify these +shapes by this weight-only cover route. This is not a claim that all other +possible proofs or geometric covers were excluded. + +Concurrent PR3169's five `(5,5)` exclusions and stronger six-vertex +coordinate budget are outside this scope; its proof was not cold-replayed +here. The six-vertex +PR3164 inequality is a positive control, not another new result. No complete +C5, `C(P112)>=64`, supplier, native/outer implementation or kappa improvement +follows from these three exclusions. Independent human and proof-kernel +review remain separate from this author-checked proof and exact replay. diff --git a/research/p112-larger-root-simplices/README.md b/research/p112-larger-root-simplices/README.md new file mode 100644 index 0000000000..caed5757fd --- /dev/null +++ b/research/p112-larger-root-simplices/README.md @@ -0,0 +1,87 @@ +# Larger root simplices exclude three P112 weight shapes + +For `b=6,7,8`, independent P112 pieces of weights bounded by `2,5^3,6^b` +cannot have code-intersection dimension at least `b`. This excludes one +named shape in each pinned TWOSIDE cell `(6,4),(7,4),(8,4)`. + +The proof extends PR3164's six-vertex root-simplex argument to seven, eight +and nine vertices. Each coordinate meets at most `12,16,20` edge supports. +The three incidence contradictions have exact margins **9, 4 and 12**. +The original source's relevant survivor counts are `69,154,251`; this package +does not claim to close those entire cells. + +[PROOF.md](PROOF.md) gives the characteristic-zero argument and its exact +hypotheses. [RESULT.json](RESULT.json) contains the replayed geometric +quantities, three literal simplex controls, original 24-cell survivor table, +three exclusion receipts and overlap audit. This is author-checked evidence, +not independent human or proof-kernel review. No full C5, `C(P112)>=64`, +decoder, supplier admission or new kappa is established. Selected frontier +files are unchanged. + +## Reproduce + +From the repository root, with Python 3.12+ and no third-party dependencies: + +```sh +python3.12 -B scripts/research_package.py --package research/p112-larger-root-simplices --check-only +python3.12 -B scripts/research_package.py --package research/p112-larger-root-simplices +``` + +The registered replay enumerates all 4,097,782 five-/six-flat kernels, checks +7,140 root planes and 960 simple reflections, reruns the original survivor +program and runs fifteen behavioral groups. It compares exact proof-relevant +JSON fields rather than timing or compressed-container bytes. Set `TMPDIR` +to an external session directory if your workspace policy requires it. +A direct replay writes nothing in the checkout: + +```sh +python3.12 -W error -B research/p112-larger-root-simplices/verify.py +python3.12 -O -W error -B research/p112-larger-root-simplices/test_verify.py +``` + +`verify.py --output /NEW/EXTERNAL/RESULT.json` creates a fresh receipt and +refuses an existing path or an output inside the checkout. A Git-free export +needs only this package and its one declared data input. [CHECKS.json](CHECKS.json) +records the environment, checks and verification limits. + +## Scope and source credit + +Nick Petalas. Apache-2.0. The original reduction, TWOSIDE piece hypotheses, +weight filters and survivor program are DreamingOfClouds's PR3154 at +`708f0ad8928c383de8294aea3c126e9461d2066d`, with the retained E8/P112 decoder +lineage. The root-simplex predecessor is Nick Petalas's PR3164 at +`857384079ab640a949fb7618b7909664d3e737e5`. Its geometry implementation and +proof are copied unchanged into `vendor/`; the new work is the larger-simplex +lemma, these three applications and their checks. The original notice and +license are retained. [SOURCES.json](SOURCES.json) pins every retained file by +source commit, Git blob and SHA256. Source equality is checked at replay; +origin-byte equality was separately checked against those Git objects. +Pending-PR Git history is not required for replay. The generic metadata pins +resolve only at main; the vendored originals have their own explicit byte +inventory, checked by `verify.py`. + +PR3167 at `c2c7508f2d731feea550f1628601aebd35c6e147` is an overlap control, +not a new dependency of the theorem. Every weight-certified four-piece +quotient cover here needs at least fourteen separate deletions, with no +nonbasis rank-four anchor. Thus the earlier eight-/ten-deletion and +rank-four/twelve-deletion bounds do not supply these exclusions by that +weight-only route. Other geometric covers or proofs are not ruled out. +Concurrent [PR3169](https://github.com/CrocSwap/integer-mult-bounds/pull/3169) +at `b859f7791a6d2dad68652d5a54e266cb020a1302` reports five ten-piece +`(5,5)` exclusions using a stronger six-vertex coordinate budget. Its PR +was read at submission, not cold-replayed. Its scope is distinct from these +seven-/eight-/nine-vertex results. + +The canonical investigation is [Discussion3156](https://github.com/CrocSwap/integer-mult-bounds/discussions/3156#discussioncomment-18999460). +[Task, handoff choice and expansion decision](TASK.json). Development and local +checking used substantial automated assistance. + +## Open next questions + +Pin one actual remaining TWOSIDE shape and check whether its small pieces +again leave a one-dimensional quotient with all edge supports below 70. +A positive complete incidence margin could justify another exclusion; +a nonpositive margin is a stop test, not a construction. Refresh the live +ledger first. The present package does not establish a complete remaining +cell or authorize further supplier construction. Structured next steps and +blockers are in [TASK.json](TASK.json). diff --git a/research/p112-larger-root-simplices/RESULT.json b/research/p112-larger-root-simplices/RESULT.json new file mode 100644 index 0000000000..dc0c650e7c --- /dev/null +++ b/research/p112-larger-root-simplices/RESULT.json @@ -0,0 +1,669 @@ +{ + "schema": "p112-larger-root-simplices/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 + }, + "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 + } + } + ], + "fixtures": { + "6": { + "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 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + 2, + 0 + ] + ], + "incidence_histogram": { + "11": 18, + "6": 19, + "10": 39, + "0": 1, + "12": 35 + }, + "maximum": 12 + }, + "7": { + "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 + ], + [ + -2, + 0, + 0, + 0, + 0, + 0, + 2, + 0 + ], + [ + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ] + ], + "incidence_histogram": { + "13": 24, + "12": 52, + "16": 35, + "0": 1 + }, + "maximum": 16 + }, + "8": { + "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 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + 2, + 0 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + "incidence_histogram": { + "15": 32, + "18": 80 + }, + "maximum": 18 + } + }, + "original_survivor_table": [ + [ + 5, + 1, + 0, + 0 + ], + [ + 5, + 2, + 0, + 0 + ], + [ + 5, + 3, + 4, + 1 + ], + [ + 5, + 4, + 15, + 1 + ], + [ + 5, + 5, + 38, + 1 + ], + [ + 5, + 6, + 77, + 1 + ], + [ + 6, + 1, + 0, + 0 + ], + [ + 6, + 2, + 1, + 1 + ], + [ + 6, + 3, + 17, + 1 + ], + [ + 6, + 4, + 69, + 1 + ], + [ + 6, + 5, + 174, + 1 + ], + [ + 6, + 6, + 364, + 1 + ], + [ + 7, + 1, + 0, + 0 + ], + [ + 7, + 2, + 2, + 1 + ], + [ + 7, + 3, + 37, + 1 + ], + [ + 7, + 4, + 154, + 1 + ], + [ + 7, + 5, + 403, + 1 + ], + [ + 7, + 6, + 885, + 1 + ], + [ + 8, + 1, + 0, + 0 + ], + [ + 8, + 2, + 3, + 1 + ], + [ + 8, + 3, + 60, + 1 + ], + [ + 8, + 4, + 251, + 1 + ], + [ + 8, + 5, + 684, + 1 + ], + [ + 8, + 6, + 1556, + 1 + ] + ], + "exclusions": [ + { + "b": 6, + "t": 4, + "weights": [ + 2, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "small_weights": [ + 2, + 5, + 5 + ], + "large_weights": [ + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "vertices": 7, + "edges": 21, + "coordinate_cap": 12, + "small_support_cap": 26, + "large_support_sum_cap": 132, + "quotient_basis_support_cap": 46, + "edge_support_cap": 66, + "outside_lower": 801, + "outside_upper": 792, + "margin": 9, + "excluded": true, + "original_cell_survivors": 69, + "weight_cover_audit": { + "distinct_basis_weight_multisets": 8, + "certified_bases": 2, + "minimum_separate_deletion_budget": 14, + "rank_four_anchor_minimum_budget": null + } + }, + { + "b": 7, + "t": 4, + "weights": [ + 2, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "small_weights": [ + 2, + 5, + 5 + ], + "large_weights": [ + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "vertices": 8, + "edges": 28, + "coordinate_cap": 16, + "small_support_cap": 26, + "large_support_sum_cap": 152, + "quotient_basis_support_cap": 46, + "edge_support_cap": 66, + "outside_lower": 1068, + "outside_upper": 1064, + "margin": 4, + "excluded": true, + "original_cell_survivors": 154, + "weight_cover_audit": { + "distinct_basis_weight_multisets": 8, + "certified_bases": 2, + "minimum_separate_deletion_budget": 14, + "rank_four_anchor_minimum_budget": null + } + }, + { + "b": 8, + "t": 4, + "weights": [ + 2, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "small_weights": [ + 2, + 5, + 5 + ], + "large_weights": [ + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "vertices": 9, + "edges": 36, + "coordinate_cap": 20, + "small_support_cap": 26, + "large_support_sum_cap": 172, + "quotient_basis_support_cap": 46, + "edge_support_cap": 66, + "outside_lower": 1388, + "outside_upper": 1376, + "margin": 12, + "excluded": true, + "original_cell_survivors": 251, + "weight_cover_audit": { + "distinct_basis_weight_multisets": 8, + "certified_bases": 2, + "minimum_separate_deletion_budget": 14, + "rank_four_anchor_minimum_budget": null + } + } + ] +} diff --git a/research/p112-larger-root-simplices/SOURCES.json b/research/p112-larger-root-simplices/SOURCES.json new file mode 100644 index 0000000000..48f24bc8e5 --- /dev/null +++ b/research/p112-larger-root-simplices/SOURCES.json @@ -0,0 +1,17 @@ +{ + "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_files": [ + {"local_path": "vendor/geometry.py", "source_head": "857384079ab640a949fb7618b7909664d3e737e5", "source_path": "research/p112-root-simplex-exclusion/geometry.py", "git_blob": "222ea556faf2b275f73815c4e7d0d5f1e3294f2f", "sha256": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021"}, + {"local_path": "vendor/ROOT-SIMPLEX-PROOF.md", "source_head": "857384079ab640a949fb7618b7909664d3e737e5", "source_path": "research/p112-root-simplex-exclusion/PROOF.md", "git_blob": "ccae08212784114e732da1192b336e47fc6a2091", "sha256": "2b5d70570e3a13d2ccc71c1fc7eef113f0d049993cb9bb24007166223ac7b734"}, + {"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"}, + {"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/PREDECESSOR-NOTICE.md", "source_head": "708f0ad8928c383de8294aea3c126e9461d2066d", "source_path": "research/p112-reduction-to-conjectures/NOTICE.md", "git_blob": "c6f3494c2c746242020ed1b7959bc48988239d6d", "sha256": "1ea58e398f40239c0945d495a807b33bcadeb6d5dcd147a12bf71ff06a9ed7ec"}, + {"local_path": "vendor/LICENSE", "source_head": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", "source_path": "LICENSE", "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4"} + ] +} diff --git a/research/p112-larger-root-simplices/TASK.json b/research/p112-larger-root-simplices/TASK.json new file mode 100644 index 0000000000..8be0e7cbb6 --- /dev/null +++ b/research/p112-larger-root-simplices/TASK.json @@ -0,0 +1,70 @@ +{ + "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": "Characteristic-zero seven-/eight-/nine-vertex root-simplex incidence lemma excluding TWOSIDE shapes 2,5^3,6^b for b=6,7,8 at t=4.", + "scope_change_reason": "Handoff-first override from Discussion3156 and PR3164. This is an exact finite proof package for three named C5-related piece shapes, not Lean formalization or a selected-interface admission.", + "bottleneck_link": "The P112 C(P112)>=64 program is a proposed decoder-cost obstruction on the binding complex side. These three exclusions shrink named low-weight piece residues; they do not prove the decoder floor or improve kappa.", + "budget_minutes": 60, + "stop_rule": "Stop at a proved named exclusion, a falsifying fixture or 60 minutes; do not expand to other cells or supplier work without a new boundary decision.", + "outcome": "completed", + "evidence": "PROOF.md and RESULT.json; complete 4,097,782-flat geometry replay, 7,140 root-plane checks, the original 24-cell table, three new exclusions and fifteen behavioral groups.", + "author": "Nick Petalas", + "ai_assistance": "Development and local checking used substantial automated assistance.", + "selection": "Handoff-first, no task-picker draw; baseline command from the provenance card passed.", + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/3156#discussioncomment-18999460", + "source_heads": { + "PR3154_DreamingOfClouds": "708f0ad8928c383de8294aea3c126e9461d2066d", + "PR3164_Nick_Petalas": "857384079ab640a949fb7618b7909664d3e737e5", + "PR3167_Nick_Petalas_overlap_control": "c2c7508f2d731feea550f1628601aebd35c6e147", + "PR3169_Nick_Petalas_concurrent_distinct_scope": "b859f7791a6d2dad68652d5a54e266cb020a1302" + }, + "boundary": "Independent pieces on P112; code intersection at least b; weights bounded by 2,5^3,6^b; characteristic-zero coefficients. No chronological word, physical bank, consumer or restoration program is supplied.", + "expansion_decision": "Narrow: finish these three mathematical exclusions. All supplier/consumer costs remain unknown here, not zero. Concurrent PR3169's (5,5) result is not duplicated; no broad census or dependent construction is authorized by this result.", + "open_questions": [ + { + "question": "Which still-open TWOSIDE weight shape admits a certified one-dimensional quotient and a larger root simplex with positive incidence margin?", + "why_it_matters": "It would remove an actual remaining piece shape without replacing a common-set obligation by a weaker per-direction deletion statement.", + "first_step": "Refresh Discussion3156 and the exact source ledger; audit one remaining shape's small-support union, quotient dimension and edge cutoff before running geometry.", + "blocked_by": "A remaining live cell and positive fully stated incidence bound are required; the present three exclusions do not settle any complete cell." + } + ] +} diff --git a/research/p112-larger-root-simplices/VERIFY.json b/research/p112-larger-root-simplices/VERIFY.json new file mode 100644 index 0000000000..df0c5d2f88 --- /dev/null +++ b/research/p112-larger-root-simplices/VERIFY.json @@ -0,0 +1,19 @@ +{ + "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": 180, + "checks": "Source bindings, complete five/six-flat capacities, Weyl-chamber quantities, all root planes, original 24-cell table, three new residue exclusions and exact receipt equality." + }, + { + "argv": ["{python}", "-O", "-W", "error", "-B", "{package}/test_verify.py"], + "timeout_seconds": 60, + "checks": "Fifteen behavioral groups with strict-boundary, failed-incidence, source/input/receipt mutants, exact rational fixture ranks and exhaustive two-level incidence assignments." + } + ] +} diff --git a/research/p112-larger-root-simplices/simplex.py b/research/p112-larger-root-simplices/simplex.py new file mode 100644 index 0000000000..75a9457ac3 --- /dev/null +++ b/research/p112-larger-root-simplices/simplex.py @@ -0,0 +1,141 @@ +"""Larger root-simplex incidence bounds and the three named weight shapes.""" + +from itertools import combinations, combinations_with_replacement, product + +from vendor.geometry import canonical, dot, require + +CAP = {2: 2, 3: 4, 4: 8, 5: 12, 6: 20, 7: 36} +TARGETS = {b: (2, 5, 5, 5) + (6,) * b for b in (6, 7, 8)} + + +def incidence_bound(b, small_cap, large_caps): + """Return a conditional certificate, never accept an uncertified boundary.""" + require(type(b) is int and 5 <= b <= 8, "unsupported simplex dimension") + require(type(small_cap) is int and 0 <= small_cap <= 112, + "invalid small-support capacity") + require(len(large_caps) == b + 1 + and all(type(x) is int and 0 <= x <= 112 for x in large_caps), + "invalid large-support capacities") + caps = sorted(large_caps) + basis_cap, edge_cap = small_cap + caps[-1], small_cap + sum(caps[-2:]) + require(basis_cap < 53, "quotient basis is not certified") + require(edge_cap < 70, "edge directions are not certified to be roots") + vertices = b + 1 + edges = vertices * b // 2 + coordinate_cap = max(vertices * vertices // 4, 2 * vertices - 3) + lower = edges * 53 - coordinate_cap * small_cap + upper = b * sum(caps) + return {"vertices": vertices, "edges": edges, "coordinate_cap": coordinate_cap, + "small_support_cap": small_cap, "large_support_sum_cap": sum(caps), + "quotient_basis_support_cap": basis_cap, "edge_support_cap": edge_cap, + "outside_lower": lower, "outside_upper": upper, + "margin": lower - upper, "excluded": lower > upper} + + +def target_bound(b): + require(type(b) is int and b in TARGETS, "unsupported target") + return {"b": b, "t": 4, "weights": list(TARGETS[b]), + "small_weights": [2, 5, 5], "large_weights": [5] + [6] * b, + **incidence_bound(b, 26, [12] + [20] * b)} + + +def feasible(weights, b): + """The pinned TWOSIDE weight-only filters, before BK/BK7.""" + require(5 <= b <= 8 and b <= len(weights) <= b + 6 + and tuple(sorted(weights)) == weights and all(w in CAP for w in weights), + "invalid ordered weight row") + distances = (0, 53, 78, 92, 100, 106, 109, 111, 112) + for level in range(1, b + 1): + prefix = weights[:len(weights) - b + level] + global_cap = sum(CAP[w] for w in prefix) + target_cap = sum(32 if w == 7 else CAP[w] for w in prefix) + 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 < distances[level]: + return False + return True + + +def basis_killed(weights, b): + basis = weights[:len(weights) - b] + if sum(CAP[w] for w in basis) >= 53: + return False + if sum(basis) <= 7: + return True + for assignment in product((0, 1), repeat=len(basis)): + loads = [sum(w for w, group in zip(basis, assignment, strict=True) if group == g) + for g in (0, 1)] + if max(loads) <= 6: + return True + return False + + +def survivor_rows(b, t=4): + require(type(b) is int and 5 <= b <= 8 and type(t) is int and 1 <= t <= 6, + "invalid TWOSIDE cell") + rows = [] + for size in range(b, b + t + 1): + for weights in combinations_with_replacement(range(2, 8), size): + if (sum(w - 2 for w in weights) < 6 * b and feasible(weights, b) + and not basis_killed(weights, b)): + rows.append(weights) + return tuple(rows) + + +def cover_audit(weights): + """Exhaust all four-piece weight-certified bases and two six-flat packs.""" + require(weights in TARGETS.values(), "unsupported cover-audit shape") + costs, anchored_costs = [], [] + bases = set(combinations(weights, 4)) + certified = 0 + for basis in sorted(bases): + if sum(CAP[w] for w in basis) >= 53: + continue + certified += 1 + rest = list(weights) + for w in basis: + rest.remove(w) + for assignment in product((0, 1, 2), repeat=4): + loads = [sum(w for w, g in zip(basis, assignment, strict=True) if g == i) + for i in (0, 1)] + if max(loads) > 6: + continue + cost = sum(CAP[w] for w, g in zip(basis, assignment, strict=True) if g == 2) + costs.append(cost) + if min(rest) <= 4: + anchored_costs.append(cost) + require(costs and certified == 2, "weight-certified cover inventory changed") + return {"distinct_basis_weight_multisets": len(bases), "certified_bases": certified, + "minimum_separate_deletion_budget": min(costs), + "rank_four_anchor_minimum_budget": min(anchored_costs, default=None)} + + +def simplex_fixture(roots, points, b): + """One literal positive fixture per size; not universal direction coverage.""" + require(b in (6, 7, 8), "unsupported fixture size") + vertices = [(0,) * 8] + for i in range(1, min(b, 7) + 1): + vertex = [0] * 8 + vertex[0], vertex[i] = (-2 if b == 7 else 2), 2 + vertices.append(tuple(vertex)) + if b == 8: + vertices.append((1,) * 8) + require(len(vertices) == b + 1, "fixture vertex count") + edges = [canonical(tuple(x - y for x, y in zip(a, c, strict=True))) + for a, c in combinations(vertices, 2)] + require(len(set(edges)) == b * (b + 1) // 2 and all(e in roots for e in edges), + "fixture is not a root simplex") + require(all(dot(a, c) == (8 if i == j else 4) + for i, a in enumerate(vertices[1:]) for j, c in enumerate(vertices[1:])), + "fixture Gram matrix is not I+J") + histogram = {} + for root in points: + values = [dot(root, vertex) for vertex in vertices] + count = sum(x != y for x, y in combinations(values, 2)) + histogram[str(count)] = histogram.get(str(count), 0) + 1 + maximum = max(map(int, histogram)) + require(maximum <= (b + 1) ** 2 // 4, "fixture exceeds universal incidence cap") + return {"vertices": [list(v) for v in vertices], "incidence_histogram": histogram, + "maximum": maximum} diff --git a/research/p112-larger-root-simplices/test_verify.py b/research/p112-larger-root-simplices/test_verify.py new file mode 100644 index 0000000000..390a3dbac7 --- /dev/null +++ b/research/p112-larger-root-simplices/test_verify.py @@ -0,0 +1,168 @@ +"""Behavioral controls and independent small exact checks.""" + +import copy +import json +import tempfile +import unittest +from fractions import Fraction +from itertools import combinations, product +from pathlib import Path + +from simplex import ( + CAP, + TARGETS, + basis_killed, + cover_audit, + feasible, + incidence_bound, + simplex_fixture, + survivor_rows, + target_bound, +) +from vendor.geometry import root_data +from verify import DATA, PACKAGE, ROOT, bind_data, bind_sources, check_receipt + + +def rational_rank(rows): + matrix = [[Fraction(x) for x in row] for row in rows] + rank = 0 + for column in range(8): + pivot = next((i for i in range(rank, len(matrix)) if matrix[i][column]), None) + if pivot is None: + continue + matrix[rank], matrix[pivot] = matrix[pivot], matrix[rank] + scale = matrix[rank][column] + matrix[rank] = [x / scale for x in matrix[rank]] + for i in range(rank + 1, len(matrix)): + scale = matrix[i][column] + matrix[i] = [x - scale * y for x, y in zip(matrix[i], matrix[rank], strict=True)] + rank += 1 + return rank + + +class Controls(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.roots, cls.points, cls.labels, _ = root_data() + cls.sources = bind_sources() + + def test_exact_new_margins(self): + self.assertEqual([target_bound(b)["margin"] for b in TARGETS], [9, 4, 12]) + self.assertTrue(all(target_bound(b)["excluded"] for b in TARGETS)) + + def test_original_six_vertex_control(self): + self.assertEqual(incidence_bound(5, 26, [12] + [20] * 5)["margin"], 1) + self.assertEqual(incidence_bound(5, 20, [20] * 6)["margin"], 15) + + def test_one_more_small_coordinate_loses_each_exclusion(self): + for b in TARGETS: + self.assertFalse(incidence_bound(b, 27, [12] + [20] * b)["excluded"]) + + def test_one_more_large_coordinate_boundary(self): + self.assertEqual(incidence_bound(7, 26, [13] + [20] * 7)["margin"], -3) + + def test_strict_quotient_boundary(self): + with self.assertRaisesRegex(ValueError, "quotient basis"): + incidence_bound(6, 33, [20] * 7) + + def test_strict_root_boundary(self): + with self.assertRaisesRegex(ValueError, "edge directions"): + incidence_bound(6, 30, [20] * 7) + + def test_invalid_shapes(self): + for b, small, caps in ((4, 26, [20] * 5), (6, -1, [20] * 7), + (6, 26, [20] * 6), (6, 26, [True] * 7)): + with self.assertRaises(ValueError): + incidence_bound(b, small, caps) + with self.assertRaises(ValueError): + target_bound(True) + + def test_all_two_level_incidence_assignments(self): + for n in (6, 7, 8, 9): + maximum = 0 + for tail in product((0, 1), repeat=n - 1): + values = (0,) + tail + count = sum(x != y for x, y in combinations(values, 2)) + maximum = max(maximum, count) + self.assertEqual(maximum, n * n // 4) + self.assertLessEqual(2 * n - 3, maximum) + + def test_literal_simplex_ranks_and_incidence(self): + maxima = [] + for b in TARGETS: + fixture = simplex_fixture(self.roots, self.points, b) + self.assertEqual(rational_rank(fixture["vertices"]), b) + self.assertEqual(sum(fixture["incidence_histogram"].values()), 112) + maxima.append(fixture["maximum"]) + self.assertEqual(maxima, [12, 16, 18]) + + def test_actual_survivors(self): + for b, expected in ((6, 69), (7, 154), (8, 251)): + rows = survivor_rows(b) + self.assertEqual(len(rows), expected) + self.assertIn(TARGETS[b], rows) + self.assertTrue(feasible(TARGETS[b], b)) + self.assertFalse(basis_killed(TARGETS[b], b)) + + def test_independent_target_prefix_and_packing_checks(self): + thresholds = [53, 78, 92, 100, 106, 109, 111, 112] + for b, weights in TARGETS.items(): + # Direct prefix checks for these targets, which contain no sevens. + for level in range(1, b + 1): + self.assertGreaterEqual(sum(CAP[w] for w in weights[:4 + level]), + thresholds[level - 1]) + self.assertEqual(sum(weights[:4]), 17) + self.assertEqual(sum(CAP[w] for w in weights[:4]), 38) + self.assertGreater(sum(weights[:4]), 12) + self.assertLess(sum(w - 2 for w in weights), 6 * b) + + def test_cover_and_anchor_overlap_controls(self): + for weights in TARGETS.values(): + result = cover_audit(weights) + self.assertEqual(result["minimum_separate_deletion_budget"], 14) + self.assertIsNone(result["rank_four_anchor_minimum_budget"]) + with self.assertRaises(ValueError): + cover_audit((2, 5, 5, 6)) + + def test_input_binding_and_label_mutant(self): + self.assertEqual(bind_data(ROOT / DATA, self.points, self.labels, self.sources), + self.sources["files"][2]["sha256"]) + with self.assertRaisesRegex(ValueError, "label binding"): + bind_data(ROOT / DATA, self.points, self.labels[::-1], self.sources) + 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, self.sources) + + def test_source_binding_and_path_mutants(self): + with tempfile.TemporaryDirectory() as directory: + package = Path(directory) + (package / "vendor").mkdir() + for row in self.sources["retained_files"]: + path = row["local_path"] + (package / path).write_bytes((PACKAGE / path).read_bytes()) + manifest = package / "SOURCES.json" + manifest.write_text(json.dumps(self.sources)) + self.assertEqual(bind_sources(package), self.sources) + path = package / self.sources["retained_files"][0]["local_path"] + path.write_bytes(path.read_bytes() + b"\n") + with self.assertRaisesRegex(ValueError, "changed retained source"): + bind_sources(package) + mutant = copy.deepcopy(self.sources) + mutant["retained_files"][0]["local_path"] = "../outside" + manifest.write_text(json.dumps(mutant)) + with self.assertRaisesRegex(ValueError, "invalid retained-source path"): + bind_sources(package) + + def test_receipt_mutant(self): + expected = json.loads((PACKAGE / "RESULT.json").read_text()) + check_receipt(expected, copy.deepcopy(expected)) + mutant = copy.deepcopy(expected) + mutant["exclusions"][0]["coordinate_cap"] = 11 + with self.assertRaisesRegex(ValueError, "receipt differs"): + check_receipt(mutant, expected) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/p112-larger-root-simplices/vendor/LICENSE b/research/p112-larger-root-simplices/vendor/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/p112-larger-root-simplices/vendor/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/p112-larger-root-simplices/vendor/PREDECESSOR-NOTICE.md b/research/p112-larger-root-simplices/vendor/PREDECESSOR-NOTICE.md new file mode 100644 index 0000000000..c6f3494c2c --- /dev/null +++ b/research/p112-larger-root-simplices/vendor/PREDECESSOR-NOTICE.md @@ -0,0 +1,3 @@ +# Notice + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0 (`LICENSE`, copied from the repository root). diff --git a/research/p112-larger-root-simplices/vendor/ROOT-SIMPLEX-PROOF.md b/research/p112-larger-root-simplices/vendor/ROOT-SIMPLEX-PROOF.md new file mode 100644 index 0000000000..ccae082127 --- /dev/null +++ b/research/p112-larger-root-simplices/vendor/ROOT-SIMPLEX-PROOF.md @@ -0,0 +1,176 @@ +# A root-simplex incidence obstruction + +## Statement and scope + +Let `K` be any characteristic-zero field. On the 112 live E8 root lines, +let `ell(t)` be the pinned binary label and let + +``` +C = {c_h : c_h(t) = , h in K^8}, +w(q) = rank_F2 {ell(t) : q(t) != 0}. +``` + +The coordinate representatives `r_t` may be doubled roots, as in the replay. +This changes no supports. Suppose nine linearly independent pieces span `T` +and `dim(T intersect C) >= 5`. Their weights cannot be bounded respectively by +either of these multisets: + +``` +3,4,4,6,6,6,6,6,6 +2,5,5,5,6,6,6,6,6. +``` + +These are precisely the two remaining `(b,t)=(5,4)` TWOSIDE beta shapes +reported by [PR3162](https://github.com/CrocSwap/integer-mult-bounds/pull/3162). The new theorem excludes them directly, without a +space-pair or deletion-set census. Combining it with that predecessor's +thirteen exclusions removes its fifteen-shape residue. That combination +inherits the predecessor's finite theorem and TWOSIDE reduction. Neither +full C5, the other beta cells, `C(P112)>=64`, supplier admission nor kappa +is established here. + +## Geometry used, with bounded replay + +The replay reconstructs the 120 E8 root lines and removes the eight pinned +frame lines. All 960 simple reflections preserve the root inventory. +Simple-root coordinates modulo two, with a leading one, give +the nine-bit labels. Their bytes agree with the declared main-branch input. +All 3,309,747 four-dimensional annihilators and all 788,035 three-dimensional +annihilators in `F2^9` are enumerated in unique reverse row-echelon form. +Their kernels establish the sharp support capacities `g(5)=12`, `g(6)=20`. +For `d=2,3,4`, the leading-one coordinate gives the elementary upper bound +`g(d)<=2^(d-1)`, hence capacities `2,4,8`. A lower-dimensional support extends +to a flat of the stated dimension, so upper bounds on piece weights suffice. + +Every nonzero codeword has support at least 53. Moreover, a codeword with +support below 70 is proportional to an E8 root codeword. Here is the +Weyl-chamber argument, with its finite quantities checked by the replay. +Below 70 means at least 43 live root lines are perpendicular. In a closed +Weyl chamber, perpendicular roots are generated by vanishing simple roots. +All 28 choices of six simple nodes contain at most 36 root lines. Thus +at least seven simple roots vanish. The eight seven-node faces have root-line +counts `42,28,22,14,16,23,37,63`. Only the last can reach 43; its normal is +a root direction. Weyl transformations preserve roots. Root directions have +live support 53 for 112 lines, or 56 for the eight removed frame lines. +This also proves the distance 53, since any putative smaller support would +be a root direction. The standard finite-root-system Weyl-chamber theorem +is used here, not formally proved by the executable. + +This argument extends to `K`. The rational roots perpendicular to a nonzero +field-valued direction have rational rank at most seven. If that rank were +at most six, a generic real normal to their span would have exactly the +roots in that span perpendicular, contradicting the rank-six bound of 36. +Thus the rank is seven, the rational kernel is one-dimensional, and the +direction is proportional over `K` to its rational generator. Apply the real +argument to that generator. The P112 roots span eight dimensions, so the +map `h -> c_h` is injective. + +## From nine pieces to six affine vertices + +Split the basis into three small pieces `s_1,s_2,s_3` and six remaining +pieces `q_0,...,q_5`. Put `S=union supp(s_j)`, `s=|S|`, and +`U=sum_i |supp(q_i)|`. In the first shape choose small weights `3,4,4`; +in the second choose `2,5,5`. + +Write `D=T intersect C` and let `lambda:T -> T/D`. Since `dim T=9` and +`dim D>=5`, the quotient has dimension at most four. For either split, +`S` together with the support of any one `q_i` has fewer than 53 lines. +The corresponding four quotient images are independent. Otherwise a +nonzero combination of four independent pieces would be a nonzero +codeword supported on fewer than 53 lines. Hence `dim(T/D)=4`, and the +three small quotient images are independent. + +Modulo their span, all six images of the `q_i` are nonzero in a +one-dimensional space. Rescale each `q_i` to give them the same image. +Supports and independence are preserved. There are unique small-piece +combinations `a_i` such that + +``` +c_i = q_i - q_0 - a_i belongs to D, i=1,...,5. +``` + +Set `c_0=0` and `a_0=0`. The five `c_i` are independent, by their distinct unit +coefficients on the nonbasis pieces `q_1,...,q_5`. Every edge + +``` +c_i-c_j = q_i-q_j-(a_i-a_j) +``` + +is nonzero and supported on `S union supp(q_i) union supp(q_j)`. +The support caps are at most 60 for the first shape and 66 for the second. +They are below 70, so all fifteen edges are root directions. By injectivity, +there are five independent vectors `h_i` with `c_i=c_{h_i}`, and each +nonzero difference among `0,h_1,...,h_5` is a scalar root. + +## Root-simplex lemma + +Normalize the real E8 roots to norm squared two. For two distinct root +lines, the only possible third root line in their rational plane occurs +in an A2 subsystem. It is represented by `alpha +/- beta` with coefficients +of absolute value one. The replay checks all 7,140 root-line pairs against +all 120 root lines using exact Gram determinants. It finds 3,780 planes +with two root lines and 3,360 with three. Alternatively this is the usual +rank-two simply-laced root-system fact. + +This fact applies to a plane over `K` as well: any rational root in the +`K`-span of two independent rational roots is already in their rational +span, by solving a nonsingular rational two-by-two coordinate minor. + +Write `h_i=b_i alpha_i`. Independence makes every pair of `alpha_i` +nonparallel. Since `h_i-h_j` is a third root line, the plane fact gives +`b_i/b_j=+1` or `-1`. Absorb these signs into the oriented roots. Thus +`h_i=b alpha_i` for one `b!=0`. Applying the same plane fact to their +differences gives `=1` and makes each +`alpha_i-alpha_j` an actual norm-two root. The six vertices +`0,alpha_1,...,alpha_5` form a root A5 simplex. + +Fix any E8 root `r` and evaluate it on those vertices. The six values + +``` +v = (0, , ..., ) +``` + +are integers. Every difference is the inner product of two roots, hence +lies in `{-2,-1,0,1,2}`. If some difference has absolute value two, +equality in Cauchy-Schwarz makes `r` the corresponding oriented edge root. +The six values then have multiplicities `1,1,4`, giving nine unequal pairs. +If no difference has absolute value two, all values occupy at most two +consecutive integer levels. There are at most `3*3=9` unequal pairs again. +Thus every live coordinate belongs to at most nine of the fifteen edge +supports. Multiplication by the common field scalar `b` changes no zeros. +This bound is universal; the literal A5 fixture in the replay is only a +sharp positive control, not a replacement for the argument. + +## Count incidences and exclude both shapes + +Each edge codeword has at least 53 nonzero coordinates. At most `9s` edge +incidences occur in `S`. Outside `S`, its coordinate is exactly +`q_i(t)-q_j(t)`. An unequal pair has a nonzero endpoint, and each nonzero +one of the six `q_i(t)` can meet only five pairs. Summing over coordinates, + +``` +15*53 - 9s <= outside edge incidences <= 5U. +``` + +The support capacities give the following contradictions. Upper bounds on +`s` decrease the left side and upper bounds on `U` increase the right side, +so overlaps or smaller actual supports only strengthen them. + +| Nine-piece shape | Small pieces | s cap | U cap | Required inequality | +|---|---|---:|---:|---| +| `3,4^2,6^6` | `3,4,4` | 20 | 120 | `615 <= 600` | +| `2,5^3,6^5` | `2,5,5` | 26 | 112 | `561 <= 560` | + +The second exclusion has margin exactly one under these bounds. Increasing +its small-support allowance from 26 to 27 would remove this contradiction; +the boundary control deliberately checks that case. No hypothesis that +the common deletion union lies in a five-flat is used. + +## Remaining obligations + +The proof concerns these two nine-piece configurations under the stated +intersection hypothesis. It uses the standard Weyl-chamber theorem and +finite exact capacity checks. There is no proof-kernel verification or +independent human review. The separate PR3162 reductions, the original +TWOSIDE feasibility filters and all other conjectures in PR3154 remain +their own dependencies. A closed weight residue does not certify a +decoder floor, a complete multiplication theorem or an improved exponent. diff --git a/research/p112-larger-root-simplices/vendor/TWOSIDE-NOTES.md b/research/p112-larger-root-simplices/vendor/TWOSIDE-NOTES.md new file mode 100644 index 0000000000..e3fd3f2b1d --- /dev/null +++ b/research/p112-larger-root-simplices/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-larger-root-simplices/vendor/__init__.py b/research/p112-larger-root-simplices/vendor/__init__.py new file mode 100644 index 0000000000..8df6dc3149 --- /dev/null +++ b/research/p112-larger-root-simplices/vendor/__init__.py @@ -0,0 +1 @@ +"""Pinned predecessor sources, isolated from installed packages of this name.""" diff --git a/research/p112-larger-root-simplices/vendor/bk2b.py b/research/p112-larger-root-simplices/vendor/bk2b.py new file mode 100644 index 0000000000..3394029014 --- /dev/null +++ b/research/p112-larger-root-simplices/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-larger-root-simplices/vendor/geometry.py b/research/p112-larger-root-simplices/vendor/geometry.py new file mode 100644 index 0000000000..222ea556fa --- /dev/null +++ b/research/p112-larger-root-simplices/vendor/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-larger-root-simplices/verify.py b/research/p112-larger-root-simplices/verify.py new file mode 100644 index 0000000000..534c077b8a --- /dev/null +++ b/research/p112-larger-root-simplices/verify.py @@ -0,0 +1,127 @@ +"""Replay larger-simplex geometry, source bindings and the three exclusions.""" + +import argparse +import hashlib +import json +import subprocess +import sys +from pathlib import Path + +from simplex import TARGETS, cover_audit, simplex_fixture, survivor_rows, target_bound +from vendor.geometry import ( + chamber_receipt, + flat_capacity, + require, + root_data, + root_plane_receipt, +) + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +DATA = "research/one-sided-six-multisets/data/data.txt" + + +def bounded_bytes(path, limit=2_000_000): + require(path.is_file() and not path.is_symlink() and path.stat().st_size <= limit, + f"missing, linked or oversized input: {path}") + return path.read_bytes() + + +def bind_sources(package=PACKAGE): + sources = json.loads(bounded_bytes(package / "SOURCES.json")) + retained = sources["retained_files"] + require(1 <= len(retained) <= 10, "invalid retained-source inventory") + require(len({row["local_path"] for row in retained}) == len(retained), + "duplicate retained source") + for row in retained: + path = Path(row["local_path"]) + require(len(path.parts) == 2 and path.parts[0] == "vendor" and ".." not in path.parts, + "invalid retained-source path") + raw = bounded_bytes(package / path) + require(hashlib.sha256(raw).hexdigest() == row["sha256"], + f"changed retained source: {path}") + blob = hashlib.sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + require(blob == row["git_blob"], f"changed retained Git bytes: {path}") + return sources + + +def bind_data(path, points, labels, sources): + pins = [row for row in sources["files"] if row["usage"] == "input"] + require(len(pins) == 1 and pins[0]["path"] == DATA, "live-input inventory") + raw = bounded_bytes(path) + 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 predecessor_table(): + result = subprocess.run([sys.executable, "-I", "-B", str(PACKAGE / "vendor/bk2b.py")], + cwd=PACKAGE, capture_output=True, text=True, check=True, + timeout=120) + require(not result.stderr and len(result.stdout) <= 4096, "unexpected predecessor output") + rows = [tuple(map(int, line.split())) for line in result.stdout.splitlines()] + require(len(rows) == 24 and all(len(row) == 4 for row in rows), "incomplete original table") + require([(r[0], r[1]) for r in rows] == [(b, t) for b in range(5, 9) for t in range(1, 7)], + "original table cell order") + return rows + + +def exclusion_receipt(table): + rows = [] + for b, expected in ((6, 69), (7, 154), (8, 251)): + survivors = survivor_rows(b) + require(len(survivors) == expected and TARGETS[b] in survivors, + "target is not in the stated original residue") + require(next(r[2] for r in table if r[:2] == (b, 4)) == len(survivors), + "original and new survivor counts disagree") + audit = cover_audit(TARGETS[b]) + require(audit["minimum_separate_deletion_budget"] == 14 + and audit["rank_four_anchor_minimum_budget"] is None, + "prior cover/anchor overlap boundary changed") + rows.append({**target_bound(b), "original_cell_survivors": len(survivors), + "weight_cover_audit": audit}) + require([r["margin"] for r in rows] == [9, 4, 12], "three contradiction margins") + return rows + + +def receipt(data_path=ROOT / DATA): + sources = bind_sources() + roots, points, labels, coordinates = root_data() + digest = bind_data(data_path, points, labels, sources) + table = predecessor_table() + return {"schema": "p112-larger-root-simplices/v1", "input_sha256": digest, + "chamber": chamber_receipt(roots, points, coordinates), + "root_planes": root_plane_receipt(roots), + "flat_capacities": [flat_capacity(labels, d) for d in (5, 6)], + "fixtures": {str(b): simplex_fixture(roots, points, b) for b in TARGETS}, + "original_survivor_table": table, "exclusions": exclusion_receipt(table)} + + +def check_receipt(actual, expected): + # Canonical JSON also normalizes the original table's internal tuples. + require(json.dumps(actual, sort_keys=True) == json.dumps(expected, sort_keys=True), + "committed mathematical receipt differs") + + +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: + check_receipt(result, json.loads(bounded_bytes(PACKAGE / "RESULT.json"))) + else: + path = args.output.expanduser().resolve() + require(not path.is_relative_to(ROOT), "receipt output must be outside checkout") + with path.open("x", encoding="utf-8") as stream: + stream.write(json.dumps(result, indent=2) + "\n") + print("PASS_LARGER_ROOT_SIMPLICES margins=9,4,12 flats=4097782 root_pairs=7140") + + +if __name__ == "__main__": + main()