From 92675b36a8e0ea41b40f0bcda2a3dd9f313abb0e Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Sat, 17 Oct 2026 16:36:14 +0100 Subject: [PATCH] test(research): exclude P112 3,4,6^8 with a weighted A6 cover --- research/p112-a6-weighted-cover/CHECKS.json | 64 +++ .../p112-a6-weighted-cover/ENGINEERING.md | 69 +++ research/p112-a6-weighted-cover/PROOF.md | 239 +++++++++ research/p112-a6-weighted-cover/README.md | 94 ++++ research/p112-a6-weighted-cover/RESULT.json | 505 ++++++++++++++++++ research/p112-a6-weighted-cover/SOURCES.json | 172 ++++++ research/p112-a6-weighted-cover/TASK.json | 76 +++ research/p112-a6-weighted-cover/VERIFY.json | 31 ++ research/p112-a6-weighted-cover/bound.py | 115 ++++ .../p112-a6-weighted-cover/independent.py | 172 ++++++ .../independent_weighted.py | 137 +++++ .../p112-a6-weighted-cover/test_verify.py | 215 ++++++++ .../p112-a6-weighted-cover/vendor/LICENSE | 201 +++++++ .../vendor/PREDECESSOR-NOTICE.md | 3 + .../vendor/ROOT-SIMPLEX-PROOF.md | 176 ++++++ .../vendor/TWOSIDE-NOTES.md | 65 +++ .../p112-a6-weighted-cover/vendor/bk2b.py | 29 + .../p112-a6-weighted-cover/vendor/geometry.py | 188 +++++++ .../p112-a6-weighted-cover/vendor/mixed.py | 358 +++++++++++++ research/p112-a6-weighted-cover/verify.py | 138 +++++ research/p112-a6-weighted-cover/weighted.py | 185 +++++++ 21 files changed, 3232 insertions(+) create mode 100644 research/p112-a6-weighted-cover/CHECKS.json create mode 100644 research/p112-a6-weighted-cover/ENGINEERING.md create mode 100644 research/p112-a6-weighted-cover/PROOF.md create mode 100644 research/p112-a6-weighted-cover/README.md create mode 100644 research/p112-a6-weighted-cover/RESULT.json create mode 100644 research/p112-a6-weighted-cover/SOURCES.json create mode 100644 research/p112-a6-weighted-cover/TASK.json create mode 100644 research/p112-a6-weighted-cover/VERIFY.json create mode 100644 research/p112-a6-weighted-cover/bound.py create mode 100644 research/p112-a6-weighted-cover/independent.py create mode 100644 research/p112-a6-weighted-cover/independent_weighted.py create mode 100644 research/p112-a6-weighted-cover/test_verify.py create mode 100644 research/p112-a6-weighted-cover/vendor/LICENSE create mode 100644 research/p112-a6-weighted-cover/vendor/PREDECESSOR-NOTICE.md create mode 100644 research/p112-a6-weighted-cover/vendor/ROOT-SIMPLEX-PROOF.md create mode 100644 research/p112-a6-weighted-cover/vendor/TWOSIDE-NOTES.md create mode 100644 research/p112-a6-weighted-cover/vendor/bk2b.py create mode 100644 research/p112-a6-weighted-cover/vendor/geometry.py create mode 100644 research/p112-a6-weighted-cover/vendor/mixed.py create mode 100644 research/p112-a6-weighted-cover/verify.py create mode 100644 research/p112-a6-weighted-cover/weighted.py diff --git a/research/p112-a6-weighted-cover/CHECKS.json b/research/p112-a6-weighted-cover/CHECKS.json new file mode 100644 index 0000000000..492c1c9401 --- /dev/null +++ b/research/p112-a6-weighted-cover/CHECKS.json @@ -0,0 +1,64 @@ +{ + "schema": "p112-a6-weighted-cover-checks/v1", + "evidence_status": "author-checked with separately implemented finite algorithms; not independent human or proof-kernel review", + "environment": { + "platform": "Linux 6.6.87.2-microsoft-standard-WSL2, x86_64 GNU/Linux", + "python_primary": "3.12.15", + "python_secondary": "3.13.5", + "dependencies": "Python standard library only", + "scratch_policy": "All exports, bytecode, receipts and logs use one session-owned directory under ~/.cache/integer-mult-bounds-runs/; replays do not write generated outputs into the checkout." + }, + "checks": [ + { + "command": "TMPDIR=$RUN PYTHONWARNINGS=error python3.12 -B scripts/research_package.py --package research/p112-a6-weighted-cover", + "result": "PASS_REGISTERED_RESEARCH_PACKAGE; all four sequential commands and sixteen optimized behavioral groups pass" + }, + { + "command": "python3.13 -B -O research/p112-a6-weighted-cover/verify.py --output $RUN/receipt-313.json; cmp $RUN/receipt-313.json research/p112-a6-weighted-cover/RESULT.json", + "result": "PASS_A6_WEIGHTED_COVER and exact receipt byte equality" + }, + { + "command": "python3.13 -B -O research/p112-a6-weighted-cover/independent_weighted.py", + "result": "PASS_INDEPENDENT_A6_WEIGHTED" + }, + { + "command": "Copy the package and sole declared input into a Git-free root, make the export read-only, then run verify.py, independent.py, independent_weighted.py and test_verify.py with python3.13 -B -O and external TMPDIR", + "result": "All three mathematical markers and sixteen tests pass without Git, network access or writes into the export" + }, + { + "command": "ruff check --no-cache research/p112-a6-weighted-cover/*.py", + "result": "All configured checks pass on new source; immutable vendor bytes retain predecessor formatting" + }, + { + "command": "python3.12 -X pycache_prefix=$RUN/compile-cache -W error -m compileall -q research/p112-a6-weighted-cover", + "result": "PASS; bytecode remains external" + } + ], + "exact_results": { + "mixed_five_cliques": 7350, + "independent_rank_six_cases": 3360, + "mixed_lower": 142, + "all_root_unstructured_losing_lower": 137, + "frame_and_six_flat_only_losing_lower": 139, + "weighted_all_root_lower": 141, + "endpoint_allowance": 140, + "weighted_six_flat_subspaces": 788035, + "independent_four_flat_subspaces": 3309747, + "orthogonal_frames": 2025, + "retained_six_flat_masks": 63, + "retained_four_flat_masks": 135, + "relevant_prefixes": 7140, + "four_flat_tests": 963900 + }, + "review_lenses": [ + "Checked the quotient independence, characteristic-zero direction reduction, complete star/graph coverage and weighted threshold implications against PROOF.md.", + "Checked source/export boundaries, deterministic receipts, explicit traversal limits and meaningful corruption/losing controls against the executable commands. These are local author checks, not separate human reviews." + ], + "publication_validation": "After committing, run scripts/check_research_commit.py for this package and replay a read-only export from the exact commit. The PR reports the actual checked publication hash.", + "unrun_obligations": [ + "Independent human review and proof-kernel formalization", + "Full C5, all TWOSIDE residues and the P112 decoder floor", + "Native supplier, physical caller, precision, restoration and outer multiplication replay", + "Hosted CI is separate from these local checks" + ] +} diff --git a/research/p112-a6-weighted-cover/ENGINEERING.md b/research/p112-a6-weighted-cover/ENGINEERING.md new file mode 100644 index 0000000000..c8b8be6093 --- /dev/null +++ b/research/p112-a6-weighted-cover/ENGINEERING.md @@ -0,0 +1,69 @@ +# Implementation scope and bounds + +The retained predecessor files are immutable inputs, not shared-code edits. +New code is limited to this package's exact certificate, separate finite +checks, CLI and tests. There is no network access, native build, recursion, +dynamic evaluation or background process in its replay. + +## Design choices + +- Build the lever. Keep the complete argument's finite decisions in scripts + and a deterministic receipt, rather than a hand-maintained numerical table. +- Prove it works. Compare reconstructed roots with the actual pinned input, + compare independent graph/flat/frame inventories, run deliberate failures + under optimization, and check the final committed export and publication bytes. +- Do not expand an already covered case. The first `2,4,6^8` candidate was + discarded after finding PR3162's implication. The one bounded pivot retains + an actual different profile and two losing controls, 137 and 139. + +## Power-of-ten inspection + +1. Calls are acyclic. Traversals use explicit bounded stacks or queues. + The only subprocess is the original TWOSIDE program, waited on with + `check=True` and a 120-second timeout. Exceptions propagate as replay failure. +2. Dimensions are fixed at eight real coordinates and nine binary coordinates. + There are 120 root lines, 248 rays, 58 graph vertices, 7,350 five-cliques, + 788,035 six-flats, 3,309,747 four-flats and 2,025 frames. Exhaustion checks + enforce the predecessor's 40,000-state clique and 407-entry stack limits; + the new frame traversal allows at most 2,000,000 visits and 961 stack entries. + Flat loops are finite products of at most nine-bit row choices. The + root-generated four-flat loop has `binom(35,4)=52,360` iterations. The + relevant weighted pair check has exactly 963,900 tests. +3. Python and its standard library allocate dynamically. Strict allocation-free + operation is unavailable in this implementation. The compensating limits + are the fixed domains above, retained sets of 63 and 135 flat masks, at most + 2,025 frames, and no concurrent replay commands. The independent clique + list has 7,350 entries; source reads are bounded by two MB and path depth 32. + Input files and output streams are opened with scoped cleanup. A future + constrained-memory implementation would use preallocated native buffers + only if a measured resource limit requires it. +4. New functions remain below the approximately sixty-line review ceiling. + They separate inventory generation, exact costs, source binding and CLI + publication. No forwarding framework or migration layer was introduced. +5. Mathematical and source invariants use `require`, which raises normally, + not Python assertions. The optimized test command checks corruption, + unsupported domains, exhausted/truncated inventories and changed receipts. +6. Mutable search state is local to its owner. Module constants are fixed + tuples, integers, paths or immutable sets. No selected record is modified. +7. Boundary reads validate paths, size, raw hashes and source semantics. + JSON and arithmetic errors fail replay. Output is exclusive-create outside + the checkout; overwrites and in-checkout destinations are rejected. +8. There is no code generation, reflection-based mathematical dispatch, + dynamic import selection or evaluation. Standard `unittest` discovery is + the bounded testing framework, not certificate logic. +9. Python member access and standard-library calls replace pointer operations. + The test framework uses its normal dynamic method dispatch over sixteen + named tests. This is a platform deviation from a ban on indirect calls; + production mathematical calls have visible fixed targets. Removing the + framework would not improve the certificate and is outside this scope. +10. Verification runs configured Ruff diagnostics on new source, warning-as-error + compilation in an external bytecode namespace, normal/optimized replays, + and both installed Python versions. Frozen vendor code keeps its exact + predecessor bytes, including original formatting and APIs. It is reviewed + as a dependency; style cleanup would invalidate its source pins and is + deferred to an explicitly versioned successor, not silently performed here. + +The managed-runtime allocation and unittest dispatch deviations are limited +to this finite standard-library package. The recorded checks enforce their +compensating bounds. No timing or multiplication-runtime speedup is claimed. +See `CHECKS.json` for the exact executed commands and verification limits. diff --git a/research/p112-a6-weighted-cover/PROOF.md b/research/p112-a6-weighted-cover/PROOF.md new file mode 100644 index 0000000000..8a129bc017 --- /dev/null +++ b/research/p112-a6-weighted-cover/PROOF.md @@ -0,0 +1,239 @@ +# The P112 `3,4,6^8` profile is impossible + +## Statement + +Use the pinned 112 live E8 root lines `r_t` and their nine-bit labels `ell(t)`. +For any characteristic-zero field `K`, define + +``` +C = {c_h : c_h(t)=, h in K^8}, +w(q) = rank_F2 {ell(t) : q(t) != 0}. +``` + +There do not exist ten independent pieces spanning `T`, with +`dim(T intersect C)>=6`, whose respective weight upper bounds are + +``` +3,4,6,6,6,6,6,6,6,6. +``` + +This is one actual TWOSIDE `(b,t)=(6,4)` profile from DreamingOfClouds's +PR3154 at `708f0ad8928c383de8294aea3c126e9461d2066d`. It is not the whole +cell, C5, the P112 decoder floor or a supplier theorem. + +## Retained geometry and exact coverage + +The source-bound [root-simplex proof](vendor/ROOT-SIMPLEX-PROOF.md) and +Nick Petalas's PR3176 supply these geometric arguments: + +- Weight-three and weight-four supports have at most four and eight lines. + Every label has leading bit one, so a binary `d`-flat contains at most + `2^(d-1)` labels. A weight-six support has at most twenty live lines. + The replay enumerates all 788,035 three-dimensional annihilators in + `F2^9` to check this last bound. +- `h -> c_h` is injective and every nonzero codeword has at least 53 live + coordinates. +- A real subspace of dimension at most six contains at most 36 E8 root lines. + The eight seven-node chamber faces contain respectively + `42,28,22,14,16,23,37,63` root lines. The 42-line face has a D7 normal; + the 63-line face has a root normal. +- Independent scalar-root directions whose pair differences are scalar + roots have one common scale and orientations making a root star, with + squared norm two and distinct inner products one. + +The standard Weyl-chamber theorem remains an explicit dependency, not a +formalized consequence of a finite test. The replay checks simple-system +positivity, 960 simple reflections and all 7,140 root planes. It reconstructs +root and label bytes independently of the predecessor's binary data tables, +then checks their equality to the declared input. + +A nonzero direction with support at most 72 has at least forty perpendicular +live roots. Their rational span cannot have rank at most six by the 36-line +bound. It therefore has rank seven and a one-dimensional rational kernel. +This also proves that a field-valued direction is a scalar multiple of a +rational vector, over any `K` of characteristic zero. The chamber-face counts +leave only a root direction or a Weyl transform of the D7 normal. + +The retained program constructs a reflection-closed inventory of 1,080 D7 +normal lines containing that chamber normal. Their live support histogram is +`70:128, 73:896, 76:56`. Thus the complete support-72 alphabet is contained in +120 root lines plus 128 eligible non-root lines. Those 128 normals have one +entry `+1` or `-1` in each coordinate pair, up to common sign. Explicit even +signed permutations preserving the deleted frame normalize each to +`a=(1,0,1,0,1,0,1,0)`. All 128 normalizations are checked. + +## Seven affine endpoints + +Choose small pieces of weights `3,4,6`, with support union `S` of size at most +`4+8+20=32`. Call the seven remaining weight-six pieces `q_0,...,q_6`. +Let `D=T intersect C`. The quotient `T/D` has dimension at most four. + +The small pieces and any one `q_i` have support union at most `32+20=52<53`. +Their quotient images are independent: a dependence would be a nonzero +codeword supported on fewer than 53 lines, since the original pieces are +independent. The quotient therefore has dimension exactly four. Modulo the +three small images, the seven remaining images are nonzero in a +one-dimensional quotient. Rescale the `q_i` to give them equal images there. +Subtract suitable small-piece combinations `s_i` and write + +``` +c_0=0, c_i=q_i-q_0-s_i in D, i=1,...,6. +``` + +The six codewords are independent by their distinct coefficients on +`q_1,...,q_6`. They give seven affinely independent vertices in `K^8`. +Every edge is supported on at most `32+20+20=72` lines, so its direction is +in the complete root/D7 alphabet. + +At any coordinate outside `S`, the endpoint evaluations differ from the +vertex evaluations by one common shift. For seven scalar values, every +common shift leaves at least + +``` +7 - maximum equality multiplicity +``` + +nonzero entries. Cancelling a largest equality class attains this minimum. +The seven endpoints permit at most `7*20=140` support incidences. Both +branches below require more. + +## Mixed root/D7 branch + +Translate and rescale a non-root edge to the segment `0,a`. Any other vertex +`x` has `x=s*u`, `a-x=t*v` for distinct allowed rays `u,v` and nonzero +coefficients. Solving `a=s*u+t*v` gives exactly 58 possible vertices. +The solution is rational even when initially sought over `K`, by an +invertible rational two-by-two coordinate minor. The compatibility graph +has 595 edges, testing whether each difference is an allowed ray. + +Five further vertices form a five-clique. The complete exact census gives + +| Rank with the anchor | Five-cliques | +|---|---:| +| 4 | 630 | +| 5 | 3,360 | +| 6 | 3,360 | + +Only rank six is admissible. For each of these 3,360 cases, sum the minimum +nonzero costs after removing the 32 largest live costs. This relaxes the +actual `S` and allows arbitrary coordinate shifts. The surviving-cost +histogram is + +``` +142:1344, 145:336, 146:336, 147:112, 148:448, 149:560, 150:224. +``` + +Thus the mixed branch requires at least 142 incidences. A separate program +uses Gram intersections, a two-plus-three clique join, fraction-free integer +elimination and frequency-based deletion. It obtains the same graph, ranks +and costs, without calling those primary algorithms. + +## Root-only A6 branch and its losing relaxation + +The root-plane lemma identifies the vertices with one scaled affine root +A6 simplex. Extend each star prefix by every root having the prescribed +inner products. Reflections perpendicular to the prefix fix it pointwise. +Retaining every orbit of this subgroup is complete, even if the subgroup +is smaller than the full stabilizer. The extension orbit sizes are +`240;56;27;16;10;6`, leaving one rank-six star. + +Evaluate its seven vertices on all 120 root lines. The minimum nonzero-cost +spectrum is + +``` +0:1, 1:21, 2:63, 3:35, total cost 252. +``` + +Arbitrary removal of eight frame lines and 32 small-support lines leaves +only 137, below the allowance 140. This is a losing control. A proof cannot +replace the small supports by forty arbitrary deletions. + +A Weyl transformation taking the star to its representative moves the +puncture to an orthogonal eight-line frame. It maps binary label flats to +flats of the same dimension. Indeed, a root reflection is an invertible +integral automorphism of the simple-root lattice; reduce its coordinates +modulo two and leave the leading one fixed. Canonical root signs do not +matter modulo two. The replay checks all 960 simple-reflection label +relations. We must retain the actual rank-six and rank-four support flats. + +## New weighted cover lemma + +Let `c` be the full120 A6 cost function above. For any orthogonal eight-line +frame `F`, binary six-flat `V`, binary four-flat `U`, and set `A` of at most +four root coordinates, + +``` +sum_{r outside F union Lambda(V) union Lambda(U) union A} c(r) >= 141. +``` + +This relaxes the weight-three support to four arbitrary coordinates. The +following finite argument proves the lemma. + +All 2,025 orthogonal frames are enumerated. Their cost histogram is +`14:210,16:735,17:630,19:420,21:30`, so a frame costs at most 21. +A four-flat contains at most eight odd labels, costing at most 24; `A` costs +at most twelve. Suppose the union removed cost at least 112. Then `V` must +have full cost at least `112-21-24-12=55`. + +The complete six-flat enumeration has maximum cost 60. Exactly 63 distinct +masks have cost at least 55: 35 cost 57, and 28 cost 60. For every one of +these masks and every frame, the prefix `B=F union Lambda(V)` has cost at +most 77. A prefix costing at most 75 is impossible, since adding `U` and +`A` removes at most another 36. The remaining prefixes are exactly + +``` +B cost 76: 4,620 pairs; B cost 77: 2,520 pairs. +``` + +For these prefixes, `U` outside `B` would need cost at least +`112-c(B)-12`, hence 24 or 23. A four-flat containing at most six cost-three +labels has cost at most `6*3+2*2=22`. Any relevant four-flat must therefore +contain at least seven of the 35 cost-three labels. Those seven labels span +four dimensions: a three-flat contains at most four odd labels. Four of +them are a basis, so enumerating all four-element subsets of the 35 labels +covers every possible relevant four-flat. + +This construction gives exactly 135 masks: thirty contain seven cost-three +labels and 105 contain eight. Every one is checked against every relevant +prefix, a total of 963,900 tests. Their maximum residual cost is twelve for +both prefix costs, strictly below the necessary 23 or 24. All other +four-flats cost at most 22 even before subtracting `B`. Thus no removed +cost reaches 112. Integrality gives removed cost at most 111 and surviving +cost at least `252-111=141`. + +The separate checker enumerates all 788,035 six-flats and all 3,309,747 +four-flats using forward-echelon annihilators, instead of the primary +reverse-echelon/high-label construction. It recovers the exact same 63 +and 135 masks and the complete six-flat weight histogram. Its frames are +the 2,025-element simple-reflection orbit of the fixed frame, not the +primary orthogonality-clique traversal. It checks every relevant pair and +reproduces both residual maxima. The shared root reconstruction and +Weyl-chamber dependency remain explicit. + +## Finish, overlap and limits + +The actual root-only supports lie inside the sets of the weighted lemma, +so at least 141 endpoint incidences remain outside the small support. The +mixed branch requires 142. Both exceed 140. This proves the statement over +all characteristic-zero fields. + +The original unmodified TWOSIDE program and a separate transcription +retain this profile among the original 69 `(6,4)` survivors. Every +weight-certified four-piece quotient basis has weights `3,4,6,6`. Its +best two-six-flat packing leaves twelve certified cuts and six rank-six +nonbasis pieces. PR3162's ten-cut theorem and PR3167's twelve-cut theorem +with a rank-four nonbasis anchor do not supply this exclusion by that +route. This is an applicability check, not a universal novelty proof. + +The first session candidate `2,4,6^8` was discarded as already covered by +PR3162 through basis `2,4,6,6`. The present result changes that candidate +and repairs two losing relaxations: forty arbitrary cuts give 137; retaining +only the frame and six-flat but allowing twelve arbitrary small coordinates +gives 139. Neither alone proves the exclusion. + +This is an author-checked mathematical exclusion with separately implemented +finite checks, not independent human or proof-kernel review. The standard +Weyl-chamber theorem, inherited root-plane argument and original decoder +reduction remain dependencies. Full C5, other profiles, `C(P112)>=64`, +physical realization and any improved multiplication exponent remain open +or unchanged. No physical costs are assumed to be zero. diff --git a/research/p112-a6-weighted-cover/README.md b/research/p112-a6-weighted-cover/README.md new file mode 100644 index 0000000000..b71f03f593 --- /dev/null +++ b/research/p112-a6-weighted-cover/README.md @@ -0,0 +1,94 @@ +# A weighted A6 cover excludes P112 `3,4,6^8` + +Nick Petalas. Apache-2.0. + +Ten independent P112 pieces with code-intersection dimension at least six +cannot have weight bounds `3,4,6^8`, over any characteristic-zero field. +This excludes one actual TWOSIDE `(6,4)` profile in DreamingOfClouds's +[PR3154](https://github.com/CrocSwap/integer-mult-bounds/pull/3154). +[PROOF.md](PROOF.md) gives the full statement and implication. + +``` +Seven weight-six endpoints allow 140 support incidences. +Mixed root/D7 edges require at least 142. +Root-only A6 edges: + forty arbitrary deletions give only 137, a losing control; + retaining the frame and six-flat alone still gives only 139; + retaining the actual four-flat as well gives at least 141. +Contradiction margin at least one. +``` + +The new weighted lemma retains a binary six-flat and four-flat, with the +rank-three support relaxed to four arbitrary coordinates. The replay covers +all 788,035 six-flats, all 2,025 orthogonal frames, and all relevant four-flats. +Only 63 high-cost six-flat masks and 135 four-flat masks survive the exact +threshold reductions. A separate program enumerates all 3,309,747 four-flats +instead of using that reduction and reconstructs frames by Weyl orbit rather +than orthogonality cliques. The mixed check covers 7,350 five-cliques, including +3,360 rank-six cases. [RESULT.json](RESULT.json) records complete counts, +witnesses and canonical hashes. + +This is an author-checked finite mathematical result, not independent human +or proof-kernel review. The programs share root reconstruction and the written +Weyl-chamber dependency. It does not close the whole cell, C5, `C(P112)>=64`, +supplier admission or a new kappa. The selected conditional kappa remains +`0.001672660197076918`. + +## Reproduce + +Python 3.12 or later, standard library only. From the repository root: + +```sh +RUN="$HOME/.cache/integer-mult-bounds-runs/p112-a6-weighted-cover-replay" +mkdir -p "$RUN" +TMPDIR="$RUN" python3.12 -B scripts/research_package.py \ + --package research/p112-a6-weighted-cover +``` + +Four registered commands run sequentially with 120-second limits. Expected +markers are `PASS_A6_WEIGHTED_COVER`, `PASS_INDEPENDENT_A6_MIXED`, +`PASS_INDEPENDENT_A6_WEIGHTED` and `Ran 16 tests ... OK`. +The tests run under optimization, so mathematical guards must remain active +without assertions. [CHECKS.json](CHECKS.json) records local checks and limits. + +`verify.py --output NEW_ABSOLUTE_PATH` writes a fresh external receipt and +refuses overwrite. Without that option it compares fresh evidence with the +committed receipt. It does not regenerate files in the checkout. Direct +Git-free replay needs this package and its sole declared input +`research/one-sided-six-multisets/data/data.txt`, at the same relative paths. +Generic provenance validation additionally requires the pinned Git objects. + +## Sources and overlap + +Base main is `997e6a9ca7b4f95d50e366f61412fd640d72a88a`, priority revision 6. +The concrete C5 handoff was taken before consulting the generic task card. +[TASK.json](TASK.json) records the changed scope from proof-assistant work +to an exact characteristic-zero lemma and the bounded candidate correction. + +DreamingOfClouds/PR3154 at `708f0ad8928c383de8294aea3c126e9461d2066d` +supplies TWOSIDE and the original filters. Nick Petalas/PR3176 at +`1111a074414c4d2be8b4e230133d873432780814` supplies the byte-identical +support-72 alphabet, rational graph and geometry routines. The retained +lineage includes PR3164/3175, DreamingOfClouds, joaqcoo's model and the +credited E8/P112 decoder sources. Frame traversal is adapted from PR3180; +the weighted A6 lemma and this five-clique application are new. +[SOURCES.json](SOURCES.json) binds exact heads, blobs and SHA256 hashes; +licenses and predecessor notices remain in `vendor/`. + +The initial candidate `2,4,6^8` was discarded because PR3162 already excludes +it. For the present `3,4,6^8` profile, the unique weight-certified quotient +basis `3,4,6,6` needs twelve cuts in the two-six-flat cover and leaves no +rank-four nonbasis anchor. The pinned ten-cut and twelve-cut-anchor theorems +do not close it by that route. Live overlap is advisory, not a novelty proof. + +No frozen input, shared implementation, research priority or selected result +changed. No Lean, Docker, physical caller or complete supplier replay was run. +[ENGINEERING.md](ENGINEERING.md) records implementation bounds and diagnostics. + +## Open next questions + +Does another actual remaining profile need this A6 cover lemma or a different +support contract? First pin that profile and prove its quotient dimension, +small-support and edge-alphabet hypotheses. The blocker is applicability, +not another seed. Do not infer a full C5 result or expand the census without +that decision. Structured relevance and a first step are in [TASK.json](TASK.json). diff --git a/research/p112-a6-weighted-cover/RESULT.json b/research/p112-a6-weighted-cover/RESULT.json new file mode 100644 index 0000000000..4d03638184 --- /dev/null +++ b/research/p112-a6-weighted-cover/RESULT.json @@ -0,0 +1,505 @@ +{ + "schema": "p112-a6-weighted-cover/v1", + "input_sha256": "ac4a48851b922f2a433684b60c74768ae3bb4fc5e8990ffe63e3942bb3c2ea34", + "alphabet": { + "root_lines": 120, + "D7_normal_lines": 1080, + "D7_support_histogram": { + "70": 128, + "73": 896, + "76": 56 + }, + "eligible_nonroots": 128, + "directions": 248, + "anchor_symmetries": 128 + }, + "graph": { + "vertices": 58, + "edges": 595, + "sha256": "f1930e07414b8cb2b7e1461b9bcb0e7e2440fd2f488f91b1c0b897b980a03acf" + }, + "mixed": { + "ranks": { + "4": 630, + "5": 3360, + "6": 3360 + }, + "bounds": { + "142": 1344, + "145": 336, + "146": 336, + "147": 112, + "148": 448, + "149": 560, + "150": 224 + }, + "witness": { + "lower": 142, + "indices": [ + 53, + 54, + 55, + 56, + 57 + ], + "spectrum": { + "0": 2, + "1": 26, + "2": 40, + "3": 26, + "4": 18 + } + } + }, + "all_root": { + "steps": [ + { + "rank": 0, + "orbit_sizes": [ + 240 + ] + }, + { + "rank": 1, + "orbit_sizes": [ + 56 + ] + }, + { + "rank": 2, + "orbit_sizes": [ + 27 + ] + }, + { + "rank": 3, + "orbit_sizes": [ + 16 + ] + }, + { + "rank": 4, + "orbit_sizes": [ + 10 + ] + }, + { + "rank": 5, + "orbit_sizes": [ + 6 + ] + } + ], + "spectrum": { + "0": 1, + "1": 21, + "2": 63, + "3": 35 + }, + "losing_after_40_cuts": 137, + "representative": [ + [ + -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 + ] + ] + }, + "application": { + "b": 6, + "t": 4, + "weights": [ + 3, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "original_survivors": 69, + "small_weights": [ + 3, + 4, + 6 + ], + "small_support_cap": 32, + "quotient_basis_cap": 52, + "edge_support_cap": 72, + "endpoints": 7, + "endpoint_support_cap": 140, + "mixed_lower": 142, + "all_root_lower": 141, + "margin": 1 + }, + "weighted": { + "six_flat_histogram": { + "0": 10795, + "12": 525, + "14": 378, + "15": 1050, + "16": 3780, + "17": 1890, + "18": 4578, + "19": 630, + "20": 1890, + "21": 12000, + "22": 19593, + "23": 27195, + "24": 32060, + "25": 28665, + "26": 57561, + "27": 58884, + "28": 22050, + "29": 13650, + "30": 26845, + "31": 15288, + "32": 72870, + "33": 98245, + "34": 34125, + "35": 44163, + "36": 75075, + "37": 23499, + "38": 12495, + "39": 12740, + "40": 5523, + "41": 11088, + "42": 27405, + "43": 14490, + "44": 3150, + "45": 4753, + "46": 4305, + "47": 2205, + "48": 350, + "49": 735, + "50": 819, + "51": 315, + "52": 315, + "57": 35, + "60": 28 + }, + "selected_six_flats": 63, + "high_four_flats": 135, + "mask_sha256": "30448edfd932d91f3c56b3590ee73b39db59ec85ce3a044a648b04f80374ff95", + "label_reflection_checks": 960, + "cover": { + "frame_costs": { + "14": 210, + "16": 735, + "17": 630, + "19": 420, + "21": 30 + }, + "prefix_costs": { + "76": 4620, + "77": 2520 + }, + "maximum_prefix": 77, + "four_flat_tests": 963900, + "residual_maxima": [ + [ + 76, + 12, + 4620 + ], + [ + 77, + 12, + 2520 + ] + ], + "removed_upper": 111, + "surviving_lower": 141, + "losing_arbitrary12_lower": 139, + "losing_witness": { + "frame": [ + 19, + 27, + 36, + 52, + 62, + 80, + 98, + 114 + ], + "six_mask": 156589743630174343786926178304 + } + } + }, + "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 + }, + "six_flat_capacity": { + "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 + } + }, + "original_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 + ] + ] +} diff --git a/research/p112-a6-weighted-cover/SOURCES.json b/research/p112-a6-weighted-cover/SOURCES.json new file mode 100644 index 0000000000..f1f748cc50 --- /dev/null +++ b/research/p112-a6-weighted-cover/SOURCES.json @@ -0,0 +1,172 @@ +{ + "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" + }, + { + "path": "research/p112-mixed-edge-simplex/vendor/geometry.py", + "usage": "provenance", + "pin": "head:1111a074414c4d2be8b4e230133d873432780814:research/p112-mixed-edge-simplex/vendor/geometry.py", + "git_blob": "222ea556faf2b275f73815c4e7d0d5f1e3294f2f", + "sha256": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021" + }, + { + "path": "research/p112-mixed-edge-simplex/vendor/ROOT-SIMPLEX-PROOF.md", + "usage": "provenance", + "pin": "head:1111a074414c4d2be8b4e230133d873432780814:research/p112-mixed-edge-simplex/vendor/ROOT-SIMPLEX-PROOF.md", + "git_blob": "ccae08212784114e732da1192b336e47fc6a2091", + "sha256": "2b5d70570e3a13d2ccc71c1fc7eef113f0d049993cb9bb24007166223ac7b734" + }, + { + "path": "research/p112-mixed-edge-simplex/vendor/TWOSIDE-NOTES.md", + "usage": "provenance", + "pin": "head:1111a074414c4d2be8b4e230133d873432780814:research/p112-mixed-edge-simplex/vendor/TWOSIDE-NOTES.md", + "git_blob": "e3fd3f2b1dfd77b597f000b38ec2dbec3dbca931", + "sha256": "226cd59ccc6bc065319e5e4c4768c889206169ff58f74ef4053eeadc5b2e03c8" + }, + { + "path": "research/p112-mixed-edge-simplex/vendor/bk2b.py", + "usage": "provenance", + "pin": "head:1111a074414c4d2be8b4e230133d873432780814:research/p112-mixed-edge-simplex/vendor/bk2b.py", + "git_blob": "3394029014bb13f16225587a153fa7b70016de6d", + "sha256": "dff16eff255c883db372a587cf3f34e6f35c08f75c60af9d11952be5a5838807" + }, + { + "path": "research/p112-mixed-edge-simplex/vendor/LICENSE", + "usage": "provenance", + "pin": "head:1111a074414c4d2be8b4e230133d873432780814:research/p112-mixed-edge-simplex/vendor/LICENSE", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "path": "research/p112-mixed-edge-simplex/vendor/PREDECESSOR-NOTICE.md", + "usage": "provenance", + "pin": "head:1111a074414c4d2be8b4e230133d873432780814:research/p112-mixed-edge-simplex/vendor/PREDECESSOR-NOTICE.md", + "git_blob": "c6f3494c2c746242020ed1b7959bc48988239d6d", + "sha256": "1ea58e398f40239c0945d495a807b33bcadeb6d5dcd147a12bf71ff06a9ed7ec" + }, + { + "path": "research/p112-mixed-edge-simplex/mixed.py", + "usage": "provenance", + "pin": "head:1111a074414c4d2be8b4e230133d873432780814:research/p112-mixed-edge-simplex/mixed.py", + "git_blob": "e79086db5cdd77aaa28602e649cf1ed21b34d759", + "sha256": "7edd4f7fee0db1b4d38e0b8d9fbd71448950045add9773dc8db4084d6550f11e" + }, + { + "path": "research/p112-reduction-to-conjectures/checks/TWOSIDE/bk2b.py", + "usage": "provenance", + "pin": "head:708f0ad8928c383de8294aea3c126e9461d2066d:research/p112-reduction-to-conjectures/checks/TWOSIDE/bk2b.py", + "git_blob": "3394029014bb13f16225587a153fa7b70016de6d", + "sha256": "dff16eff255c883db372a587cf3f34e6f35c08f75c60af9d11952be5a5838807" + }, + { + "path": "research/p112-reduction-to-conjectures/checks/TWOSIDE/NOTES.md", + "usage": "provenance", + "pin": "head:708f0ad8928c383de8294aea3c126e9461d2066d:research/p112-reduction-to-conjectures/checks/TWOSIDE/NOTES.md", + "git_blob": "e3fd3f2b1dfd77b597f000b38ec2dbec3dbca931", + "sha256": "226cd59ccc6bc065319e5e4c4768c889206169ff58f74ef4053eeadc5b2e03c8" + }, + { + "path": "research/p112-weighted-flat-pair/bound.py", + "usage": "provenance", + "pin": "head:595a78f7925c8802f764792098806ebfbff1f27a:research/p112-weighted-flat-pair/bound.py", + "git_blob": "2fc0f64b1f68dd129f25a43ea9a8159b32f3f61e", + "sha256": "592c2a42162fd8ad580939b4cefb7b60874e70844091ee2911551df2235e2186" + }, + { + "path": "research/p112-mixed-edge-simplex/independent.py", + "usage": "provenance", + "pin": "head:1111a074414c4d2be8b4e230133d873432780814:research/p112-mixed-edge-simplex/independent.py", + "git_blob": "0df0659d4e9ed5c8a4fd2acf95547d6316b66ca1", + "sha256": "7fec3685cb9f8e6436c10816b5ab2bff356d5a40cba57d40f91025e756bac08e" + } + ], + "retained_files": [ + { + "local_path": "vendor/geometry.py", + "source_commit": "1111a074414c4d2be8b4e230133d873432780814", + "source_path": "research/p112-mixed-edge-simplex/vendor/geometry.py", + "git_blob": "222ea556faf2b275f73815c4e7d0d5f1e3294f2f", + "sha256": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021" + }, + { + "local_path": "vendor/ROOT-SIMPLEX-PROOF.md", + "source_commit": "1111a074414c4d2be8b4e230133d873432780814", + "source_path": "research/p112-mixed-edge-simplex/vendor/ROOT-SIMPLEX-PROOF.md", + "git_blob": "ccae08212784114e732da1192b336e47fc6a2091", + "sha256": "2b5d70570e3a13d2ccc71c1fc7eef113f0d049993cb9bb24007166223ac7b734" + }, + { + "local_path": "vendor/TWOSIDE-NOTES.md", + "source_commit": "1111a074414c4d2be8b4e230133d873432780814", + "source_path": "research/p112-mixed-edge-simplex/vendor/TWOSIDE-NOTES.md", + "git_blob": "e3fd3f2b1dfd77b597f000b38ec2dbec3dbca931", + "sha256": "226cd59ccc6bc065319e5e4c4768c889206169ff58f74ef4053eeadc5b2e03c8" + }, + { + "local_path": "vendor/bk2b.py", + "source_commit": "1111a074414c4d2be8b4e230133d873432780814", + "source_path": "research/p112-mixed-edge-simplex/vendor/bk2b.py", + "git_blob": "3394029014bb13f16225587a153fa7b70016de6d", + "sha256": "dff16eff255c883db372a587cf3f34e6f35c08f75c60af9d11952be5a5838807" + }, + { + "local_path": "vendor/LICENSE", + "source_commit": "1111a074414c4d2be8b4e230133d873432780814", + "source_path": "research/p112-mixed-edge-simplex/vendor/LICENSE", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "local_path": "vendor/PREDECESSOR-NOTICE.md", + "source_commit": "1111a074414c4d2be8b4e230133d873432780814", + "source_path": "research/p112-mixed-edge-simplex/vendor/PREDECESSOR-NOTICE.md", + "git_blob": "c6f3494c2c746242020ed1b7959bc48988239d6d", + "sha256": "1ea58e398f40239c0945d495a807b33bcadeb6d5dcd147a12bf71ff06a9ed7ec" + }, + { + "local_path": "vendor/mixed.py", + "source_commit": "1111a074414c4d2be8b4e230133d873432780814", + "source_path": "research/p112-mixed-edge-simplex/mixed.py", + "git_blob": "e79086db5cdd77aaa28602e649cf1ed21b34d759", + "sha256": "7edd4f7fee0db1b4d38e0b8d9fbd71448950045add9773dc8db4084d6550f11e" + } + ], + "predecessors": [ + { + "pr": 3154, + "author": "DreamingOfClouds", + "head": "708f0ad8928c383de8294aea3c126e9461d2066d", + "role": "TWOSIDE reduction and original filters" + }, + { + "pr": 3176, + "author": "Nick Petalas", + "head": "1111a074414c4d2be8b4e230133d873432780814", + "role": "retained E8/P112 geometry and support-72 mixed-edge alphabet, following PR3164/3175 and credited decoder lineage" + }, + { + "pr": 3180, + "author": "Nick Petalas", + "head": "595a78f7925c8802f764792098806ebfbff1f27a", + "role": "frame traversal adapted, not a mathematical dependency on the weighted A7 result" + } + ] +} diff --git a/research/p112-a6-weighted-cover/TASK.json b/research/p112-a6-weighted-cover/TASK.json new file mode 100644 index 0000000000..31bcc5cbce --- /dev/null +++ b/research/p112-a6-weighted-cover/TASK.json @@ -0,0 +1,76 @@ +{ + "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 exclusion of the actual P112 TWOSIDE (6,4) profile 3,4,6^8 by a new A6 weighted frame/six-flat/four-flat cover lemma and a complete five-clique mixed-edge check.", + "scope_change_reason": "Took Discussion3156's concrete C5 handoff before the generic task card. This is an exact mathematical lemma with finite checks, not a Lean formalization or a selected-supplier interface admission. The first candidate 2,4,6^8 was discarded as already implied by PR3162; one bounded pivot retained 3,4,6^8, whose old cover needs twelve cuts without a rank-four nonbasis anchor.", + "bottleneck_link": "Removes one actual low-cost piece profile in the pending P112 decoder-floor reduction. It repairs the losing arbitrary-deletion root-A6 bound without asserting the whole C5 conjecture, a new supplier or a kappa improvement.", + "budget_minutes": 60, + "stop_rule": "Finish this one checked exclusion, stop at a failed quotient or coverage premise, or stop at the approximately 60-minute session budget. Do not extend the census without another actual-profile applicability decision.", + "outcome": "completed", + "evidence": "PROOF.md and RESULT.json. Complete primary exact replay; separate Gram/split-clique/integer-rank census; separate forward-echelon full six/four-flat census and Weyl frame orbit; optimized behavioral controls. Author-checked, not independent human or proof-kernel review.", + "author": "Nick Petalas", + "ai_assistance": "Substantial automated assistance in analysis, implementation and local checking; independent human review remains outstanding.", + "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/3156", + "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/3156#discussioncomment-19000400", + "milestone": "local mathematical exclusion, not supplier admission", + "family_expansion_decision": "narrow: finish one actual profile; no new dependent search or supplier implementation", + "initial_checkpoint": { + "canonical_main": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "priority_revision": 6, + "checked_at": "2026-10-17T15:25:33Z", + "overlap_coverage": "302 open PRs and 1966 discussion records, complete pagination; no code-diff or universal novelty coverage" + }, + "submission_checkpoint": { + "canonical_main": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "priority_revision": 6, + "checked_at": "2026-10-17T15:34:06Z", + "overlap_coverage": "304 open PRs and 1967 discussion records, complete pagination with no warnings. Concurrent PR3185 proves a different cover-floor statement and does not claim this profile exclusion; PR3169 and the earlier ten-cut/anchor results were checked for applicability." + }, + "open_questions": [ + { + "question": "Does another actual remaining TWOSIDE profile need this weighted A6 lemma or a changed support contract?", + "why_it_matters": "A new applicability argument can remove a concrete remaining decoder-floor case; another unbound census does not establish progress toward C5.", + "first_step": "Pin one still-open profile and derive its quotient dimension, small-support union, endpoint allowance and full edge alphabet before extending the certificate.", + "blocked_by": "No additional profile applicability or full C5 reduction is proved by this package; standard Weyl-chamber and original decoder-reduction dependencies remain." + } + ] +} diff --git a/research/p112-a6-weighted-cover/VERIFY.json b/research/p112-a6-weighted-cover/VERIFY.json new file mode 100644 index 0000000000..ecf1549070 --- /dev/null +++ b/research/p112-a6-weighted-cover/VERIFY.json @@ -0,0 +1,31 @@ +{ + "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 source/data binding, six-flat capacity, complete mixed and weighted A6 cover census, original TWOSIDE inclusion and receipt equality" + }, + { + "argv": ["{python}", "-B", "{package}/independent.py"], + "timeout_seconds": 120, + "checks": "Separate Gram intersections, 2+3 clique join, integer rank and frequency-deletion census" + }, + { + "argv": ["{python}", "-B", "{package}/independent_weighted.py"], + "timeout_seconds": 120, + "checks": "Forward-echelon exhaustive six/four-flat reconstruction, complete Weyl frame orbit, weighted-cover equality" + }, + { + "argv": ["{python}", "-B", "-O", "{package}/test_verify.py"], + "timeout_seconds": 120, + "checks": "Sixteen mathematical boundary, source-corruption, inventory, semantic, output and optimization controls" + } + ] +} diff --git a/research/p112-a6-weighted-cover/bound.py b/research/p112-a6-weighted-cover/bound.py new file mode 100644 index 0000000000..14b05de535 --- /dev/null +++ b/research/p112-a6-weighted-cover/bound.py @@ -0,0 +1,115 @@ +"""Seven-endpoint exclusion for the actual P112 3,4,6^8 profile. + +Nick Petalas. Apache-2.0. Geometry and mixed-edge routines retain PR3176's +exact source; this five-clique application and its support budget are new. +""" + +from collections import Counter +from itertools import combinations_with_replacement, product + +from vendor.geometry import dot, require +from vendor.mixed import ANCHOR, CAP, cliques, rational_rank, root_extensions + +PROFILE = (3, 4) + (6,) * 8 + + +def support_lower(costs, removed): + require(len(costs) in (112, 120), "support inventory size") + require(type(removed) is int and 0 <= removed <= len(costs), "deletion budget") + require(all(type(c) is int and 0 <= c <= 6 for c in costs), "support costs") + return sum(sorted(costs)[:len(costs) - removed]) + + +def mixed_six(vertices, adjacency, points): + anchor = tuple(2 * x for x in ANCHOR) + evaluations = tuple( + (0, dot(p, anchor), *(dot(p, v) for v in vertices)) for p in points + ) + ranks, bounds = Counter(), Counter() + witness = None + for chosen in cliques(adjacency, 5): + rank = rational_rank((anchor, *(vertices[i] for i in chosen))) + ranks[rank] += 1 + if rank != 6: + continue + costs = [ + 7 - max(Counter(row[:2] + tuple(row[i + 2] for i in chosen)).values()) + for row in evaluations + ] + lower = support_lower(costs, 32) + bounds[lower] += 1 + if witness is None or lower < witness["lower"]: + witness = {"lower": lower, "indices": chosen, + "spectrum": dict(sorted(Counter(costs).items()))} + require(ranks == {4: 630, 5: 3360, 6: 3360}, "five-clique rank census") + require(bounds == {142: 1344, 145: 336, 146: 336, 147: 112, + 148: 448, 149: 560, 150: 224}, "mixed support census") + require(witness is not None and witness["lower"] == 142, "minimum witness") + return {"ranks": dict(sorted(ranks.items())), + "bounds": dict(sorted(bounds.items())), "witness": witness} + + +def all_root_six(roots): + level, steps = [()], [] + for rank in range(6): + following = [] + for prefix in level: + representatives, sizes = root_extensions(prefix, roots) + steps.append({"rank": rank, "orbit_sizes": sizes}) + following.extend((*prefix, v) for v in representatives) + level = following + require(len(level) == 1, "root A6 branch count") + costs = tuple( + 7 - max(Counter((0, *(dot(r, v) for v in level[0]))).values()) + for r in roots + ) + require(Counter(costs) == {0: 1, 1: 21, 2: 63, 3: 35}, "A6 spectrum") + losing = support_lower(costs, 40) + require(losing == 137, "A6 arbitrary-deletion losing control") + return {"steps": steps, "spectrum": dict(sorted(Counter(costs).items())), + "losing_after_40_cuts": losing, "representative": level[0]} + + +def original_survivors(): + """Independent transcription of the pinned filter, only for (b,t)=(6,4).""" + distance = (0, 53, 78, 92, 100, 106, 109) + rows = [] + for size in range(6, 11): + for weights in combinations_with_replacement(range(2, 8), size): + if sum(w - 2 for w in weights) >= 36: + continue + feasible = True + for level in range(1, 7): + prefix = weights[:size - 6 + level] + total = sum(CAP[w] for w in prefix) + target = sum(32 if w == 7 else CAP[w] for w in prefix) + if ((level == 1 and target < 53 and total < 73) + or (level == 2 and target < 78 and total < 82) + or (level >= 3 and total < distance[level])): + feasible = False + break + basis = weights[:size - 6] + killed = False + if sum(CAP[w] for w in basis) < 53: + killed = sum(basis) <= 7 or any( + all(sum(w for w, g in zip(basis, assignment, strict=True) + if g == group) <= 6 for group in (0, 1)) + for assignment in product(range(2), repeat=len(basis)) + ) + if feasible and not killed: + rows.append(weights) + require(len(rows) == 69 and PROFILE in rows, "original (6,4) residue changed") + return rows + + +def application(): + rows = original_survivors() + small = (3, 4, 6) + support = sum(CAP[w] for w in small) + require(support == 32 and support + 20 < 53, "quotient basis budget") + require(support + 40 == 72, "edge alphabet boundary") + return {"b": 6, "t": 4, "weights": PROFILE, "original_survivors": len(rows), + "small_weights": small, "small_support_cap": support, + "quotient_basis_cap": support + 20, "edge_support_cap": 72, + "endpoints": 7, "endpoint_support_cap": 140, + "mixed_lower": 142, "all_root_lower": 141, "margin": 1} diff --git a/research/p112-a6-weighted-cover/independent.py b/research/p112-a6-weighted-cover/independent.py new file mode 100644 index 0000000000..c22a4ae258 --- /dev/null +++ b/research/p112-a6-weighted-cover/independent.py @@ -0,0 +1,172 @@ +"""Separate Gram-intersection, 2+3 clique, integer-rank and support check. + +Adapted from Nick Petalas's PR3176 independent checker. It shares root +reconstruction and source binding, but not the primary graph, clique, rank, +or coordinate-multiplicity algorithms. Apache-2.0. +""" + +import json +from collections import Counter +from fractions import Fraction +from itertools import combinations, product +from math import gcd + +from vendor.geometry import frame_lines, require, root_lines +from verify import PACKAGE, bind_sources, graph_digest, read_bytes + +A = (1, 0, 1, 0, 1, 0, 1, 0) + + +def line(row): + divisor = gcd(*row) + require(divisor != 0, "zero projective line") + values = tuple(x // divisor for x in row) + return values if next(x for x in values if x) > 0 else tuple(-x for x in values) + + +def inner(u, v): + return sum(u[i] * v[i] for i in range(8)) + + +def direction_inventory(): + extra = { + line(tuple(signs[i // 2] if i % 2 == choices[i // 2] else 0 for i in range(8))) + for choices in product(range(2), repeat=4) + for signs in product((-1, 1), repeat=4) + } + directions = tuple(sorted({line(r) for r in root_lines()} | extra)) + require(len(extra) == 128 and len(directions) == 248, "independent alphabet") + return directions + + +def gram_vertices(directions): + require(len(directions) == len(set(directions)) == 248, "Gram alphabet inventory") + vertices = set() + for u, v in combinations(directions, 2): + uu, uv, vv = inner(u, u), inner(u, v), inner(v, v) + ua, va = inner(u, A), inner(v, A) + determinant = uu * vv - uv * uv + require(determinant > 0, "parallel alphabet rays") + s = Fraction(ua * vv - va * uv, determinant) + t = Fraction(va * uu - ua * uv, determinant) + if s and t and all(s * u[i] + t * v[i] == A[i] for i in range(8)): + for coefficient, direction in ((s, u), (t, v)): + doubled = tuple(2 * coefficient * x for x in direction) + require(all(x.denominator == 1 for x in doubled), "non-half-integral point") + vertices.add(tuple(int(x) for x in doubled)) + require(len(vertices) == 58, "independent anchored vertices") + return tuple(sorted(vertices)) + + +def graph(vertices, directions): + require(len(vertices) == 58 and len(directions) == 248, "graph inventory") + allowed = set(directions) + adjacency = [0] * 58 + for i, j in combinations(range(58), 2): + if line(tuple(vertices[i][k] - vertices[j][k] for k in range(8))) in allowed: + adjacency[i] += 1 << j + adjacency[j] += 1 << i + require(sum(row.bit_count() for row in adjacency) == 1190, "independent edge count") + return tuple(adjacency) + + +def split_cliques(adjacency): + require(len(adjacency) == 58, "clique graph dimension") + pairs = [ij for ij in combinations(range(58), 2) if adjacency[ij[0]] >> ij[1] & 1] + triples = [ijk for ijk in combinations(range(58), 3) + if all(adjacency[i] >> j & 1 for i, j in combinations(ijk, 2))] + require(len(pairs) == 595 and len(triples) == 2114, "2/3 clique inventory") + masks = [(indices, sum(1 << i for i in indices)) for indices in triples] + result = [] + for pair in pairs: + common = adjacency[pair[0]] & adjacency[pair[1]] + for triple, mask in masks: + if pair[-1] < triple[0] and mask & common == mask: + result.append(pair + triple) + require(len(result) == len(set(result)) == 7350, "2+3 clique coverage") + return result + + +def integer_rank(rows): + size = len(rows) + require(1 <= size <= 8 and all(len(row) == 8 for row in rows), "rank dimensions") + matrix = [list(row) for row in rows] + rank = 0 + for column in range(8): + selected = next((i for i in range(rank, size) if matrix[i][column]), None) + if selected is None: + continue + matrix[rank], matrix[selected] = matrix[selected], matrix[rank] + for i in range(rank + 1, size): + if matrix[i][column]: + a, b = matrix[rank][column], matrix[i][column] + matrix[i] = [a * x - b * y + for x, y in zip(matrix[i], matrix[rank], strict=True)] + divisor = gcd(*matrix[i]) + if divisor: + matrix[i] = [x // divisor for x in matrix[i]] + require(all(abs(x) < 1 << 128 for x in matrix[i]), "integer rank capacity") + rank += 1 + return rank + + +def census(vertices, adjacency): + points = tuple(r for r in root_lines() if r not in frame_lines()) + anchor = tuple(2 * x for x in A) + ranks, bounds = Counter(), Counter() + for indices in split_cliques(adjacency): + rows = (anchor, *(vertices[i] for i in indices)) + rank = integer_rank(rows) + ranks[rank] += 1 + if rank != 6: + continue + costs = [] + for point in points: + values = [0] + [inner(point, row) for row in rows] + costs.append(7 - max(values.count(x) for x in values)) + # Remove the 32 largest entries without the primary sorting routine. + remaining, removed = Counter(costs), 32 + for cost in range(6, -1, -1): + take = min(remaining[cost], removed) + remaining[cost] -= take + removed -= take + require(removed == 0, "deletion capacity exhausted") + bounds[sum(cost * count for cost, count in remaining.items())] += 1 + return dict(sorted(ranks.items())), dict(sorted(bounds.items())) + + +def root_fixture(): + roots = root_lines() + star = tuple(tuple(2 * (j == i) - 2 * (j == 7) for j in range(8)) for i in range(6)) + require(all(line(v) in {line(r) for r in roots} for v in star), "fixture root membership") + require(integer_rank(star) == 6, "fixture rank") + require(all(inner(a, b) == 4 for a, b in combinations(star, 2)), "fixture root star") + costs = [] + for root in roots: + values = [0] + [inner(root, v) for v in star] + costs.append(7 - max(values.count(v) for v in values)) + require(Counter(costs) == {0: 1, 1: 21, 2: 63, 3: 35}, "independent A6 spectrum") + require(sum(costs) - 35 * 3 - 5 * 2 == 137, "independent A6 losing control") + return dict(sorted(Counter(costs).items())) + + +def main(): + bind_sources() + expected = json.loads(read_bytes(PACKAGE / "RESULT.json")) + directions = direction_inventory() + vertices = gram_vertices(directions) + adjacency = graph(vertices, directions) + require(graph_digest(vertices, adjacency) == expected["graph"]["sha256"], + "independent graph differs") + ranks, bounds = census(vertices, adjacency) + require({str(k): v for k, v in ranks.items()} == expected["mixed"]["ranks"], + "independent exact ranks differ") + require({str(k): v for k, v in bounds.items()} == expected["mixed"]["bounds"], + "independent support histogram differs") + require({str(k): v for k, v in root_fixture().items()} == expected["all_root"]["spectrum"], + "independent root spectrum differs") + print("PASS_INDEPENDENT_A6_MIXED cliques=7350 rank6=3360 mixed=142") + + +if __name__ == "__main__": + main() diff --git a/research/p112-a6-weighted-cover/independent_weighted.py b/research/p112-a6-weighted-cover/independent_weighted.py new file mode 100644 index 0000000000..9680d041ee --- /dev/null +++ b/research/p112-a6-weighted-cover/independent_weighted.py @@ -0,0 +1,137 @@ +"""Separate forward-echelon flat and Weyl-orbit frame cover replay. + +The primary code uses reverse-echelon annihilators, root-generated four-flats +and an orthogonality-clique frame traversal. This program imports none of +those algorithms. Root/label reconstruction and source binding are shared. +""" + +import hashlib +import json +from collections import Counter +from itertools import combinations, product + +from independent import inner +from vendor.geometry import SIMPLE, canonical, frame_lines, require, root_data +from verify import PACKAGE, bind_sources, read_bytes + +ALL = (1 << 120) - 1 + + +def flat_masks(labels, dimension): + require(len(labels) == 120 and dimension in (4, 6), "forward-flat domain") + kernels = [sum(1 << i for i, label in enumerate(labels) + if not ((label & vector).bit_count() % 2)) for vector in range(512)] + dual_dimension = 9 - dimension + count = 0 + for pivots in combinations(range(9), dual_dimension): + rows = [] + for pivot in pivots: + free = [i for i in range(pivot + 1, 9) if i not in pivots] + rows.append([kernels[(1 << pivot) + sum(((code >> j) & 1) << i + for j, i in enumerate(free))] + for code in range(1 << len(free))]) + for chosen in product(*rows): + mask = ALL + for kernel in chosen: + mask &= kernel + count += 1 + yield mask + require(count == {4: 3309747, 6: 788035}[dimension], "forward-flat coverage") + + +def frame_orbit(roots): + index = {r: i for i, r in enumerate(roots)} + permutations = [] + for simple in SIMPLE: + permutation = [] + for root in roots: + factor = inner(root, simple) // 4 + image = canonical(tuple(root[i] - factor * simple[i] for i in range(8))) + permutation.append(index[image]) + require(len(set(permutation)) == 120, "frame reflection permutation") + permutations.append(tuple(permutation)) + first = tuple(sorted(index[r] for r in frame_lines())) + queue, seen = [first], {first} + for i in range(2025): + require(i < len(queue), "frame orbit stopped early") + for permutation in permutations: + image = tuple(sorted(permutation[j] for j in queue[i])) + if image not in seen: + seen.add(image) + queue.append(image) + require(len(queue) <= 2025, "frame orbit capacity") + require(len(queue) == len(seen) == 2025, "complete frame orbit") + require(all(all(inner(roots[i], roots[j]) == 0 for i, j in combinations(frame, 2)) + for frame in queue), "nonorthogonal orbit frame") + return tuple(sorted(seen)) + + +def inventories(labels, costs): + exact = tuple(sum(1 << i for i, c in enumerate(costs) if c == j) for j in range(4)) + six, four, histogram = set(), set(), Counter() + for mask in flat_masks(labels, 6): + cost = sum(j * (mask & exact[j]).bit_count() for j in range(1, 4)) + histogram[cost] += 1 + if cost >= 55: + six.add(mask) + for mask in flat_masks(labels, 4): + if (mask & exact[3]).bit_count() >= 7: + four.add(mask) + require(len(six) == 63 and len(four) == 135, "independent weighted inventories") + return tuple(sorted(six)), tuple(sorted(four)), dict(sorted(histogram.items())), exact + + +def cover(frames, six, four, exact): + def cost(mask): + return sum(j * (mask & exact[j]).bit_count() for j in range(1, 4)) + + frame_histogram, prefix_histogram, maxima = Counter(), Counter(), Counter() + maximum_prefix = 0 + for frame in frames: + frame_mask = sum(1 << i for i in frame) + frame_histogram[cost(frame_mask)] += 1 + for flat in six: + removed = frame_mask | flat + prefix = cost(removed) + maximum_prefix = max(maximum_prefix, prefix) + if prefix >= 76: + prefix_histogram[prefix] += 1 + maximum = max(cost(candidate & ~removed) for candidate in four) + require(prefix + max(22, maximum) + 12 < 112, + "independent cover reaches threshold") + maxima[prefix, maximum] += 1 + require(maximum_prefix == 77, "independent prefix maximum") + return {"frame_costs": dict(sorted(frame_histogram.items())), + "prefix_costs": dict(sorted(prefix_histogram.items())), + "residual_maxima": [[a, b, n] for (a, b), n in sorted(maxima.items())]} + + +def main(): + bind_sources() + expected = json.loads(read_bytes(PACKAGE / "RESULT.json"))["weighted"] + roots, _, _, coordinates = root_data() + # Match the canonical A6 star using an explicit fixture, not a stabilizer traversal. + star = tuple(tuple(-2 * (j == 0) - 2 * (j == i) for j in range(8)) + for i in range(1, 7)) + costs = [] + for root in roots: + values = [0] + [inner(root, v) for v in star] + costs.append(7 - max(values.count(value) for value in values)) + labels = tuple(1 + sum((int(x) & 1) << (j + 1) for j, x in enumerate(row)) + for row in coordinates) + require(Counter(costs) == {0: 1, 1: 21, 2: 63, 3: 35}, "independent A6 costs") + six, four, histogram, exact = inventories(labels, costs) + raw = json.dumps({"six": six, "four": four}, separators=(",", ":")).encode() + require(hashlib.sha256(raw).hexdigest() == expected["mask_sha256"], + "independent flat masks differ") + require({str(k): v for k, v in histogram.items()} == expected["six_flat_histogram"], + "independent full weighted census differs") + actual = cover(frame_orbit(roots), six, four, exact) + for key, value in actual.items(): + require(json.dumps(value, sort_keys=True) == json.dumps(expected["cover"][key], sort_keys=True), + "independent weighted cover differs: " + key) + print("PASS_INDEPENDENT_A6_WEIGHTED six_flats=788035 four_flats=3309747 frames=2025 lower=141") + + +if __name__ == "__main__": + main() diff --git a/research/p112-a6-weighted-cover/test_verify.py b/research/p112-a6-weighted-cover/test_verify.py new file mode 100644 index 0000000000..3229a2d058 --- /dev/null +++ b/research/p112-a6-weighted-cover/test_verify.py @@ -0,0 +1,215 @@ +"""Behavioral and corruption controls; run with Python optimization enabled.""" + +import copy +import hashlib +import json +import os +import tempfile +import unittest +from collections import Counter +from itertools import combinations, product +from pathlib import Path + +import bound +import independent +import independent_weighted +import verify +import weighted +from vendor.geometry import dot, root_data +from vendor.mixed import ( + ANCHOR, + alphabet, + cliques, + compatibility, + intersections, + rational_rank, +) + + +class Controls(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.roots, cls.points, cls.labels, cls.coordinates = root_data() + cls.directions, _, _ = alphabet(cls.roots, cls.points) + cls.vertices = intersections(cls.directions) + cls.adjacency = compatibility(cls.vertices, cls.directions) + cls.root_result = bound.all_root_six(cls.roots) + star = cls.root_result["representative"] + cls.costs = tuple(7 - max(Counter((0, *(dot(r, v) for v in star))).values()) + for r in cls.roots) + cls.layers = weighted.cost_layers(cls.costs) + cls.full_labels = weighted.full_labels(cls.coordinates) + cls.six, _ = weighted.selected_six_flats(cls.full_labels, cls.layers) + cls.four = weighted.high_four_flats(cls.full_labels, cls.layers) + cls.frames = weighted.frame_inventory(cls.roots) + cls.sources = verify.bind_sources() + + def test_literal_source_translation(self): + digest = verify.bind_data(verify.ROOT / verify.DATA, self.points, self.labels, self.sources) + self.assertEqual(digest, "ac4a48851b922f2a433684b60c74768ae3bb4fc5e8990ffe63e3942bb3c2ea34") + self.assertEqual(weighted.label_reflections(self.roots, self.full_labels), 960) + + def test_actual_profile_and_old_cover_boundary(self): + result = bound.application() + self.assertEqual(result["weights"], (3, 4) + (6,) * 8) + self.assertEqual(result["original_survivors"], 69) + bases = {basis for basis in combinations(bound.PROFILE, 4) + if sum(bound.CAP[w] for w in basis) < 53} + self.assertEqual(bases, {(3, 4, 6, 6)}) + basis = (3, 4, 6, 6) + cuts = [sum(bound.CAP[w] for w, g in zip(basis, assignment, strict=True) if g == 2) + for assignment in product(range(3), repeat=4) + if all(sum(w for w, g in zip(basis, assignment, strict=True) if g == group) <= 6 + for group in (0, 1))] + self.assertEqual(min(cuts), 12) + nonbasis = list(bound.PROFILE) + for weight in basis: + nonbasis.remove(weight) + self.assertEqual(nonbasis, [6] * 6) + + def test_alphabet_truncation_is_rejected(self): + with self.assertRaises(ValueError): + intersections(self.directions[:-1]) + with self.assertRaises(ValueError): + alphabet(self.roots[:-1], self.points) + + def test_independent_intersections_and_graph(self): + directions = independent.direction_inventory() + vertices = independent.gram_vertices(directions) + self.assertEqual(vertices, self.vertices) + self.assertEqual(independent.graph(vertices, directions), self.adjacency) + with self.assertRaises(ValueError): + independent.gram_vertices(directions[:-1]) + + def test_complete_clique_sets_agree(self): + primary = set(cliques(self.adjacency, 5)) + alternate = set(independent.split_cliques(self.adjacency)) + self.assertEqual(primary, alternate) + self.assertEqual(len(primary), 7350) + with self.assertRaises(ValueError): + list(cliques(self.adjacency, 8)) + + def test_exact_rank_and_minimum_witness(self): + receipt = json.loads(verify.read_bytes(verify.PACKAGE / "RESULT.json")) + indices = receipt["mixed"]["witness"]["indices"] + anchor = tuple(2 * x for x in ANCHOR) + rows = (anchor, *(self.vertices[i] for i in indices)) + self.assertEqual(rational_rank(rows), 6) + self.assertEqual(independent.integer_rank(rows), 6) + self.assertEqual(independent.integer_rank((*rows[:5], rows[0])), 5) + costs = [] + for root in self.points: + values = [0] + [dot(root, row) for row in rows] + costs.append(7 - max(values.count(value) for value in values)) + self.assertEqual(bound.support_lower(costs, 32), 142) + self.assertEqual(bound.support_lower(costs, 33), 139) + + def test_common_shift_minimum(self): + for values in product((-1, 0, 1), repeat=7): + actual = min(sum(value + shift != 0 for value in values) for shift in (-1, 0, 1)) + self.assertEqual(actual, 7 - max(Counter(values).values())) + + def test_root_arbitrary_cut_loses(self): + self.assertEqual(self.root_result["losing_after_40_cuts"], 137) + self.assertEqual(independent.root_fixture(), self.root_result["spectrum"]) + self.assertEqual(bound.support_lower(self.costs, 38), 141) + with self.assertRaises(ValueError): + bound.support_lower(self.costs, 121) + + def test_high_four_flat_coverage(self): + exhaustive = {mask for mask in independent_weighted.flat_masks(self.full_labels, 4) + if (mask & self.layers[2]).bit_count() >= 7} + self.assertEqual(exhaustive, set(self.four)) + self.assertEqual(len(exhaustive), 135) + self.assertEqual(max(mask.bit_count() for mask in exhaustive), 8) + + def test_frame_orbit_is_complete(self): + self.assertEqual(set(independent_weighted.frame_orbit(self.roots)), set(self.frames)) + self.assertEqual(len(self.frames), 2025) + + def test_weighted_cover_and_oversized_flat_control(self): + result = weighted.cover_pairs(self.frames, self.six, self.four, self.layers) + self.assertEqual(result["surviving_lower"], 141) + with self.assertRaises(ValueError): + weighted.cover_pairs(self.frames, (weighted.ALL, *self.six[1:]), self.four, self.layers) + with self.assertRaises(ValueError): + weighted.cover_pairs(self.frames, self.six, (weighted.ALL, *self.four[1:]), self.layers) + with self.assertRaises(ValueError): + weighted.cover_pairs(self.frames[:-1], self.six, self.four, self.layers) + + def test_retaining_only_the_six_flat_still_loses(self): + result = json.loads(verify.read_bytes(verify.PACKAGE / "RESULT.json")) + witness = result["weighted"]["cover"]["losing_witness"] + self.assertIn(tuple(witness["frame"]), self.frames) + self.assertIn(witness["six_mask"], self.six) + prefix = witness["six_mask"] | sum(1 << i for i in witness["frame"]) + costs = sorted(c for i, c in enumerate(self.costs) if not (prefix >> i & 1)) + self.assertEqual(sum(costs[:-12]), 139) + self.assertEqual(weighted.arbitrary_extra(prefix, self.layers, 12), sum(costs[-12:])) + with self.assertRaises(ValueError): + weighted.arbitrary_extra(prefix, self.layers, -1) + + def test_source_corruption_is_rejected(self): + with tempfile.TemporaryDirectory(dir=os.environ.get("TMPDIR")) as directory: + package = Path(directory) + (package / "vendor").mkdir() + manifest = copy.deepcopy(self.sources) + for row in manifest["retained_files"]: + (package / row["local_path"]).write_bytes( + verify.read_bytes(verify.PACKAGE / row["local_path"])) + (package / "SOURCES.json").write_text(json.dumps(manifest), encoding="utf-8") + verify.bind_sources(package) + (package / "vendor/geometry.py").write_text("changed\n", encoding="utf-8") + with self.assertRaises(ValueError): + verify.bind_sources(package) + manifest["retained_files"][0]["local_path"] = "../geometry.py" + (package / "SOURCES.json").write_text(json.dumps(manifest), encoding="utf-8") + with self.assertRaises(ValueError): + verify.bind_sources(package) + + def test_input_hash_and_semantic_controls(self): + with tempfile.TemporaryDirectory(dir=os.environ.get("TMPDIR")) as directory: + path = Path(directory) / "data.txt" + raw = verify.read_bytes(verify.ROOT / verify.DATA) + lines = raw.decode("utf-8").splitlines() + labels = lines[0].split() + labels[0], labels[1] = labels[1], labels[0] + lines[0] = " ".join(labels) + path.write_text("\n".join(lines) + "\n", encoding="utf-8") + with self.assertRaises(ValueError): + verify.bind_data(path, self.points, self.labels, self.sources) + sources = copy.deepcopy(self.sources) + for row in sources["files"]: + if row["usage"] == "input": + row["sha256"] = hashlib.sha256(path.read_bytes()).hexdigest() + with self.assertRaises(ValueError): + verify.bind_data(path, self.points, self.labels, sources) + + def test_symlink_and_output_guards(self): + with tempfile.TemporaryDirectory(dir=os.environ.get("TMPDIR")) as directory: + root = Path(directory) + target = root / "target" + target.mkdir() + (target / "data").write_bytes(b"data") + (root / "alias").symlink_to(target, target_is_directory=True) + with self.assertRaises(ValueError): + verify.read_bytes(root / "alias/data") + output = root / "receipt.json" + verify.publish_receipt({"ok": True}, output) + with self.assertRaises(FileExistsError): + verify.publish_receipt({"ok": False}, output) + self.assertEqual(json.loads(output.read_text()), {"ok": True}) + with self.assertRaises(ValueError): + verify.publish_receipt({}, verify.PACKAGE / "not-written.json") + + def test_changed_receipt_is_rejected(self): + result = json.loads(verify.read_bytes(verify.PACKAGE / "RESULT.json")) + changed = copy.deepcopy(result) + changed["weighted"]["cover"]["surviving_lower"] = 140 + with self.assertRaises(ValueError): + verify.check_receipt(result, changed) + verify.check_receipt(result, copy.deepcopy(result)) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/p112-a6-weighted-cover/vendor/LICENSE b/research/p112-a6-weighted-cover/vendor/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/p112-a6-weighted-cover/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-a6-weighted-cover/vendor/PREDECESSOR-NOTICE.md b/research/p112-a6-weighted-cover/vendor/PREDECESSOR-NOTICE.md new file mode 100644 index 0000000000..c6f3494c2c --- /dev/null +++ b/research/p112-a6-weighted-cover/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-a6-weighted-cover/vendor/ROOT-SIMPLEX-PROOF.md b/research/p112-a6-weighted-cover/vendor/ROOT-SIMPLEX-PROOF.md new file mode 100644 index 0000000000..ccae082127 --- /dev/null +++ b/research/p112-a6-weighted-cover/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-a6-weighted-cover/vendor/TWOSIDE-NOTES.md b/research/p112-a6-weighted-cover/vendor/TWOSIDE-NOTES.md new file mode 100644 index 0000000000..e3fd3f2b1d --- /dev/null +++ b/research/p112-a6-weighted-cover/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-a6-weighted-cover/vendor/bk2b.py b/research/p112-a6-weighted-cover/vendor/bk2b.py new file mode 100644 index 0000000000..3394029014 --- /dev/null +++ b/research/p112-a6-weighted-cover/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-a6-weighted-cover/vendor/geometry.py b/research/p112-a6-weighted-cover/vendor/geometry.py new file mode 100644 index 0000000000..222ea556fa --- /dev/null +++ b/research/p112-a6-weighted-cover/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-a6-weighted-cover/vendor/mixed.py b/research/p112-a6-weighted-cover/vendor/mixed.py new file mode 100644 index 0000000000..e79086db5c --- /dev/null +++ b/research/p112-a6-weighted-cover/vendor/mixed.py @@ -0,0 +1,358 @@ +"""Exact 72-support direction alphabet and anchored P112 simplex census. + +Root-star stabilizer coverage follows Nick Petalas's PR3175. The mixed-edge +alphabet, rational two-ray intersections and application are new here. +""" + +from collections import Counter +from fractions import Fraction +from itertools import combinations, combinations_with_replacement, product + +from vendor.geometry import SIMPLE, canonical, dot, primitive, require, solve + +ANCHOR = (1, 0, 1, 0, 1, 0, 1, 0) +CAP = {2: 2, 3: 4, 4: 8, 5: 12, 6: 20, 7: 36} +PROFILE = (4, 5, 5) + (6,) * 9 + + +def projective(row): + require(len(row) == 8 and any(row), "invalid projective vector") + return primitive(tuple(map(Fraction, row))) + + +def alphabet(roots, points): + require(len(roots) == 120 and len(points) == 112, "incomplete root inventory") + norm_four = { + canonical(tuple(x + sign * y for x, y in zip(a, b, strict=True))) + for a, b in combinations(roots, 2) + if dot(a, b) == 0 + for sign in (-1, 1) + } + require( + len(norm_four) == 1080 and all(dot(v, v) == 16 for v in norm_four), + "norm-four projective inventory", + ) + for normal in norm_four: + for simple in SIMPLE: + pairing = dot(normal, simple) + require(pairing % 4 == 0, "nonintegral norm-four reflection") + reflected = canonical( + tuple(x - pairing // 4 * y for x, y in zip(normal, simple, strict=True)) + ) + require(reflected in norm_four, "norm-four inventory not Weyl closed") + ray = projective(solve(SIMPLE, [1] + [0] * 7)) + require(ray in {projective(v) for v in norm_four}, "missing D7 chamber ray") + histogram = Counter(sum(dot(v, p) != 0 for p in points) for v in norm_four) + require(histogram == {70: 128, 73: 896, 76: 56}, "D7 support spectrum") + short = { + projective(v) for v in norm_four if sum(dot(v, p) != 0 for p in points) <= 72 + } + expected = { + canonical( + tuple(signs[i // 2] if i % 2 == choices[i // 2] else 0 for i in range(8)) + ) + for choices in product(range(2), repeat=4) + for signs in product((-1, 1), repeat=4) + } + require(short == expected and len(short) == 128, "non-root anchor orbit") + directions = tuple(sorted({projective(v) for v in roots} | short)) + require(len(directions) == 248 and ANCHOR in short, "72-support alphabet") + return directions, tuple(sorted(short)), dict(sorted(histogram.items())) + + +def anchor_orbit(roots, frame, normals): + """An even signed permutation maps every short D7 normal to ANCHOR.""" + require(len(normals) == 128 and len(frame) == 8, "anchor-orbit input") + for normal in normals: + permutation = [0] * 8 + signs = [1] * 8 + for pair in range(4): + positions = (2 * pair, 2 * pair + 1) + live = next(i for i in positions if normal[i]) + permutation[2 * pair], permutation[2 * pair + 1] = ( + live, + sum(positions) - live, + ) + signs[2 * pair] = normal[live] + if signs.count(-1) % 2: + signs[1] = -1 # This position has zero anchor value. + image = tuple(signs[i] * normal[permutation[i]] for i in range(8)) + require(image == ANCHOR and signs.count(-1) % 2 == 0, "anchor normalization") + transformed = { + canonical(tuple(signs[i] * r[permutation[i]] for i in range(8))) + for r in roots + } + moved_frame = { + canonical(tuple(signs[i] * r[permutation[i]] for i in range(8))) + for r in frame + } + require( + transformed == set(roots) and moved_frame == set(frame), + "anchor symmetry changes P112", + ) + return len(normals) + + +def intersections(directions): + """Solve a=s*u+t*v for each pair of distinct projective directions.""" + require(len(directions) == len(set(directions)) == 248, "incomplete alphabet") + vertices = set() + for u, v in combinations(directions, 2): + i, j = next( + (i, j) for i, j in combinations(range(8), 2) if u[i] * v[j] != u[j] * v[i] + ) + determinant = u[i] * v[j] - u[j] * v[i] + s = Fraction(ANCHOR[i] * v[j] - ANCHOR[j] * v[i], determinant) + t = Fraction(u[i] * ANCHOR[j] - u[j] * ANCHOR[i], determinant) + if s and t and all(s * u[k] + t * v[k] == ANCHOR[k] for k in range(8)): + vertices.add(tuple(s * x for x in u)) + vertices.add(tuple(t * x for x in v)) + require(len(vertices) == 58, "anchored vertex inventory changed") + require( + all((2 * x).denominator == 1 for v in vertices for x in v), + "non-half-integral anchored vertex", + ) + return tuple(sorted(tuple(int(2 * x) for x in v) for v in vertices)) + + +def compatibility(vertices, directions): + require(len(vertices) == len(set(vertices)) == 58, "invalid vertex inventory") + allowed = set(directions) + adjacency = [0] * 58 + for i, j in combinations(range(58), 2): + difference = tuple(x - y for x, y in zip(vertices[i], vertices[j], strict=True)) + if projective(difference) in allowed: + adjacency[i] |= 1 << j + adjacency[j] |= 1 << i + require( + sum(row.bit_count() for row in adjacency) == 1190, "compatibility graph changed" + ) + return tuple(adjacency) + + +def cliques(adjacency, size): + """Unique increasing cliques; at most 34,834 states for size seven.""" + require(len(adjacency) == 58 and 0 <= size <= 7, "unsupported clique domain") + require( + all(type(row) is int and 0 <= row < 1 << 58 for row in adjacency), + "invalid adjacency bits", + ) + stack = [((), (1 << 58) - 1)] + for _ in range(40_000): + if not stack: + return + chosen, candidates = stack.pop() + if len(chosen) == size: + yield chosen + continue + for _ in range(58): + if not candidates: + break + bit = candidates & -candidates + candidates ^= bit + index = bit.bit_length() - 1 + stack.append(((*chosen, index), candidates & adjacency[index])) + require(len(stack) <= 407, "clique work-stack capacity") + require(not stack, "clique state budget exhausted") + + +def rational_rank(rows): + require( + 1 <= len(rows) <= 8 and all(len(row) == 8 for row in rows), + "rank input dimension", + ) + matrix = [list(map(Fraction, row)) for row in rows] + pivot = 0 + for col in range(8): + selected = next((i for i in range(pivot, len(matrix)) if matrix[i][col]), None) + if selected is None: + continue + matrix[pivot], matrix[selected] = matrix[selected], matrix[pivot] + scale = matrix[pivot][col] + matrix[pivot] = [x / scale for x in matrix[pivot]] + for i in range(pivot + 1, len(matrix)): + scale = matrix[i][col] + matrix[i] = [ + x - scale * y for x, y in zip(matrix[i], matrix[pivot], strict=True) + ] + pivot += 1 + return pivot + + +def surviving_support(values, removed): + require( + len(values) == 112 and type(removed) is int and 0 <= removed <= 112, + "invalid support/deletion domain", + ) + require(all(len(row) == 9 for row in values), "nine vertex values required") + costs = [9 - max(Counter(row).values()) for row in values] + return sum(sorted(costs)[: 112 - removed]), dict(sorted(Counter(costs).items())) + + +def mixed_census(vertices, adjacency, points): + anchor = tuple(2 * x for x in ANCHOR) + evaluations = tuple( + (0, dot(p, anchor), *(dot(p, v) for v in vertices)) for p in points + ) + ranks, bounds = Counter(), Counter() + witness, minimum, count = None, 1000, 0 + for chosen in cliques(adjacency, 7): + count += 1 + rank = rational_rank((anchor, *(vertices[i] for i in chosen))) + ranks[rank] += 1 + if rank != 8: + continue + values = tuple( + row[:2] + tuple(row[i + 2] for i in chosen) for row in evaluations + ) + lower, spectrum = surviving_support(values, 32) + bounds[lower] += 1 + if lower < minimum: + minimum, witness = ( + lower, + { + "indices": chosen, + "spectrum": spectrum, + "vertices_doubled": [anchor] + [vertices[i] for i in chosen], + }, + ) + require( + count == 10520 and ranks == {5: 840, 6: 5040, 7: 4032, 8: 608}, + "incomplete mixed-simplex rank census", + ) + require( + minimum == 182 + and bounds == {182: 112, 184: 16, 190: 112, 191: 128, 194: 128, 199: 112}, + "mixed-simplex support bound changed", + ) + return { + "cliques": count, + "rank_histogram": dict(sorted(ranks.items())), + "support_histogram": dict(sorted(bounds.items())), + "minimum_after_32_cuts": minimum, + "witness": witness, + } + + +def root_extensions(prefix, roots): + signed = tuple(v for r in roots for v in (r, tuple(-x for x in r))) + candidates = {r for r in signed if all(dot(r, p) == 4 for p in prefix)} + normals = tuple(r for r in roots if all(dot(r, p) == 0 for p in prefix)) + unseen, representatives, sizes = set(candidates), [], [] + for _ in range(240): + if not unseen: + break + first = min(unseen) + queue, seen = [first], {first} + for index in range(240): + if index >= len(queue): + break + for normal in normals: + pairing = dot(queue[index], normal) + require(pairing % 4 == 0, "nonintegral root-star reflection") + image = tuple( + x - pairing // 4 * y + for x, y in zip(queue[index], normal, strict=True) + ) + require(image in candidates, "root-star reflection leaves candidates") + if image not in seen: + seen.add(image) + queue.append(image) + require(len(queue) <= 240, "root-star orbit capacity") + require(seen <= unseen, "overlapping root-star orbits") + unseen.difference_update(seen) + representatives.append(first) + sizes.append(len(seen)) + require(not unseen, "incomplete root-star partition") + return representatives, sizes + + +def all_root_census(roots): + level, steps = [()], [] + for rank in range(8): + following = [] + for prefix in level: + representatives, sizes = root_extensions(prefix, roots) + steps.append({"rank": rank, "orbit_sizes": sizes}) + following.extend((*prefix, v) for v in representatives) + level = following + require(len(level) == 1, "rank-eight root-star orbit inventory") + costs = [ + 9 - max(Counter([0] + [dot(r, v) for v in level[0]]).values()) for r in roots + ] + require(Counter(costs) == {2: 36, 3: 84}, "A8 evaluation spectrum") + lower = sum(sorted(costs)[:80]) # Relax frame + small support to any 40 root lines. + require(lower == 204, "all-root support budget") + return {"steps": steps, "spectrum": {2: 36, 3: 84}, "minimum_after_40_cuts": lower} + + +def original_survivors(): + distance = (0, 53, 78, 92, 100, 106, 109, 111, 112) + rows = [] + for size in range(8, 13): + for weights in combinations_with_replacement(range(2, 8), size): + if sum(w - 2 for w in weights) >= 48: + continue + feasible = True + for level in range(1, 9): + prefix = weights[: size - 8 + level] + total = sum(CAP[w] for w in prefix) + target = sum(32 if w == 7 else CAP[w] for w in prefix) + if ( + (level == 1 and target < 53 and total < 73) + or (level == 2 and target < 78 and total < 82) + or (level >= 3 and total < distance[level]) + ): + feasible = False + break + basis = weights[: size - 8] + killed = False + if sum(CAP[w] for w in basis) < 53: + killed = sum(basis) <= 7 or any( + all( + sum( + w + for w, g in zip(basis, assignment, strict=True) + if g == group + ) + <= 6 + for group in (0, 1) + ) + for assignment in product(range(2), repeat=len(basis)) + ) + if feasible and not killed: + rows.append(weights) + require(len(rows) == 251 and PROFILE in rows, "original (8,4) residue changed") + return rows + + +def application(): + original = original_survivors() + bases = sorted( + {basis for basis in combinations(PROFILE, 4) if sum(CAP[w] for w in basis) < 53} + ) + require(bases == [PROFILE[:4]], "weight-certified quotient bases changed") + basis = bases[0] + cuts = [ + sum(CAP[w] for w, g in zip(basis, assignment, strict=True) if g == 2) + for assignment in product(range(3), repeat=4) + if all( + sum(w for w, g in zip(basis, assignment, strict=True) if g == group) <= 6 + for group in (0, 1) + ) + ] + require(min(cuts) == 20, "old weight-cover boundary changed") + return { + "b": 8, + "t": 4, + "weights": PROFILE, + "original_survivors": len(original), + "small_support_cap": 32, + "quotient_basis_cap": 52, + "edge_support_cap": 72, + "endpoint_support_cap": 180, + "mixed_lower": 182, + "all_root_lower": 204, + "margin": 2, + "weight_only_two_six_flat_cut_allowance": min(cuts), + } diff --git a/research/p112-a6-weighted-cover/verify.py b/research/p112-a6-weighted-cover/verify.py new file mode 100644 index 0000000000..7641e2c48c --- /dev/null +++ b/research/p112-a6-weighted-cover/verify.py @@ -0,0 +1,138 @@ +"""Replay the characteristic-zero P112 3,4,6^8 weighted-cover exclusion.""" + +import argparse +import hashlib +import json +import subprocess +import sys +from pathlib import Path + +from bound import all_root_six, application, mixed_six +from vendor.geometry import ( + chamber_receipt, + flat_capacity, + frame_lines, + require, + root_data, + root_plane_receipt, +) +from vendor.mixed import alphabet, anchor_orbit, compatibility, intersections +from weighted import weighted_cover + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +DATA = "research/one-sided-six-multisets/data/data.txt" +RETAINED = frozenset(("geometry.py", "mixed.py", "bk2b.py", "LICENSE", + "PREDECESSOR-NOTICE.md", "ROOT-SIMPLEX-PROOF.md", + "TWOSIDE-NOTES.md")) + + +def read_bytes(path): + require(len(path.parts) <= 32, "input path depth") + require(not any(p.is_symlink() for p in (path, *path.parents)), "linked input") + require(path.is_file() and path.stat().st_size <= 2_000_000, + f"missing or oversized input: {path}") + return path.read_bytes() + + +def bind_sources(package=PACKAGE): + sources = json.loads(read_bytes(package / "SOURCES.json")) + rows = sources["retained_files"] + require(len(rows) == 7, "retained source inventory size") + require({row["local_path"] for row in rows} + == {"vendor/" + name for name in RETAINED}, "retained source inventory") + for row in rows: + raw = read_bytes(package / row["local_path"]) + require(hashlib.sha256(raw).hexdigest() == row["sha256"], "changed retained source") + blob = hashlib.sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw, + usedforsecurity=False).hexdigest() + require(blob == row["git_blob"], "changed retained Git bytes") + 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 changed") + raw = read_bytes(path) + digest = hashlib.sha256(raw).hexdigest() + require(digest == pins[0]["sha256"], "changed P112 data") + lines = raw.decode("utf-8").splitlines() + require(len(lines) >= 114, "truncated P112 input") + require(tuple(map(int, lines[0].split())) == labels, "P112 labels differ") + require(tuple(tuple(map(int, line.split())) for line in lines[2:114]) == points, + "P112 roots differ") + 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 original 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), "original table shape") + 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 order") + require(rows[9][2] == 69, "original (6,4) cell changed") + return rows + + +def graph_digest(vertices, adjacency): + raw = json.dumps({"vertices_doubled": vertices, "adjacency": adjacency}, + sort_keys=True, separators=(",", ":")).encode() + return hashlib.sha256(raw).hexdigest() + + +def receipt(): + sources = bind_sources() + roots, points, labels, coordinates = root_data() + digest = bind_data(ROOT / DATA, points, labels, sources) + directions, normals, norm_four_histogram = alphabet(roots, points) + symmetries = anchor_orbit(roots, frame_lines(), normals) + vertices = intersections(directions) + adjacency = compatibility(vertices, directions) + root_bound = all_root_six(roots) + return { + "schema": "p112-a6-weighted-cover/v1", "input_sha256": digest, + "alphabet": {"root_lines": 120, "D7_normal_lines": 1080, + "D7_support_histogram": norm_four_histogram, + "eligible_nonroots": len(normals), "directions": len(directions), + "anchor_symmetries": symmetries}, + "graph": {"vertices": len(vertices), "edges": 595, + "sha256": graph_digest(vertices, adjacency)}, + "mixed": mixed_six(vertices, adjacency, points), + "all_root": root_bound, "application": application(), + "weighted": weighted_cover(roots, coordinates, root_bound["representative"]), + "chamber": chamber_receipt(roots, points, coordinates), + "root_planes": root_plane_receipt(roots), + "six_flat_capacity": flat_capacity(labels, 6), + "original_table": predecessor_table(), + } + + +def check_receipt(actual, expected): + require(json.dumps(actual, sort_keys=True) == json.dumps(expected, sort_keys=True), + "committed mathematical receipt differs") + + +def publish_receipt(result, output): + if output is None: + check_receipt(result, json.loads(read_bytes(PACKAGE / "RESULT.json"))) + return + destination = output.expanduser().resolve() + require(not destination.is_relative_to(ROOT), "output must be outside checkout") + with destination.open("x", encoding="utf-8") as stream: + stream.write(json.dumps(result, indent=2) + "\n") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="write fresh external evidence, no overwrite") + args = parser.parse_args() + publish_receipt(receipt(), args.output) + print("PASS_A6_WEIGHTED_COVER profile=3,4,6^8 mixed=142 root=141 allowance=140 margin=1") + + +if __name__ == "__main__": + main() diff --git a/research/p112-a6-weighted-cover/weighted.py b/research/p112-a6-weighted-cover/weighted.py new file mode 100644 index 0000000000..de5ab021ec --- /dev/null +++ b/research/p112-a6-weighted-cover/weighted.py @@ -0,0 +1,185 @@ +"""A6 weighted frame/six-flat/four-flat cover certificate. + +The rank-three support is relaxed to four arbitrary coordinates. Frame +traversal is adapted from Nick Petalas's PR3180; all weighted bounds here +are new. Apache-2.0. +""" + +import hashlib +import json +from collections import Counter +from itertools import combinations, product + +from vendor.geometry import SIMPLE, canonical, dot, require + +ALL = (1 << 120) - 1 + + +def full_labels(coordinates): + labels = tuple(1 | sum((int(x) % 2) << (i + 1) for i, x in enumerate(row)) + for row in coordinates) + require(len(labels) == len(set(labels)) == 120, "full120 labels") + require(all(0 < x < 512 and x & 1 for x in labels), "odd full120 labels") + return labels + + +def label_reflections(roots, labels): + index = {r: i for i, r in enumerate(roots)} + for r, label in zip(roots, labels, strict=True): + for j, simple in enumerate(SIMPLE): + factor = dot(r, simple) // 4 + reflected = canonical(tuple(x - factor * y + for x, y in zip(r, simple, strict=True))) + require(labels[index[reflected]] == label ^ ((factor & 1) << (j + 1)), + "Weyl label-linear relation") + return 960 + + +def cost_layers(costs): + require(len(costs) == 120 and Counter(costs) == {0: 1, 1: 21, 2: 63, 3: 35}, + "A6 cost inventory") + return tuple(sum(1 << i for i, c in enumerate(costs) if c >= level) + for level in (1, 2, 3)) + + +def weight(mask, layers): + return sum((mask & layer).bit_count() for layer in layers) + + +def frame_inventory(roots): + require(len(roots) == 120, "frame root count") + adjacency = tuple(sum(1 << j for j, s in enumerate(roots) if dot(r, s) == 0) + for r in roots) + stack, frames = [((), ALL)], [] + for _ in range(2_000_000): + if not stack: + break + chosen, candidates = stack.pop() + if len(chosen) == 8: + frames.append(chosen) + continue + for _ in range(120): + if not candidates: + break + bit = candidates & -candidates + candidates ^= bit + i = bit.bit_length() - 1 + stack.append(((*chosen, i), candidates & adjacency[i])) + require(len(stack) <= 961, "frame stack capacity") + require(not stack and len(frames) == len(set(frames)) == 2025, + "complete orthogonal-frame inventory") + return tuple(frames) + + +def selected_six_flats(labels, layers): + require(len(labels) == 120 and len(layers) == 3, "six-flat input dimensions") + kernels = tuple(ALL ^ sum(1 << i for i, label in enumerate(labels) + if (label & x).bit_count() & 1) for x in range(512)) + selected, histogram = set(), Counter() + for pivots in combinations(range(9), 3): + choices = [] + 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) << c + for i, c in enumerate(free)) + for code in range(1 << len(free))) + choices.append(tuple(kernels[row] for row in rows)) + for chosen in product(*choices): + mask = chosen[0] & chosen[1] & chosen[2] + cost = weight(mask, layers) + histogram[cost] += 1 + if cost >= 55: + selected.add(mask) + require(sum(histogram.values()) == 788035 and max(histogram) == 60, + "complete weighted six-flat census") + require(len(selected) == 63 + and Counter(weight(m, layers) for m in selected) == {57: 35, 60: 28}, + "high-weight six-flat inventory") + return tuple(sorted(selected)), dict(sorted(histogram.items())) + + +def high_four_flats(labels, layers): + high = tuple(label for i, label in enumerate(labels) if layers[2] >> i & 1) + require(len(high) == 35, "cost-three labels") + index = {label: i for i, label in enumerate(labels)} + masks = set() + for basis in combinations(high, 4): + span = {0} + for label in basis: + span.update(tuple(x ^ label for x in tuple(span))) + if len(span) != 16: + continue + mask = sum(1 << index[x] for x in span if x in index) + if (mask & layers[2]).bit_count() >= 7: + masks.add(mask) + require(len(masks) == 135 + and Counter((m & layers[2]).bit_count() for m in masks) == {7: 30, 8: 105}, + "high-cost four-flat inventory") + return tuple(sorted(masks)) + + +def arbitrary_extra(prefix, layers, removed): + require(type(removed) is int and 0 <= removed <= 120, "arbitrary-cut budget") + extra = 0 + for level in (3, 2, 1): + exact = layers[level - 1] ^ (layers[level] if level < 3 else 0) + taken = min(removed, (exact & ~prefix).bit_count()) + extra += level * taken + removed -= taken + return extra + + +def cover_pairs(frames, six_flats, four_flats, layers): + require(len(frames) == 2025 and len(six_flats) == 63 and len(four_flats) == 135, + "cover inventory sizes") + frame_histogram, prefix_histogram, quad_maxima = Counter(), Counter(), Counter() + maximum_prefix, tested, losing_maximum = 0, 0, 0 + losing_witness = None + for frame in frames: + frame_mask = sum(1 << i for i in frame) + frame_histogram[weight(frame_mask, layers)] += 1 + for six in six_flats: + prefix = frame_mask | six + cost = weight(prefix, layers) + maximum_prefix = max(maximum_prefix, cost) + relaxed = cost + arbitrary_extra(prefix, layers, 12) + if relaxed > losing_maximum: + losing_maximum = relaxed + losing_witness = {"frame": frame, "six_mask": six} + if cost < 76: + continue + prefix_histogram[cost] += 1 + required = 100 - cost # 112 total, allowing 12 for four arbitrary roots. + residual_maximum = 0 + for four in four_flats: + tested += 1 + residual = weight(four & ~prefix, layers) + residual_maximum = max(residual_maximum, residual) + require(residual < required, "weighted cover reaches 112") + quad_maxima[(cost, residual_maximum)] += 1 + require(frame_histogram == {14: 210, 16: 735, 17: 630, 19: 420, 21: 30}, + "A6 frame cost spectrum") + require(maximum_prefix == 77 and prefix_histogram == {76: 4620, 77: 2520}, + "frame/six-flat prefix boundary") + require(tested == 963900, "four-flat check coverage") + require(losing_maximum == 113, "arbitrary-twelve-cut losing control") + return {"frame_costs": dict(sorted(frame_histogram.items())), + "prefix_costs": dict(sorted(prefix_histogram.items())), + "maximum_prefix": maximum_prefix, "four_flat_tests": tested, + "residual_maxima": [[a, b, n] for (a, b), n in sorted(quad_maxima.items())], + "removed_upper": 111, "surviving_lower": 141, + "losing_arbitrary12_lower": 139, "losing_witness": losing_witness} + + +def weighted_cover(roots, coordinates, star): + costs = tuple(7 - max(Counter((0, *(dot(r, v) for v in star))).values()) + for r in roots) + labels = full_labels(coordinates) + layers = cost_layers(costs) + six, histogram = selected_six_flats(labels, layers) + four = high_four_flats(labels, layers) + raw = json.dumps({"six": six, "four": four}, separators=(",", ":")).encode() + return {"six_flat_histogram": histogram, "selected_six_flats": len(six), + "high_four_flats": len(four), "mask_sha256": hashlib.sha256(raw).hexdigest(), + "label_reflection_checks": label_reflections(roots, labels), + "cover": cover_pairs(frame_inventory(roots), six, four, layers)}