From c2c7508f2d731feea550f1628601aebd35c6e147 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Sat, 17 Oct 2026 14:28:54 +0100 Subject: [PATCH] test(research): certify a sharp P112 mixed-rank anchor bound --- research/p112-mixed-rank-anchor/CHECKS.json | 66 + .../p112-mixed-rank-anchor/CONTROL14.json | 109 ++ .../p112-mixed-rank-anchor/ENGINEERING.md | 95 + research/p112-mixed-rank-anchor/PROOF.md | 201 ++ research/p112-mixed-rank-anchor/README.md | 100 + research/p112-mixed-rank-anchor/RESULT.json | 1636 +++++++++++++++++ research/p112-mixed-rank-anchor/SOURCES.json | 83 + research/p112-mixed-rank-anchor/TASK.json | 90 + research/p112-mixed-rank-anchor/VERIFY.json | 35 + research/p112-mixed-rank-anchor/scan.cpp | 212 +++ .../p112-mixed-rank-anchor/test_verify.py | 238 +++ .../p112-mixed-rank-anchor/vendor/LICENSE | 201 ++ .../p112-mixed-rank-anchor/vendor/NOTICE.md | 14 + .../vendor/PR3162-PROOF.md | 196 ++ .../vendor/PREDECESSOR-NOTICE.md | 13 + .../p112-mixed-rank-anchor/vendor/TWOSIDE.md | 65 + .../p112-mixed-rank-anchor/vendor/census.cpp | 389 ++++ .../p112-mixed-rank-anchor/vendor/geometry.py | 296 +++ research/p112-mixed-rank-anchor/verify.py | 519 ++++++ 19 files changed, 4558 insertions(+) create mode 100644 research/p112-mixed-rank-anchor/CHECKS.json create mode 100644 research/p112-mixed-rank-anchor/CONTROL14.json create mode 100644 research/p112-mixed-rank-anchor/ENGINEERING.md create mode 100644 research/p112-mixed-rank-anchor/PROOF.md create mode 100644 research/p112-mixed-rank-anchor/README.md create mode 100644 research/p112-mixed-rank-anchor/RESULT.json create mode 100644 research/p112-mixed-rank-anchor/SOURCES.json create mode 100644 research/p112-mixed-rank-anchor/TASK.json create mode 100644 research/p112-mixed-rank-anchor/VERIFY.json create mode 100644 research/p112-mixed-rank-anchor/scan.cpp create mode 100644 research/p112-mixed-rank-anchor/test_verify.py create mode 100644 research/p112-mixed-rank-anchor/vendor/LICENSE create mode 100644 research/p112-mixed-rank-anchor/vendor/NOTICE.md create mode 100644 research/p112-mixed-rank-anchor/vendor/PR3162-PROOF.md create mode 100644 research/p112-mixed-rank-anchor/vendor/PREDECESSOR-NOTICE.md create mode 100644 research/p112-mixed-rank-anchor/vendor/TWOSIDE.md create mode 100644 research/p112-mixed-rank-anchor/vendor/census.cpp create mode 100644 research/p112-mixed-rank-anchor/vendor/geometry.py create mode 100644 research/p112-mixed-rank-anchor/verify.py diff --git a/research/p112-mixed-rank-anchor/CHECKS.json b/research/p112-mixed-rank-anchor/CHECKS.json new file mode 100644 index 0000000000..d19823fe4e --- /dev/null +++ b/research/p112-mixed-rank-anchor/CHECKS.json @@ -0,0 +1,66 @@ +{ + "status": "PASS_AUTHOR_CHECKED_P112_MIXED_RANK_ANCHOR", + "checked_at_utc": "2026-10-17T13:27:21.151324+00:00", + "canonical_main": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "priority_revision": 6, + "environment": { + "platform": "Linux-6.6.87.2-microsoft-standard-WSL2-x86_64-with-glibc2.41", + "python": [ + "3.12.15", + "3.13.5" + ], + "gcc": "Debian 14.2.0-19", + "clang": "Debian 19.1.7", + "python_dependencies": "standard library only" + }, + "checks": [ + { + "command": "python3.12 -B scripts/research_package.py --package research/p112-mixed-rank-anchor", + "result": "PASS_REGISTERED_RESEARCH_PACKAGE; complete scan and 14 behavioral test groups; mathematical receipt equal" + }, + { + "command": "python3.13 -O -W error -B research/p112-mixed-rank-anchor/test_verify.py", + "result": "14 tests pass, including two compiled semantic/coverage mutants" + }, + { + "command": "ruff check --select E,F,B,UP,SIM,C4,ISC,PIE,PGH,RUF research/p112-mixed-rank-anchor/verify.py research/p112-mixed-rank-anchor/test_verify.py", + "result": "All checks passed with Ruff 0.17.1" + }, + { + "command": "Warnings-as-errors byte compilation to an external cache; AST function-length inspection", + "result": "PASS; largest new Python function is audit_census at 54 lines" + }, + { + "command": "clang++ -std=c++17 -O2 -g -fsanitize=address,undefined -fno-omit-frame-pointer -Wall -Wextra -Wpedantic -Wconversion -Wsign-conversion -Wshadow -Werror research/p112-mixed-rank-anchor/scan.cpp -o EXTERNAL/scan; EXTERNAL/scan EXTERNAL/fixture.txt --self-test; EXTERNAL/scan EXTERNAL/fixture.txt", + "result": "PASS; no sanitizer finding; full census stdout byte-identical to GCC replay" + }, + { + "command": "Compare every SOURCES.json retained_files copy with git show COMMIT:SOURCE and recorded Git blob/SHA256", + "result": "PASS all six exact origin-byte comparisons" + }, + { + "command": "python3.13 -O -W error -B EXTERNAL_READ_ONLY_GIT_FREE_EXPORT/research/p112-mixed-rank-anchor/verify.py", + "result": "PASS; identical receipt; no Git history, checkout writes or third-party Python modules needed" + } + ], + "measurement": { + "scope": "Python 3.12 full verifier including GCC compilation and independent Python checks", + "wall_seconds": 7.634217109000019, + "maximum_child_rss_kib": 119428, + "test_suite_seconds": 25.243 + }, + "review": { + "kind": "Author checking, independent Python versus native oracle/rank checks and local read-only mathematical/source audit", + "subagent_review": "Unavailable in this session", + "independent_human_review": false, + "proof_kernel_verification": false, + "concurrent_PR3164": "Proof read at 857384079ab640a949fb7618b7909664d3e737e5 for overlap only, not cold-replayed; beta application is corroboration." + }, + "unrun": [ + "Other P112 C1-C7 obligations and beta cells", + "Full inherited TWOSIDE feasibility/filter ledger", + "Selected native/supplier/outer cold replay", + "Independent human or proof-kernel review" + ], + "publication": "Run scripts/check_research_commit.py after committing; this file does not predeclare publication-byte or hosted-CI success." +} diff --git a/research/p112-mixed-rank-anchor/CONTROL14.json b/research/p112-mixed-rank-anchor/CONTROL14.json new file mode 100644 index 0000000000..b1b51ce513 --- /dev/null +++ b/research/p112-mixed-rank-anchor/CONTROL14.json @@ -0,0 +1,109 @@ +{ + "scope": "Counterexample to the separate-fourteen-deletion rank-five-anchor span-four relaxation, not to a common deletion or beta conjecture.", + "first": [ + 298398672570286131, + 52776760246272 + ], + "second": [ + 368712, + 24234763680 + ], + "anchor": { + "vector": [ + 0, + 0, + 0, + 0, + 1, + 0, + -1, + 0 + ], + "cut": [ + 9331885590326542336, + 10170482589700 + ] + }, + "directions": [ + { + "vector": [ + 0, + 0, + 0, + 0, + 0, + 1, + 0, + -1 + ], + "cut": [ + 108519598638235648, + 7146859266058 + ] + }, + { + "vector": [ + 0, + 0, + 0, + 0, + 1, + 0, + -1, + 0 + ], + "cut": [ + 2493515008, + 10170501464064 + ] + }, + { + "vector": [ + 1, + 1, + -1, + -1, + 1, + 1, + -1, + -1 + ], + "cut": [ + 274928243200, + 206162627154 + ] + }, + { + "vector": [ + 1, + 1, + -1, + 1, + 1, + 1, + 1, + -1 + ], + "cut": [ + 78953733651841024, + 11003707294208 + ] + }, + { + "vector": [ + 1, + 1, + 1, + 1, + 1, + 1, + -1, + -1 + ], + "cut": [ + 688008463360, + 3298555871237 + ] + } + ] +} diff --git a/research/p112-mixed-rank-anchor/ENGINEERING.md b/research/p112-mixed-rank-anchor/ENGINEERING.md new file mode 100644 index 0000000000..341426fd39 --- /dev/null +++ b/research/p112-mixed-rank-anchor/ENGINEERING.md @@ -0,0 +1,95 @@ +# Execution and verification boundary + +## Exit predicate and playbook + +Exit when one named beta shape has a precise proof, a source-bound complete +finite check with meaningful rejection controls, reproduction instructions and +a focused published PR. Do not claim a supplier or exponent improvement. + +The autonomous local run playbook was applied as follows. + +1. State the exit predicate before the first iteration. + The predicate above narrowed the live PR3162 handoff to one beta exclusion. +2. Choose a local wake method. Prefer an event-aware watcher for process completion or file changes. Otherwise use a bounded polling interval appropriate to the task. Use the host's recurring wake capability only when the user explicitly asks for future or repeated execution. + Bounded synchronous commands supplied process completion; no recurring job. +3. Start a decision trail with `show-me-your-work` when installed. Otherwise create an append-only `decisions.tsv` with timestamp, phase, decision, reason, evidence, and result columns. + A session-owned external trail recorded scope, the probe, controls and checks. +4. Each iteration makes the smallest evidence-supported change, checks the predicate, logs the result, and discards changes that did not help. + Retain the successful rank-four/twelve-line theorem. Do not extend it to the + failed rank-five/fourteen-line relaxation; retain its exact counterexample. +5. Handle reversible local blockers within scope. Under an explicit full-autonomy grant, apply a default for a reversible user preference, explain it, and give one reply word that reverses it. Pause for missing authority, an irreversible decision, or a user-named gate. + Reuse the clean existing worker and branch from fetched canonical main. No + additional checkout, force operation or selected-record change was needed. +6. Continue through a plateau by changing the hypothesis or measurement. Stop at the predicate or a documented dead end. Never weaken the predicate. + Preserve the rank-four anchor rather than dropping it to obtain a generic + twelve-line statement. The resulting proof excludes exactly one shape. + The submission overlap refresh found PR3164's different proof of both beta + exclusions. Preserve the distinct sharp mixed-rank theorem and label the + application as corroboration; do not claim a still-open-cell closure. + +Build the Lever produced `scan.cpp` and `verify.py` rather than a hand-checked +claim. Prove It Works required all recorded anchor decisions and positive pairs +to receive Python checks. Test Behavior, Not Implementation required actual CLI, +source, cut and compiled-code mutants, not tests of copied constants alone. + +## Code constraints + +The changed execution path is `verify.py`, `scan.cpp`, and their test driver. +The frozen vendor supplies data reconstruction, flat/orbit enumeration and the +rank-six oracle. Its hashes are checked; it is not silently refactored. + +- Rules 1 and 2. No new recursion, asynchronous workers or unstructured jumps. + Native bounds are 112 labels, 248 directions, 120 root anchors, 511 character + words, 788,035 flats and 159 orbits. The anchor examines at most 4,845 bases. + Exhaustive controls stop at 2^20 subsets. Python's census parser consumes at + most 10,000 bounded output lines, advancing its cursor on every iteration. + Every subprocess has a timeout. Capacity failures reject, never truncate. +- Rule 3 deviation. Python and STL allocate managed containers. Eliminating + that allocation would require a different runtime and rewrite frozen inputs. + Scope is this finite replay only. Fixed input sizes and capacities bound live + containers; subprocesses and temporary directories have scoped lifetimes. + The measured Python/GCC replay, including compilation, has maximum child RSS + 119,428 KiB. Native sanitizer controls and the full census pass. If dimensions + are generalized, replace these capacities and measure memory before adoption. +- Rule 4. Each new function is at most sixty physical lines after formatting. + The streaming record boundary was split into `anchor_check`, which validates + one anchor, and `audit_census`, which owns chronological coverage accounting. + Unchanged vendored routines retain their source shape and attribution. +- Rule 5. Runtime contracts check source inventories, all-direction coverage, + record counts, witness cuts, field ranks and exact receipt equality. Native + guards remain active with optimization; Python does not rely on `assert`. +- Rules 6 and 7. Mathematical state is local and passed explicitly. Globals are + immutable paths/flags. Compiler and scanner statuses are checked, and failures + propagate. Regular-file Path writes either complete or raise; their integer + return counts are intentionally unused, and generated evidence is read back. +- Rule 8. One simple macro renames the retained standalone `main` before a fixed + source inclusion. There is no token construction, variadic macro, recursion + through callbacks or generated executable logic. +- Rule 9. No new function pointers or nested pointer ownership. Native tables + and vectors have one local owner. Python imports one static vendor module; + its source bytes are authenticated before mathematical acceptance. This is + not a sandbox against concurrent hostile code replacement. +- Rule 10. Every replay compiles with `-Wall -Wextra -Wpedantic -Wconversion + -Wsign-conversion -Wshadow -Werror`. Python runs with warnings as errors. + Local checks also run Ruff's E,F,B,UP,SIM,C4,ISC,PIE,PGH,RUF diagnostics, + warnings-as-errors byte compilation, and a Clang ASan/UBSan full replay. + No diagnostic is suppressed in source. Ruff ALL additionally reports optional + annotations/docstrings, unittest-versus-pytest style, domain literals, + namespace/CLI conventions and trusted subprocess warnings. Requiring those + unrelated conventions or adding a CI lint dependency is outside this isolated + scientific package. Revisit that policy if this code becomes shared tooling. + +## Review limits + +The independent implementation boundary is the Python anchor/span and deletion +checks versus the C++ scanner. Flat/orbit generation and the Weyl geometry are +credited inherited code, not a separately reimplemented proof. ASan/UBSan, +optimized Python and negative controls are not independent human review. + +No internal subagent review capability was available. A local read-only audit +checked the proof against the actual pruning inequalities, the new cutoff gap, +empty-mask coverage, the quotient basis, and the declared source/CI boundary. +Attention remains on the standard Weyl-chamber theorem, the finite enumerator, +and TWOSIDE's inherited reduction hypotheses. Those dependencies do not vanish +when this isolated result is accepted. PR3164's newly reported beta closure was +read for overlap, not independently cold-replayed here. diff --git a/research/p112-mixed-rank-anchor/PROOF.md b/research/p112-mixed-rank-anchor/PROOF.md new file mode 100644 index 0000000000..230c852f7e --- /dev/null +++ b/research/p112-mixed-rank-anchor/PROOF.md @@ -0,0 +1,201 @@ +# A mixed-rank anchor closes one beta shape + +All label spaces are over F2. Direction spans and piece coefficients are over +a characteristic-zero field K. Use the pinned doubled E8 roots r_t, the 112 +nonframe lines, and the nine-bit labels ell(t). Define + +``` +Lambda(V) = {t : ell(t) is in V} +Off(h) = {t : r_t dot h != 0}. +``` + +## Finite theorem + +Fix any two six-dimensional label spaces V1,V2 and let X be the union of their +live-line masks. For j in {4,6}, define H_j to consist of the nonzero projective +directions h for which some set D_h of at most twelve live lines satisfies + +``` +rank_F2 ell(Off(h) \ (X union D_h)) <= j. +``` + +If H_4 is nonempty, then dim_K span(H_6) <= 3. The bound is sharp for this +separate-deletion contract. It therefore also bounds any subfamily using one +common deletion set. Common-set attainment is not claimed. + +This is an exact finite geometric result, not a supplier or multiplication +claim. Its proof uses the finite census and the standard E8 Weyl-chamber theorem. + +## Direction completeness at support seventy-two + +The retained flat enumerator covers all 788,035 three-dimensional annihilators +in F2^9. Their kernels are all six-flats. Every live six-flat mask has at most +twenty lines. Every live label is odd, so a rank-four label set has at most eight +lines: the first-coordinate functional cuts a four-dimensional space in at most +eight points. + +Every H_6 direction consequently has support at most + +``` +20 + 20 + 12 + 20 = 72. +``` + +Thus at least forty of the 120 E8 root lines are perpendicular. The retained +geometry checks a simple system, positivity of all root coordinates in it, and +all 28 six-node parabolic enlargements. They have at most 36 root lines. In a +closed Weyl chamber, forty perpendicular lines therefore force a seven-node +face. The eight fundamental-ray perpendicular counts are + +``` +42, 28, 22, 14, 16, 23, 37, 63. +``` + +Only the 42 and 63 rays can qualify. Their projective reflection closure has +1,080 D7 normals and 120 E7/root normals. The P112 support histogram of this +whole closure is + +``` +53:112, 56:8, 70:128, 73:896, 76:56. +``` + +There are no supports 71 or 72. The predecessor's 248 directions at cutoff +seventy therefore remain complete at the new cutoff seventy-two. This gap is +explicitly recomputed in `mixed_direction_coverage`; it is not inferred from +having used the old catalogue. The same argument proves the nonzero P112 root +code distance is 53. + +For general K, the rational span of the roots perpendicular to h has rank at +most seven. Rank at most six would give a generic real normal with at least +forty perpendicular roots of rank at most six, contrary to the parabolic cap. +Thus its rational kernel is a line, h is proportional to its rational generator, +and the real classification applies. Scalar extension preserves the ranks of +the resulting rational direction vectors. This also handles complex directions. + +## Complete pair coverage and pruning + +There are 776,805 distinct nonempty six-flat masks. Empty masks cannot admit an +H_6 direction: the other flat, residual flat and deletions cover at most 52 +lines, below distance 53. Repeated masks do not change the question. + +The retained twelve generators preserve binary-label relations. Their signed +Gram matrices are checked against every root pair, and the live roots span Q^8. +Hence the permutations are induced by invertible rational orthogonal maps. +They preserve both residual binary ranks and characteristic-zero direction +spans. Union-find gives 159 first-mask orbits. One first mask per orbit paired +with every second mask covers all pairs, giving 123,511,995 representative pairs. +No symmetry of rational rank is inferred from support permutations alone. + +An anchor in H_4 has support at most 20+20+12+8=60, so only the 120 root normals +need be tested. Before the second flat is removed it has at most forty lines; +afterwards at most twenty. These are necessary cardinality inequalities. Every +remaining decision goes to the exact rank-four oracle. After finding one anchor +for a pair, the program tests every catalogue direction whose residual support +has at most 32 lines for membership in H_6. It does not replace the anchor's +rank-four requirement with rank six. + +The completed census reports 987 anchor decisions, 832 anchor-positive pairs +and 2,146 rank-six oracle calls. Every positive pair has H_6 span at most three. +Python checks every recorded anchor answer, recomputes the complete H_6 list for +every positive pair, validates the literal cuts and computes rational rank. +All 159 orbit rows and coverage totals are required. `RESULT.json` retains them. + +## Exact deletion oracles and sharpness + +For a residual set S of at most twenty odd labels, rank-four retention after +p<=12 deletions is automatic when |S|<=p+4, by keeping any four points. If +|S|>p+8 it is impossible. Otherwise a successful retained set has at least five +points, so rank exactly four and a four-point basis. Four distinct odd labels +x,y,z,w are independent precisely when x XOR y XOR z != w. The odd points of +their span are those four points and their four triple XORs. Enumerating at most +C(20,4)=4,845 bases therefore decides the question exactly. Python independently +constructs full XOR spans instead of using the eight-point formula. + +For rank six, retain PR3161/3162's dual-code oracle. If S has rank r>6, deletion +to rank six is equivalent to r-6 independent restricted character words with +support union of size at most twelve. Here r-6<=3. Enumerate the 511 ambient +nonzero characters and deduplicate restrictions. Three distinct words are +independent exactly when none is the XOR of the other two. Positive answers +carry cuts; Python checks negative answers and the complete direction list. + +The native controls compare both oracles against exhaustive retained-subset +optima for all 4,096 subsets of a rank-nine twelve-point fixture at budgets +zero through twelve. The rank-four control additionally covers a twenty-point +fixture and its 210 one/two-point deletions. Its optimum table enumerates all +1,048,576 subsets. There are 109,239 decision comparisons in total. + +The sharp fixture in `RESULT.json` has first mask +`(881632412340060325,35734196326400)` and second mask +`(4293210,52413606960)`, encoded as low/high 64-bit words. Its four qualifying +vectors are + +``` +(0,0,0,0,0,0,1,1) +(0,0,0,0,1,1,0,0) +(1,1,-1,1,1,-1,-1,-1) +(1,1,-1,1,1,-1,1,1). +``` + +Their rational span has dimension three. The second vector supplies the +rank-four anchor with the retained literal cut. All four rank-six directions +and their cuts are reconstructed and separately checked during replay. + +## Application to the pinned TWOSIDE beta residue + +Retain TWOSIDE's low-piece/fundamental-circuit hypotheses, stated explicitly +here. B is a linearly independent family of nine piece vectors. Each piece q_k +has support in a line set A_k whose binary label rank is its weight w_k. Set +T=span_K B and let C be the P112 root evaluation code. Assume dim(T intersect C) +is at least five, as in the `(b,t)=(5,4)` beta cell. These are inherited reduction +hypotheses, not consequences of the finite scan. + +Consider the weight multiset + +``` +3,4,4,6,6,6,6,6,6. +``` + +Choose four pieces X0 with weights 3,4,6,6. Their support union has at most + +``` +4 + 8 + 20 + 20 = 52 < 53 +``` + +lines. No nonzero combination of them is a codeword. Their images in +T/(T intersect C) are independent. That quotient has dimension at most four, +so they are a quotient basis and dim(T intersect C)=5. + +For each of the five nonbasis pieces, subtract the unique combination of X0 +with the same quotient image. The resulting five vectors c_y lie in C and are +independent: their B coordinates on the nonbasis pieces are distinct unit +vectors. Write c_y as the root evaluations of h_y. The evaluation map is +injective because the live roots span eight dimensions, so the h_y are five +independent directions. + +Put the supports of the two weight-six X0 pieces in V1,V2. Let P be the union +of the other two X0 supports. It has at most 4+8=12 lines and is common to all +five c_y. Outside Lambda(V1) union Lambda(V2) union P, the support of c_y lies +in A_y. The remaining weights are 4,6,6,6,6. Thus all five directions belong to +H_6 and one belongs to H_4. The finite theorem gives span at most three, in +contradiction to independence. + +This excludes exactly the named shape. Against the pinned historical PR3162 +15-to-2 weight ledger, it leaves `2,5,5,5,6,6,6,6,6`. Concurrent PR3164 at +`857384079ab640a949fb7618b7909664d3e737e5` now reports both shapes excluded by a +different root-simplex argument. Our application corroborates one of its +exclusions; it is not a new unresolved-cell closure. Our finite theorem has no +nine-piece or root-simplex premise, so that theorem is a distinct result. +The preceding ledger and TWOSIDE reduction are inherited, not all replayed here. +In particular this is not a claim that all C5 cells, C1-C7, or C(P112)>=64 have +been proved. + +## Controls that prevent an unjustified extension + +The retained PR3162 rank-five witness checks that unstructured separate +twelve-deletion directions can span five. The rank-four anchor premise matters. + +`CONTROL14.json` is a second exact witness: a rank-five anchor at deletion budget +fourteen coexists with five independent rank-six directions at that budget. +Its literal roots, masks and cuts are checked without the exploratory scanner. +Its cut union exceeds fourteen. It refutes that separate-set relaxation, not +the common-set conjecture or the remaining actual beta shape. Do not close the +remaining shape merely by changing four/twelve to five/fourteen in this theorem. diff --git a/research/p112-mixed-rank-anchor/README.md b/research/p112-mixed-rank-anchor/README.md new file mode 100644 index 0000000000..bdb828917c --- /dev/null +++ b/research/p112-mixed-rank-anchor/README.md @@ -0,0 +1,100 @@ +# Mixed residual ranks close one P112 beta shape + +For any two P112 six-dimensional label spaces, suppose some direction reaches +residual binary rank four after at most twelve line deletions. Then all directions +reaching rank six after separately chosen twelve-line deletions span at most +three dimensions. This finite bound is sharp for the separate-set contract. + +Under the pinned TWOSIDE piece and quotient hypotheses, this excludes beta +`(b,t)=(5,4)` shape `3,4^2,6^6`. The observation is to retain the weight-four +nonbasis piece as a rank-four anchor; a generic separate-twelve-deletion +extension is false. + +The submission refresh found concurrent [PR3164](https://github.com/CrocSwap/integer-mult-bounds/pull/3164), +head `857384079ab640a949fb7618b7909664d3e737e5`, which reports a different +root-simplex proof excluding both shapes left by PR3162. This package therefore +corroborates one of those exclusions, not a still-open residue. Its distinct +result is the sharp mixed-rank theorem for arbitrary flat pairs and separate +cuts, without a nine-piece or root-simplex hypothesis. PR3164's proof was read, +not cold-replayed in this session. + +This is author-checked finite evidence, not independent human or proof-kernel +review. It does not prove the full C5 conjecture, `C(P112)>=64`, a new decoder, +a supplier admission or a new kappa. The selected frontier is unchanged. + +## Evidence + +[PROOF.md](PROOF.md) states the theorem, the all-direction coverage argument, +the exact oracles and the quotient-basis application. [RESULT.json](RESULT.json) +records all 159 first-flat orbit rows covering 123,511,995 representative pairs. +Every one of 987 anchor answers and all 832 positive pairs also receive Python +checks, including complete direction inventories and rational ranks. Native +oracles pass 109,239 comparisons against exhaustive retained-subset optima. + +The cutoff grows from seventy to seventy-two, but an explicitly checked gap in +the complete E7/D7 support histogram leaves the same 248 directions. The scan +retains the predecessor's signed-Gram symmetry checks. Root-only coverage would +not justify the rank-six theorem. + +Two exact negative controls delimit the result. PR3162's unanchored twelve-line +fixture has rank five. [CONTROL14.json](CONTROL14.json) gives a rank-five anchor +and five independent rank-six directions with separate fourteen-line cuts. +Neither fixture refutes a common-set or actual-piece conjecture. + +## Reproduce + +From the repository root, with Python 3.12+ and a C++17 compiler: + +```sh +python3.12 -B scripts/research_package.py --package research/p112-mixed-rank-anchor --check-only +python3.12 -B scripts/research_package.py --package research/p112-mixed-rank-anchor +``` + +The replay and fourteen behavioral test groups take about thirty seconds on the +author's machine. Exact environment and additional checks are in +[CHECKS.json](CHECKS.json). No third-party Python dependencies, Lean or Docker +are needed. A direct replay can retain diagnostics externally: + +```sh +python3.12 -B research/p112-mixed-rank-anchor/verify.py --work /YOUR/NEW/EXTERNAL/DIRECTORY +``` + +Without `--work`, scratch is temporary and removed on exit. Set `TMPDIR` to a +session-owned external directory if required by your workspace policy. A direct +Git-free export needs this package and the two `VERIFY.json` input paths. + +[SOURCES.json](SOURCES.json) pins main, the original card and both live inputs. +Its `retained_files` inventory authenticates the vendored PR3162 files by SHA256 +and records their exact source commit, path and Git blob. Replay does not require +a pending PR's Git history. Origin-byte equality was separately checked before +publication; reviewers can fetch PR3162 and compare those recorded blobs. No +predecessor file is edited. All new files are confined to this package. + +## Open next questions + +- Can the 832 positive pairs be classified geometrically, replacing part of the + finite census? Start with the sharp span-three fixture and the source-bound + signed-Gram group. No such classification is supplied. + +The previous remaining `2,5^3,6^5` shape is now reported excluded by concurrent +PR3164. Do not assign another search for it on the basis of PR3162's historical +residue. `CONTROL14.json` still usefully rejects a different attempted relaxation; +it does not contradict PR3164 or any common-set theorem. + +[Task and overlap record](TASK.json). The canonical investigation is +[Discussion3156](https://github.com/CrocSwap/integer-mult-bounds/discussions/3156), +particularly [PR3162's handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/3156#discussioncomment-18998421). + +## Credit + +Nick Petalas. Apache-2.0. The reduction, TWOSIDE hypotheses and original finite +programs are DreamingOfClouds's PR3154, exact head +`708f0ad8928c383de8294aea3c126e9461d2066d`, with the retained E8/decoder lineage. +This successor builds on Nick Petalas's PR3161 and PR3162, the latter at +`ebd7fd275288e4a9f658e77fa77a0119a8322e74`. PR3163 is a distinct rank-seven +common-deletion calibration slice, not this mixed-rank exclusion. The flat/orbit +enumerator, dual rank-six oracle and geometry are copied unchanged from PR3162; +the anchor oracle, mixed-rank scan, independent checks and new application are +added here. See `vendor/PREDECESSOR-NOTICE.md` and `vendor/LICENSE`. + +Development and internal checking used substantial automated assistance. diff --git a/research/p112-mixed-rank-anchor/RESULT.json b/research/p112-mixed-rank-anchor/RESULT.json new file mode 100644 index 0000000000..0b241cebac --- /dev/null +++ b/research/p112-mixed-rank-anchor/RESULT.json @@ -0,0 +1,1636 @@ +{ + "status": "PASS_P112_MIXED_RANK_ANCHOR", + "sources": { + "research/one-sided-six-multisets/data/data.txt": "ac4a48851b922f2a433684b60c74768ae3bb4fc5e8990ffe63e3942bb3c2ea34", + "research/one-sided-six-multisets/data/gens.txt": "0679ba17f68761c9aea31230df8a7ac4a86533b24ee53d786dd1afa216a4b2c9", + "vendor/census.cpp": "cdb2a0599d9a5afed1223dcce0b49500f7e58160a820bb7b33a6a4bab083c306", + "vendor/geometry.py": "c18d0b18eeb6aa01d18103dbb45d788f5ad5807a1d8828dfe1e0ede9bb0e77dd", + "vendor/PR3162-PROOF.md": "6978f53d37a8e262bd9a443425441922c13508e19cb564e37f369f690ef4bfe8", + "vendor/TWOSIDE.md": "226cd59ccc6bc065319e5e4c4768c889206169ff58f74ef4053eeadc5b2e03c8", + "vendor/LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "vendor/PREDECESSOR-NOTICE.md": "7335843fe4bea21e6c65d69970f3314aa1c40ad23ef93b4643b5b226829f6bed" + }, + "fixture_sha256": "882444bb07d2bf04b00663ee47184b663bdc7ac5974600253132da791415a571", + "coverage": { + "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 + ], + "chamber_zero_counts": [ + 42, + 28, + 22, + 14, + 16, + 23, + 37, + 63 + ], + "weyl_directions": 1200, + "e7": 120, + "d7": 1080, + "retained": 248, + "orthogonal_generator_negative_signs": [ + 56, + 32, + 16, + 0, + 104, + 0, + 0, + 0, + 72, + 56, + 84, + 72 + ] + }, + "mixed_direction_coverage": { + "support_cutoff": 72, + "required_perpendicular_lines": 40, + "orbit_support_histogram": [ + [ + 53, + 112 + ], + [ + 56, + 8 + ], + [ + 70, + 128 + ], + [ + 73, + 896 + ], + [ + 76, + 56 + ] + ], + "retained": 248 + }, + "oracle_comparisons": 109239, + "census": { + "rows": [ + [ + 0, + 145014, + 8, + 0, + 0, + 0 + ], + [ + 1, + 238743, + 7, + 0, + 0, + 0 + ], + [ + 2, + 264349, + 8, + 0, + 0, + 0 + ], + [ + 3, + 318523, + 10, + 0, + 0, + 0 + ], + [ + 4, + 342563, + 8, + 0, + 0, + 0 + ], + [ + 5, + 364172, + 10, + 0, + 0, + 0 + ], + [ + 6, + 372752, + 8, + 0, + 0, + 0 + ], + [ + 7, + 373623, + 8, + 0, + 0, + 0 + ], + [ + 8, + 373651, + 12, + 0, + 0, + 0 + ], + [ + 9, + 373843, + 16, + 0, + 0, + 0 + ], + [ + 10, + 373844, + 16, + 0, + 0, + 0 + ], + [ + 11, + 374246, + 16, + 0, + 0, + 0 + ], + [ + 12, + 407847, + 7, + 0, + 0, + 0 + ], + [ + 13, + 412262, + 8, + 0, + 0, + 0 + ], + [ + 14, + 412390, + 8, + 0, + 0, + 0 + ], + [ + 15, + 412414, + 10, + 0, + 0, + 0 + ], + [ + 16, + 420027, + 4, + 0, + 0, + 0 + ], + [ + 17, + 420029, + 8, + 0, + 0, + 0 + ], + [ + 18, + 420030, + 12, + 0, + 0, + 0 + ], + [ + 19, + 420058, + 16, + 0, + 0, + 0 + ], + [ + 20, + 420289, + 12, + 0, + 0, + 0 + ], + [ + 21, + 423074, + 10, + 0, + 0, + 0 + ], + [ + 22, + 423128, + 10, + 0, + 0, + 0 + ], + [ + 23, + 424027, + 16, + 1, + 28, + 28 + ], + [ + 24, + 450215, + 8, + 0, + 0, + 0 + ], + [ + 25, + 450220, + 16, + 0, + 0, + 0 + ], + [ + 26, + 450273, + 20, + 3, + 65, + 65 + ], + [ + 27, + 457586, + 12, + 0, + 0, + 0 + ], + [ + 28, + 457587, + 12, + 0, + 0, + 0 + ], + [ + 29, + 457659, + 14, + 1, + 20, + 20 + ], + [ + 30, + 458596, + 16, + 0, + 0, + 0 + ], + [ + 31, + 460758, + 12, + 0, + 0, + 0 + ], + [ + 32, + 460767, + 12, + 0, + 0, + 0 + ], + [ + 33, + 475396, + 8, + 0, + 0, + 0 + ], + [ + 34, + 478001, + 12, + 0, + 0, + 0 + ], + [ + 35, + 478006, + 12, + 0, + 0, + 0 + ], + [ + 36, + 478753, + 14, + 1, + 20, + 20 + ], + [ + 37, + 479260, + 11, + 0, + 0, + 0 + ], + [ + 38, + 479318, + 14, + 0, + 0, + 0 + ], + [ + 39, + 488685, + 16, + 0, + 0, + 0 + ], + [ + 40, + 489280, + 8, + 0, + 0, + 0 + ], + [ + 41, + 495922, + 16, + 1, + 24, + 24 + ], + [ + 42, + 502366, + 15, + 0, + 0, + 0 + ], + [ + 43, + 502657, + 16, + 1, + 32, + 32 + ], + [ + 44, + 502683, + 15, + 1, + 32, + 32 + ], + [ + 45, + 502728, + 19, + 0, + 12, + 0 + ], + [ + 46, + 507932, + 11, + 0, + 0, + 0 + ], + [ + 47, + 513915, + 16, + 0, + 0, + 0 + ], + [ + 48, + 513947, + 16, + 0, + 0, + 0 + ], + [ + 49, + 515687, + 16, + 0, + 0, + 0 + ], + [ + 50, + 515777, + 16, + 1, + 28, + 28 + ], + [ + 51, + 523319, + 12, + 0, + 0, + 0 + ], + [ + 52, + 523379, + 14, + 0, + 0, + 0 + ], + [ + 53, + 523393, + 14, + 0, + 0, + 0 + ], + [ + 54, + 525275, + 14, + 0, + 0, + 0 + ], + [ + 55, + 525276, + 14, + 0, + 0, + 0 + ], + [ + 56, + 525277, + 16, + 0, + 0, + 0 + ], + [ + 57, + 525280, + 16, + 1, + 32, + 32 + ], + [ + 58, + 525911, + 14, + 0, + 0, + 0 + ], + [ + 59, + 527694, + 12, + 0, + 0, + 0 + ], + [ + 60, + 543784, + 12, + 0, + 0, + 0 + ], + [ + 61, + 545358, + 16, + 0, + 0, + 0 + ], + [ + 62, + 545821, + 16, + 0, + 0, + 0 + ], + [ + 63, + 545859, + 16, + 0, + 0, + 0 + ], + [ + 64, + 558726, + 11, + 0, + 0, + 0 + ], + [ + 65, + 558761, + 11, + 0, + 0, + 0 + ], + [ + 66, + 558762, + 15, + 0, + 0, + 0 + ], + [ + 67, + 560034, + 15, + 0, + 0, + 0 + ], + [ + 68, + 567649, + 14, + 0, + 0, + 0 + ], + [ + 69, + 567653, + 20, + 2, + 24, + 24 + ], + [ + 70, + 574219, + 10, + 0, + 0, + 0 + ], + [ + 71, + 574305, + 12, + 0, + 0, + 0 + ], + [ + 72, + 574310, + 12, + 0, + 0, + 0 + ], + [ + 73, + 574312, + 12, + 0, + 0, + 0 + ], + [ + 74, + 574333, + 12, + 0, + 0, + 0 + ], + [ + 75, + 574608, + 12, + 0, + 0, + 0 + ], + [ + 76, + 580573, + 12, + 0, + 0, + 0 + ], + [ + 77, + 581557, + 20, + 3, + 65, + 65 + ], + [ + 78, + 589937, + 10, + 0, + 0, + 0 + ], + [ + 79, + 589953, + 10, + 0, + 0, + 0 + ], + [ + 80, + 597570, + 12, + 0, + 0, + 0 + ], + [ + 81, + 597574, + 12, + 0, + 0, + 0 + ], + [ + 82, + 597576, + 12, + 0, + 0, + 0 + ], + [ + 83, + 597586, + 12, + 0, + 0, + 0 + ], + [ + 84, + 599668, + 16, + 0, + 0, + 0 + ], + [ + 85, + 599678, + 12, + 0, + 0, + 0 + ], + [ + 86, + 600659, + 16, + 0, + 0, + 0 + ], + [ + 87, + 600705, + 16, + 0, + 0, + 0 + ], + [ + 88, + 601211, + 20, + 0, + 0, + 0 + ], + [ + 89, + 607186, + 18, + 0, + 0, + 0 + ], + [ + 90, + 607187, + 18, + 3, + 53, + 53 + ], + [ + 91, + 616255, + 14, + 0, + 0, + 0 + ], + [ + 92, + 620767, + 12, + 0, + 0, + 0 + ], + [ + 93, + 621131, + 14, + 0, + 0, + 0 + ], + [ + 94, + 621151, + 20, + 0, + 0, + 0 + ], + [ + 95, + 621172, + 16, + 0, + 0, + 0 + ], + [ + 96, + 627135, + 16, + 0, + 0, + 0 + ], + [ + 97, + 627611, + 16, + 0, + 0, + 0 + ], + [ + 98, + 627612, + 16, + 0, + 0, + 0 + ], + [ + 99, + 633891, + 16, + 0, + 0, + 0 + ], + [ + 100, + 653847, + 18, + 0, + 0, + 0 + ], + [ + 101, + 656472, + 16, + 0, + 0, + 0 + ], + [ + 102, + 657431, + 15, + 0, + 0, + 0 + ], + [ + 103, + 657632, + 15, + 0, + 0, + 0 + ], + [ + 104, + 657790, + 12, + 0, + 0, + 0 + ], + [ + 105, + 658198, + 15, + 0, + 0, + 0 + ], + [ + 106, + 661350, + 16, + 1, + 24, + 24 + ], + [ + 107, + 661833, + 18, + 2, + 4, + 4 + ], + [ + 108, + 670140, + 12, + 0, + 0, + 0 + ], + [ + 109, + 677469, + 10, + 0, + 0, + 0 + ], + [ + 110, + 684272, + 12, + 0, + 0, + 0 + ], + [ + 111, + 684486, + 16, + 0, + 0, + 0 + ], + [ + 112, + 684958, + 6, + 0, + 0, + 0 + ], + [ + 113, + 684959, + 6, + 0, + 0, + 0 + ], + [ + 114, + 685338, + 12, + 0, + 0, + 0 + ], + [ + 115, + 685346, + 12, + 0, + 0, + 0 + ], + [ + 116, + 685354, + 12, + 0, + 0, + 0 + ], + [ + 117, + 685430, + 8, + 0, + 0, + 0 + ], + [ + 118, + 685464, + 16, + 1, + 32, + 32 + ], + [ + 119, + 685478, + 16, + 0, + 0, + 0 + ], + [ + 120, + 685502, + 16, + 0, + 0, + 0 + ], + [ + 121, + 685902, + 10, + 0, + 0, + 0 + ], + [ + 122, + 686532, + 20, + 3, + 161, + 129 + ], + [ + 123, + 687046, + 10, + 0, + 0, + 0 + ], + [ + 124, + 687049, + 12, + 0, + 0, + 0 + ], + [ + 125, + 692522, + 14, + 0, + 0, + 0 + ], + [ + 126, + 692523, + 14, + 0, + 0, + 0 + ], + [ + 127, + 703759, + 16, + 0, + 0, + 0 + ], + [ + 128, + 703824, + 18, + 0, + 0, + 0 + ], + [ + 129, + 704618, + 14, + 0, + 0, + 0 + ], + [ + 130, + 706114, + 12, + 0, + 0, + 0 + ], + [ + 131, + 706330, + 14, + 0, + 0, + 0 + ], + [ + 132, + 706337, + 16, + 0, + 0, + 0 + ], + [ + 133, + 707421, + 14, + 0, + 0, + 0 + ], + [ + 134, + 707422, + 14, + 0, + 0, + 0 + ], + [ + 135, + 707661, + 16, + 0, + 0, + 0 + ], + [ + 136, + 707667, + 16, + 0, + 0, + 0 + ], + [ + 137, + 707735, + 18, + 0, + 96, + 0 + ], + [ + 138, + 707740, + 14, + 1, + 32, + 32 + ], + [ + 139, + 712806, + 14, + 0, + 0, + 0 + ], + [ + 140, + 712939, + 16, + 0, + 0, + 0 + ], + [ + 141, + 712940, + 16, + 3, + 20, + 20 + ], + [ + 142, + 718805, + 18, + 3, + 53, + 53 + ], + [ + 143, + 723673, + 14, + 0, + 0, + 0 + ], + [ + 144, + 733507, + 12, + 0, + 0, + 0 + ], + [ + 145, + 733647, + 16, + 0, + 0, + 0 + ], + [ + 146, + 742641, + 12, + 0, + 0, + 0 + ], + [ + 147, + 742663, + 12, + 0, + 0, + 0 + ], + [ + 148, + 746536, + 16, + 0, + 0, + 0 + ], + [ + 149, + 746594, + 12, + 0, + 0, + 0 + ], + [ + 150, + 747334, + 12, + 0, + 0, + 0 + ], + [ + 151, + 750649, + 16, + 0, + 0, + 0 + ], + [ + 152, + 756065, + 20, + 0, + 0, + 0 + ], + [ + 153, + 756254, + 12, + 0, + 0, + 0 + ], + [ + 154, + 756264, + 12, + 0, + 0, + 0 + ], + [ + 155, + 763031, + 19, + 0, + 0, + 0 + ], + [ + 156, + 766178, + 16, + 1, + 32, + 32 + ], + [ + 157, + 766210, + 20, + 0, + 0, + 0 + ], + [ + 158, + 773428, + 19, + 3, + 98, + 83 + ] + ], + "total": { + "pairs": 123511995, + "anchor_tests": 987, + "positive_pairs": 832, + "rank_six_oracle_calls": 2146, + "max_span": 3 + }, + "witness": { + "first": [ + 881632412340060325, + 35734196326400 + ], + "second": [ + 4293210, + 52413606960 + ], + "anchor": 11, + "anchor_cut": [ + 3458777914118504448, + 17867200266252 + ], + "directions": [ + 1, + 11, + 227, + 228 + ], + "vectors": [ + [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + [ + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0 + ], + [ + 1, + 1, + -1, + 1, + 1, + -1, + -1, + -1 + ], + [ + 1, + 1, + -1, + 1, + 1, + -1, + 1, + 1 + ] + ], + "rank": 3 + }, + "native_stdout_sha256": "6983d102c1ed9fa9c96b615832b5bd57491855d266b1a9248f167acd79eeeaa0", + "independent_anchor_checks": 987, + "independent_positive_pairs": 832 + }, + "unanchored_control": { + "source": "PR3162 WITNESS_12", + "witness": [ + 298398672570286131, + 52776760246272, + 516232, + 28051596928, + 5, + 2, + 162762907430420484, + 8797703766112, + 7, + 108508605669441600, + 8800924893472, + 221, + 1152930301523001344, + 3367275333632, + 230, + 18577350611437568, + 8830453975040, + 246, + 86704654336, + 73701659770888 + ], + "rank": 5 + }, + "fourteen_control": { + "witness": { + "scope": "Counterexample to the separate-fourteen-deletion rank-five-anchor span-four relaxation, not to a common deletion or beta conjecture.", + "first": [ + 298398672570286131, + 52776760246272 + ], + "second": [ + 368712, + 24234763680 + ], + "anchor": { + "vector": [ + 0, + 0, + 0, + 0, + 1, + 0, + -1, + 0 + ], + "cut": [ + 9331885590326542336, + 10170482589700 + ] + }, + "directions": [ + { + "vector": [ + 0, + 0, + 0, + 0, + 0, + 1, + 0, + -1 + ], + "cut": [ + 108519598638235648, + 7146859266058 + ] + }, + { + "vector": [ + 0, + 0, + 0, + 0, + 1, + 0, + -1, + 0 + ], + "cut": [ + 2493515008, + 10170501464064 + ] + }, + { + "vector": [ + 1, + 1, + -1, + -1, + 1, + 1, + -1, + -1 + ], + "cut": [ + 274928243200, + 206162627154 + ] + }, + { + "vector": [ + 1, + 1, + -1, + 1, + 1, + 1, + 1, + -1 + ], + "cut": [ + 78953733651841024, + 11003707294208 + ] + }, + { + "vector": [ + 1, + 1, + 1, + 1, + 1, + 1, + -1, + -1 + ], + "cut": [ + 688008463360, + 3298555871237 + ] + } + ] + }, + "rank": 5, + "cut_union_size": 52 + }, + "beta": { + "cell": [ + 5, + 4 + ], + "weights": [ + 3, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "quotient_basis": [ + 3, + 4, + 6, + 6 + ], + "support_cap": 52, + "common_deletion_cap": 12, + "nonbasis_weights": [ + 4, + 6, + 6, + 6, + 6 + ], + "forced_direction_rank": 5, + "finite_upper_bound": 3, + "remaining_from_PR3162": [ + 2, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6 + ] + } +} diff --git a/research/p112-mixed-rank-anchor/SOURCES.json b/research/p112-mixed-rank-anchor/SOURCES.json new file mode 100644 index 0000000000..2ec170f2e8 --- /dev/null +++ b/research/p112-mixed-rank-anchor/SOURCES.json @@ -0,0 +1,83 @@ +{ + "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/one-sided-six-multisets/data/gens.txt", + "usage": "input", + "git_blob": "ba27ea667b9d00e6976c11d349fa84d959b78253", + "sha256": "0679ba17f68761c9aea31230df8a7ac4a86533b24ee53d786dd1afa216a4b2c9" + } + ], + "retained_files": [ + { + "copy": "vendor/census.cpp", + "sha256": "cdb2a0599d9a5afed1223dcce0b49500f7e58160a820bb7b33a6a4bab083c306", + "source": "research/p112-ten-deletion-span/census.cpp", + "commit": "ebd7fd275288e4a9f658e77fa77a0119a8322e74", + "git_blob": "6e33b5c713aaa75a4ac6392daabd08c8480b6c6b" + }, + { + "copy": "vendor/geometry.py", + "sha256": "c18d0b18eeb6aa01d18103dbb45d788f5ad5807a1d8828dfe1e0ede9bb0e77dd", + "source": "research/p112-ten-deletion-span/geometry.py", + "commit": "ebd7fd275288e4a9f658e77fa77a0119a8322e74", + "git_blob": "3579fa6a786f7b96386b7a3b938790cbbaf88b3b" + }, + { + "copy": "vendor/PR3162-PROOF.md", + "sha256": "6978f53d37a8e262bd9a443425441922c13508e19cb564e37f369f690ef4bfe8", + "source": "research/p112-ten-deletion-span/PROOF.md", + "commit": "ebd7fd275288e4a9f658e77fa77a0119a8322e74", + "git_blob": "fb45b45d0ced71d3c9ed0b6523f8edaef28ded35" + }, + { + "copy": "vendor/TWOSIDE.md", + "sha256": "226cd59ccc6bc065319e5e4c4768c889206169ff58f74ef4053eeadc5b2e03c8", + "source": "research/p112-ten-deletion-span/vendor/TWOSIDE.md", + "commit": "ebd7fd275288e4a9f658e77fa77a0119a8322e74", + "git_blob": "e3fd3f2b1dfd77b597f000b38ec2dbec3dbca931" + }, + { + "copy": "vendor/LICENSE", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "source": "research/p112-ten-deletion-span/vendor/LICENSE", + "commit": "ebd7fd275288e4a9f658e77fa77a0119a8322e74", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64" + }, + { + "copy": "vendor/PREDECESSOR-NOTICE.md", + "sha256": "7335843fe4bea21e6c65d69970f3314aa1c40ad23ef93b4643b5b226829f6bed", + "source": "research/p112-ten-deletion-span/vendor/NOTICE.md", + "commit": "ebd7fd275288e4a9f658e77fa77a0119a8322e74", + "git_blob": "227999aa6e6c46e48c7abea758ce967051dd0f30" + } + ], + "retained_source_policy": "Vendored PR3162 files are authenticated by SHA256 during replay. Exact upstream commit and Git blob are recorded for separately fetching/comparing origin bytes, without requiring pending PR history for offline replay.", + "related_work": [ + { + "pr": 3164, + "commit": "857384079ab640a949fb7618b7909664d3e737e5", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3164", + "usage": "Overlap comparison only; proof read, mathematics not cold-replayed and not a replay dependency." + } + ] +} diff --git a/research/p112-mixed-rank-anchor/TASK.json b/research/p112-mixed-rank-anchor/TASK.json new file mode 100644 index 0000000000..bca0f2a056 --- /dev/null +++ b/research/p112-mixed-rank-anchor/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 6, + "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?", + "starting_points": [ + "certificates/selected-result.json", + "research/hyperplane-end-lean/PROOF.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the sharp P112 rank-four-anchor/rank-six twelve-deletion theorem, and give its conditional beta application as corroboration of concurrent PR3164.", + "scope_change_reason": "Take the live PR3162 quotient-basis-cover handoff in Discussion3156. The nonbasis weight-four piece supplies a stronger mixed-rank constraint than the failed generic twelve-deletion extension. This is a finite geometric theorem, not a Lean formalization. Submission refresh found PR3164 already reports both beta shapes excluded by a different proof. Retain the distinct arbitrary-flat/separate-cut theorem and label the beta application as corroboration rather than a still-open-cell closure.", + "bottleneck_link": "A sharp finite support restriction independently corroborates one named beta exclusion. Concurrent PR3164 already reports both shapes closed; no still-open-cell, supplier or kappa gain is claimed.", + "budget_minutes": 60, + "stop_rule": "Stop at one certified beta exclusion, a falsifier or sixty minutes; do not expand into another supplier or full C1-C7 census.", + "outcome": "partial", + "evidence": "RESULT.json records all 159 first-flat orbits, 123511995 representative pairs, 987 independently checked anchor decisions, 832 independently checked positive pairs and a sharp span-three fixture.", + "author": "Nick Petalas", + "ai_assistance": "Development and internal checking used substantial automated assistance; independent human or proof-kernel review is not claimed.", + "open_questions": [ + { + "question": "Can the 832 mixed-positive pairs be replaced by a short geometric classification?", + "why_it_matters": "It would shrink the finite computational proof dependency.", + "first_step": "Classify the sharp three-dimensional fixture and the retained first-flat types under the source-bound signed-Gram group.", + "blocked_by": "No such classification is proved here." + } + ], + "coordination": { + "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/3156#discussioncomment-18998421", + "nearest_prs": [ + 3154, + 3161, + 3162, + 3163, + 3164 + ], + "scope_distinction": "New mixed residual-rank hypothesis, not another unconstrained rank-seven slice or generic separate-twelve census. C6 is claimed by the predecessor and is untouched. PR3164 at 857384079ab640a949fb7618b7909664d3e737e5 reports both beta shapes excluded. Its argument assumes nine pieces/root-simplex relations; the mixed-rank theorem does not.", + "advance_claim": "Not posted; bounded session after live overlap inspection." + }, + "freshness": { + "canonical_main": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "priority_revision": 6, + "checked_at_utc": "2026-10-17T13:26:27.851882+00:00", + "overlap_coverage": { + "open_prs": { + "fetched_at": "2026-10-17T13:24:52.393611+00:00", + "complete_pagination": true, + "records": 284 + }, + "discussions": { + "fetched_at": "2026-10-17T13:25:20.328087+00:00", + "complete_pagination": true, + "records": 1933 + } + }, + "overlap_warnings": [] + } +} diff --git a/research/p112-mixed-rank-anchor/VERIFY.json b/research/p112-mixed-rank-anchor/VERIFY.json new file mode 100644 index 0000000000..39c2a55f23 --- /dev/null +++ b/research/p112-mixed-rank-anchor/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/one-sided-six-multisets/data/data.txt", + "research/one-sided-six-multisets/data/gens.txt" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Complete mixed-rank pair census; cutoff-72 Weyl coverage; signed-Gram symmetry; 109239 exhaustive oracle comparisons; separate Python checks of every anchor decision and positive pair; beta application and unanchored rank-five control." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 180, + "checks": "Fourteen behavioral groups including compiled anchor/coverage mutants, changed source and receipt controls, malformed native inputs, invalid cuts and rational-versus-binary rank." + } + ] +} diff --git a/research/p112-mixed-rank-anchor/scan.cpp b/research/p112-mixed-rank-anchor/scan.cpp new file mode 100644 index 0000000000..d1bce05e13 --- /dev/null +++ b/research/p112-mixed-rank-anchor/scan.cpp @@ -0,0 +1,212 @@ +// Mixed residual-rank anchor census. Nick Petalas. Apache-2.0. +// The frozen predecessor supplies flat/orbit enumeration and rank-six oracle. +#define main retained_predecessor_main +#include "vendor/census.cpp" +#undef main + +bool anchor(const Data &data, Mask rest, int budget, Mask *cut = nullptr) { + if (budget < 0 || budget > 12) throw std::runtime_error("anchor budget capacity"); + const int size = count(rest); + if (size > budget + 8) return false; + std::array labels{}; + std::array position{}; + position.fill(-1); + int n = 0; + for (int i = 0; i < 112; ++i) if (has(rest, i)) { + if (n >= 20) throw std::runtime_error("anchor label capacity"); + const int x = data.labels[static_cast(i)]; + labels[static_cast(n++)] = x; + position[static_cast(x)] = i; + } + if (size <= budget + 4) { + Mask kept{}; + for (int i = 0; i < std::min(n, 4); ++i) + set(kept, position[static_cast(labels[static_cast(i)])]); + if (cut) *cut = minus(rest, kept); + return true; + } + for (int a = 0; a < n; ++a) for (int b = a + 1; b < n; ++b) + for (int c = b + 1; c < n; ++c) for (int d = c + 1; d < n; ++d) { + const int x = labels[static_cast(a)], y = labels[static_cast(b)]; + const int z = labels[static_cast(c)], w = labels[static_cast(d)]; + if ((x ^ y ^ z) == w) continue; + Mask kept{}; + for (int value : {x, y, z, w, x ^ y ^ z, x ^ y ^ w, x ^ z ^ w, y ^ z ^ w}) { + const int i = position[static_cast(value)]; + if (i >= 0) set(kept, i); + } + if (size - count(kept) <= budget) { + if (cut) *cut = minus(rest, kept); + return true; + } + } + return false; +} + +struct Candidate { + int direction = 0; + Mask rest{}; +}; + +std::size_t anchor_candidates(const Data &data, Mask first, + std::array &active) { + std::size_t n = 0; + for (int h = 0; h < 248; ++h) { + if (count(data.off[static_cast(h)]) > 60) continue; + const Mask rest = minus(data.off[static_cast(h)], first); + if (count(rest) > 40) continue; + if (n >= active.size()) throw std::runtime_error("root anchor inventory"); + active[n++] = {h, rest}; + } + return n; +} + +int emit_positive(const Data &data, Mask first, Mask second, U &calls) { + Found found{}; + int n = 0; + std::array cuts{}; + for (int h = 0; h < 248; ++h) { + const Mask rest = minus(data.off[static_cast(h)], first | second); + if (count(rest) > 32) continue; + ++calls; + Mask cut{}; + if (deletable(data, rest, 12, &cut)) { + found[static_cast(n)] = h; + cuts[static_cast(n++)] = cut; + } + } + std::cout << "POS " << n; + for (int i = 0; i < n; ++i) { + const Mask cut = cuts[static_cast(i)]; + std::cout << ' ' << found[static_cast(i)] << ' ' << cut.lo << ' ' << cut.hi; + } + std::cout << '\n'; + return rational_rank(data, found, n); +} + +void mixed_census(const Data &data, const std::vector &space, + const std::vector &reps) { + U pairs = 0, tests = 0, positives = 0, calls = 0; + int global = 0; + std::cout << "COVER " << space.size() << ' ' << reps.size() << '\n'; + for (std::size_t ri = 0; ri < reps.size(); ++ri) { + const Mask first = space[reps[ri]]; + std::array active{}; + const std::size_t n = anchor_candidates(data, first, active); + U row_tests = 0, row_positives = 0; + int maximum = 0; + for (std::size_t j = 0; j < space.size(); ++j) { + ++pairs; + for (std::size_t a = 0; a < n; ++a) { + const Mask rest = minus(active[a].rest, space[j]); + if (count(rest) > 20) continue; + ++row_tests; + Mask cut{}; + const bool answer = anchor(data, rest, 12, &cut); + std::cout << "ANCHOR " << ri << ' ' << j << ' ' << first.lo << ' ' << first.hi + << ' ' << space[j].lo << ' ' << space[j].hi << ' ' << active[a].direction + << ' ' << answer << ' ' << cut.lo << ' ' << cut.hi << '\n'; + if (!answer) continue; + ++row_positives; + maximum = std::max(maximum, emit_positive(data, first, space[j], calls)); + break; + } + } + tests += row_tests; + positives += row_positives; + global = std::max(global, maximum); + std::cout << "ROW " << ri << ' ' << reps[ri] << ' ' << count(first) << ' ' + << maximum << ' ' << row_tests << ' ' << row_positives << '\n'; + } + std::cout << "TOTAL " << pairs << ' ' << tests << ' ' << positives << ' ' << calls << ' ' << global << '\n'; +} + +std::vector best_retained(const Data &data, const std::array &indices, + int bits, int target) { + if (bits < 1 || bits > 20 || target < 0 || target > 9) + throw std::runtime_error("exhaustive oracle capacity"); + const unsigned capacity = 1U << bits; + std::vector best(capacity); + for (unsigned code = 0; code < capacity; ++code) { + Mask mask{}; + for (int bit = 0; bit < bits; ++bit) + if ((code >> bit) & 1U) set(mask, indices[static_cast(bit)]); + if (binary_rank(data, mask) <= target) best[code] = __builtin_popcount(code); + } + for (int bit = 0; bit < bits; ++bit) for (unsigned code = 0; code < capacity; ++code) + if ((code >> bit) & 1U) best[code] = std::max(best[code], best[code ^ (1U << bit)]); + return best; +} + +void check_oracle(const Data &data, const std::array &indices, + unsigned code, int target, const std::vector &best, U &checks) { + Mask mask{}; + for (int bit = 0; bit < 20; ++bit) + if ((code >> bit) & 1U) set(mask, indices[static_cast(bit)]); + const int minimum = __builtin_popcount(code) - best[code]; + for (int budget = 0; budget <= 12; ++budget) { + Mask cut{}; + const bool answer = target == 4 ? anchor(data, mask, budget, &cut) + : deletable(data, mask, budget, &cut); + if (answer != (minimum <= budget) || + (answer && (count(cut) > budget || count(minus(cut, mask)) || + binary_rank(data, minus(mask, cut)) > target))) + throw std::runtime_error("oracle disagrees with exhaustive retained-subset optimum"); + ++checks; + } +} + +void oracle_controls(const Data &data) { + std::array indices{}; + Mask selected{}; + int n = 0; + for (int i = 0; i < 112; ++i) { + Mask trial = selected; + set(trial, i); + if (binary_rank(data, trial) > binary_rank(data, selected)) { + indices[static_cast(n++)] = i; + selected = trial; + } + } + if (n != 9) throw std::runtime_error("full binary rank control"); + for (int i = 0; i < 112 && n < 20; ++i) if (!has(selected, i)) { + indices[static_cast(n++)] = i; + set(selected, i); + } + if (n != 20) throw std::runtime_error("oracle fixture capacity"); + U checks = 0; + for (int target : {4, 6}) { + const auto best = best_retained(data, indices, 12, target); + for (unsigned code = 0; code < 4096; ++code) + check_oracle(data, indices, code, target, best, checks); + } + const auto best = best_retained(data, indices, 20, 4); + constexpr unsigned full = (1U << 20) - 1; + check_oracle(data, indices, full, 4, best, checks); + for (int a = 0; a < 20; ++a) { + check_oracle(data, indices, full ^ (1U << a), 4, best, checks); + for (int b = a + 1; b < 20; ++b) + check_oracle(data, indices, full ^ (1U << a) ^ (1U << b), 4, best, checks); + } + std::cout << "PASS_ORACLES " << checks << " exhaustive20 1048576\n"; +} + +int main(int argc, char **argv) { + try { + if (argc < 2 || argc > 3) throw std::runtime_error("usage: scan FIXTURE [--self-test]"); + const Data data = read_data(argv[1]); + for (int label : data.labels) if (!(label & 1)) throw std::runtime_error("labels must be odd"); + if (argc == 3) { + if (std::string(argv[2]) != "--self-test") throw std::runtime_error("unknown mode"); + oracle_controls(data); + } else { + const auto space = flats(data); + const auto reps = representatives(data, space); + mixed_census(data, space, reps); + } + return 0; + } catch (const std::exception &error) { + std::cerr << error.what() << '\n'; + return 2; + } +} diff --git a/research/p112-mixed-rank-anchor/test_verify.py b/research/p112-mixed-rank-anchor/test_verify.py new file mode 100644 index 0000000000..2d314668cf --- /dev/null +++ b/research/p112-mixed-rank-anchor/test_verify.py @@ -0,0 +1,238 @@ +"""Behavioral controls for the mixed-rank theorem's public replay surface.""" + +import copy +import json +import os +import shutil +import subprocess +import tempfile +import unittest +from pathlib import Path + +import verify as v + + +class ReplayTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.temporary = tempfile.TemporaryDirectory( + prefix="p112-anchor-tests-", dir=os.environ.get("TMPDIR") + ) + cls.work = Path(cls.temporary.name) + cls.fixture, _ = v.fixture(*(v.ROOT / name for name in v.INPUTS)) + cls.data = v.parse_fixture(cls.fixture) + cls.path = cls.work / "fixture.txt" + cls.path.write_text(cls.fixture) + cls.binary = v.build(cls.work) + cls.raw = v.run([str(cls.binary), str(cls.path)], cls.work, "census.txt") + cls.result = json.loads((v.PACKAGE / "RESULT.json").read_text()) + + @classmethod + def tearDownClass(cls): + cls.temporary.cleanup() + + def rejects_native(self, args, text): + result = subprocess.run( + [str(self.binary), *args], capture_output=True, text=True, timeout=10 + ) + self.assertEqual(result.returncode, 2) + self.assertIn(text, result.stderr) + + def test_complete_replay_and_literal_theorem(self): + actual = v.audit_census(self.raw, self.data) + self.assertEqual(json.loads(json.dumps(actual)), self.result["census"]) + self.assertEqual( + actual["total"], + { + "pairs": 123511995, + "anchor_tests": 987, + "positive_pairs": 832, + "rank_six_oracle_calls": 2146, + "max_span": 3, + }, + ) + + def test_native_invalid_modes(self): + self.rejects_native([], "usage:") + self.rejects_native([str(self.path), "--unknown"], "unknown mode") + self.rejects_native([str(self.work / "absent")], "cannot read fixture") + + def test_native_duplicate_even_trailing_and_truncated_inputs(self): + lines = self.fixture.splitlines() + labels = lines[0].split() + cases = [ + (labels[:1] + labels[:-1], "invalid label"), + (["2", *labels[1:]], "labels must be odd"), + ] + for index, (changed, expected) in enumerate(cases): + mutant = self.work / f"labels-{index}.txt" + mutant.write_text(" ".join(changed) + "\n" + "\n".join(lines[1:]) + "\n") + self.rejects_native([str(mutant)], expected) + for index, (text, expected) in enumerate( + ( + (self.fixture + "extra\n", "trailing"), + (lines[0] + "\n", "invalid coordinate"), + ) + ): + mutant = self.work / f"boundary-{index}.txt" + mutant.write_text(text) + self.rejects_native([str(mutant)], expected) + + def test_cut_budget_membership_and_rank(self): + labels = self.data[0] + rest = (1 << 20) - 1 + with self.assertRaisesRegex(ValueError, "deletion cut"): + v.check_cut(rest, (1 << 13) - 1, 4, labels) + with self.assertRaisesRegex(ValueError, "deletion cut"): + v.check_cut(rest, 1 << 50, 4, labels) + with self.assertRaisesRegex(ValueError, "residual rank"): + v.check_cut(rest, 0, 4, labels) + v.check_cut(15, 0, 4, labels) + self.assertEqual(v.binary_rank(v.values(15, labels)), 3) + + def test_binary_and_characteristic_zero_rank_are_distinct(self): + rows = [ + [1, 1, 0, 0, 0, 0, 0, 0], + [1, 0, 1, 0, 0, 0, 0, 0], + [0, 1, 1, 0, 0, 0, 0, 0], + ] + self.assertEqual(v.rational_rank(rows), 3) + self.assertEqual(v.binary_rank([3, 5, 6]), 2) + rows[-1] = [2, 1, 1, 0, 0, 0, 0, 0] + self.assertEqual(v.rational_rank(rows), 2) + + def test_anchor_oracle_positive_negative_and_capacity(self): + labels = self.data[0] + self.assertTrue(v.anchor_oracle(15, labels, 0)) + self.assertFalse(v.anchor_oracle((1 << 20) - 1, labels, 0)) + with self.assertRaisesRegex(ValueError, "capacity"): + v.anchor_oracle((1 << 21) - 1, labels) + self.assertEqual(len(v.binary_span([1, 3, 5, 9])), 16) + + def test_missing_row_and_inconsistent_total(self): + lines = self.raw.splitlines() + removed = ( + "\n".join(line for line in lines if not line.startswith("ROW 42 ")) + "\n" + ) + with self.assertRaises(ValueError): + v.audit_census(removed, self.data) + mutant = self.raw.replace( + "TOTAL 123511995 987 832 2146 3", "TOTAL 123511994 987 832 2146 3" + ) + with self.assertRaisesRegex(ValueError, "coverage total"): + v.audit_census(mutant, self.data) + with self.assertRaisesRegex(ValueError, "line capacity"): + v.audit_census("", self.data) + + def test_missing_direction_and_mutated_cut(self): + lines = self.raw.splitlines() + position = next(i for i, line in enumerate(lines) if line.startswith("POS ")) + parts = lines[position].split() + parts[1] = str(int(parts[1]) + 1) + lines[position] = " ".join(parts) + with self.assertRaisesRegex(ValueError, "positive list capacity"): + v.audit_census("\n".join(lines), self.data) + parts = self.raw.splitlines()[position].split() + parts[3] = str((1 << 64) - 1) + lines[position] = " ".join(parts) + with self.assertRaisesRegex(ValueError, "deletion cut"): + v.audit_census("\n".join(lines), self.data) + + def test_unanchored_rank_five_control(self): + actual = v.unanchored_control(self.data) + self.assertEqual(actual["rank"], 5) + self.assertEqual( + json.loads(json.dumps(actual)), self.result["unanchored_control"] + ) + + def test_fourteen_anchor_extension_is_false(self): + actual = v.fourteen_control(self.data) + self.assertEqual(actual["rank"], 5) + self.assertGreater(actual["cut_union_size"], 14) + mutant = self.work / "fourteen-mutant.json" + control = copy.deepcopy(actual["witness"]) + control["anchor"]["cut"] = [0, 0] + mutant.write_text(json.dumps(control)) + with self.assertRaisesRegex(ValueError, "residual rank"): + v.fourteen_control(self.data, mutant) + + def test_new_beta_shape_and_remaining_shape(self): + actual = v.beta_application() + self.assertEqual(actual["nonbasis_weights"], [4, 6, 6, 6, 6]) + self.assertEqual(actual["support_cap"], 52) + self.assertEqual(actual["remaining_from_PR3162"], [2, 5, 5, 5, 6, 6, 6, 6, 6]) + self.assertEqual( + actual["forced_direction_rank"] - actual["finite_upper_bound"], 2 + ) + + def test_source_binding_and_exact_inventory(self): + root = self.work / "source-control" + package = root / "research/p112-mixed-rank-anchor" + package.mkdir(parents=True) + shutil.copytree(v.PACKAGE / "vendor", package / "vendor") + shutil.copyfile(v.PACKAGE / "SOURCES.json", package / "SOURCES.json") + for name in v.INPUTS: + target = root / name + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes((v.ROOT / name).read_bytes()) + self.assertEqual(v.bound_sources(root, package), self.result["sources"]) + path = package / "vendor/geometry.py" + path.write_bytes(path.read_bytes() + b"\n") + with self.assertRaisesRegex(ValueError, "changed source"): + v.bound_sources(root, package) + path.write_bytes((v.PACKAGE / "vendor/geometry.py").read_bytes()) + target = root / v.INPUTS[0] + target.write_bytes(target.read_bytes() + b"\n") + with self.assertRaisesRegex(ValueError, "changed source"): + v.bound_sources(root, package) + + def test_receipt_mismatch_fails_cli(self): + package = self.work / "receipt-control/research/p112-mixed-rank-anchor" + shutil.copytree(v.PACKAGE, package) + for name in v.INPUTS: + target = package.parent.parent / name + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes((v.ROOT / name).read_bytes()) + receipt = copy.deepcopy(self.result) + receipt["census"]["total"]["max_span"] = 4 + (package / "RESULT.json").write_text(json.dumps(receipt)) + env = os.environ | {"PYTHONDONTWRITEBYTECODE": "1"} + result = subprocess.run( + [os.sys.executable, "-B", str(package / "verify.py")], + env=env, + capture_output=True, + text=True, + timeout=180, + ) + self.assertNotEqual(result.returncode, 0) + self.assertIn("receipt mismatch", result.stderr) + + def test_compiled_anchor_and_coverage_mutants(self): + source = (v.PACKAGE / "scan.cpp").read_text() + mutants = ( + ("size <= budget + 4", "size <= budget + 5", "--self-test"), + ("ri < reps.size()", "ri + 1 < reps.size()", None), + ) + for index, (before, after, mode) in enumerate(mutants): + package = self.work / f"native-mutant-{index}" + package.mkdir() + (package / "vendor").mkdir() + shutil.copyfile( + v.PACKAGE / "vendor/census.cpp", package / "vendor/census.cpp" + ) + self.assertEqual(source.count(before), 1) + (package / "scan.cpp").write_text(source.replace(before, after)) + binary = v.build(package, package) + args = [str(binary), str(self.path)] + ([mode] if mode else []) + result = subprocess.run(args, capture_output=True, text=True, timeout=180) + if mode: + self.assertEqual(result.returncode, 2) + self.assertIn("oracle disagrees", result.stderr) + else: + self.assertEqual(result.returncode, 0) + with self.assertRaises(ValueError): + v.audit_census(result.stdout, self.data) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/p112-mixed-rank-anchor/vendor/LICENSE b/research/p112-mixed-rank-anchor/vendor/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/p112-mixed-rank-anchor/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-mixed-rank-anchor/vendor/NOTICE.md b/research/p112-mixed-rank-anchor/vendor/NOTICE.md new file mode 100644 index 0000000000..a64c562db1 --- /dev/null +++ b/research/p112-mixed-rank-anchor/vendor/NOTICE.md @@ -0,0 +1,14 @@ +# Retained source boundary + +`PREDECESSOR-NOTICE.md` is copied verbatim from Nick Petalas's PR3162 at +`ebd7fd275288e4a9f658e77fa77a0119a8322e74`. It describes that predecessor, +including files not copied here. This package retains only the six files in +`SOURCES.json.retained_files`. Their exact origin paths, blobs and SHA256 hashes +are recorded there and their working bytes are authenticated during replay. + +The original TWOSIDE reduction and its predecessor attribution belong to +DreamingOfClouds, PR3154 at `708f0ad8928c383de8294aea3c126e9461d2066d`. +The flat/orbit and rank-six oracle lineage includes Nick Petalas's PR3161 at +`a1aba8389b87412e6f72ccf4d11f31e0ea232327`. All retained source is Apache-2.0; +`LICENSE` is copied unchanged. No credit for that work is claimed as a new result +in this successor. diff --git a/research/p112-mixed-rank-anchor/vendor/PR3162-PROOF.md b/research/p112-mixed-rank-anchor/vendor/PR3162-PROOF.md new file mode 100644 index 0000000000..fb45b45d0c --- /dev/null +++ b/research/p112-mixed-rank-anchor/vendor/PR3162-PROOF.md @@ -0,0 +1,196 @@ +# Ten deletions at residual rank six + +Use the pinned P112 label map `ell(t)` into `F2^9` and doubled E8 root +representatives `r_t` in `Q^8`. Write + +``` +Lambda(V) = {t : ell(t) belongs to V} +Off(h) = {t : r_t dot h != 0}. +``` + +## The finite theorem + +For every pair of six-dimensional binary label spaces `V1,V2`, let `H` be +the projective directions for which there is a separately chosen set `D_h` +of at most ten P112 lines such that + +``` +rank_F2 ell(Off(h) \ (Lambda(V1) union Lambda(V2) union D_h)) <= 6. +``` + +Then `dim span(H) <= 4` over the reals and every characteristic-zero field. +Four is attained with separate deletion sets. The upper bound also holds +when one common deletion set is required. Common-set attainment is not +claimed. There can be ten qualifying projective directions; a bound of four +on their count would be false. + +The proof combines the direction-completeness argument below with an exact +finite census. It is a finite geometric theorem, not a multiplication theorem. + +## Complete direction coverage + +The native replay enumerates all 788,035 three-dimensional annihilators in +`F2^9`. Their kernels are all six-dimensional label spaces. It verifies that +every six-flat contains at most twenty P112 lines. A residual set of binary +rank at most six extends into a six-flat, so every admissible direction has + +``` +|Off(h)| <= 20 + 20 + 10 + 20 = 70. +``` + +At least 42 of the 112 live root lines, and therefore at least 42 of the +120 E8 root lines, are perpendicular to `h`. + +Here is a finite specialization of the usual Weyl-chamber argument. The +displayed eight simple roots in `geometry.py` form an E8 simple system. +Exact coordinates verify that every one of the 120 root lines is positive +or negative in that basis. In a closed Weyl chamber, the perpendicular roots +are generated by the simple roots on which the direction vanishes. For a +face with at most six vanishing simple roots, enlarge that set to six. +The replay checks all 28 such six-node subsets and finds at most 36 root +lines. Thus at least 42 perpendicular lines force exactly seven vanishing +simple roots. The direction is one of eight fundamental-weight rays, up to +the Weyl group. + +The eight ray counts are `42,28,22,14,16,23,37,63`. Only the first and last +can qualify. Closing their projective directions under the eight exact simple +reflections gives 1,080 D7 normals and 120 E7/root normals. Closure is checked, +with a hard capacity of 1,200. The actual P112 support cutoff of seventy +retains 128 D7 normals and all 120 root normals, hence 248 candidates. In +particular, extending the predecessor's root-only direction list would have +left an unproved completeness step. + +The same catalogue certifies the code distance 53 used below. Any direction +of smaller support would meet the cutoff of seventy and hence appear in the +catalogue, whose minimum support is 53. Root directions attain that minimum. + +For an arbitrary characteristic-zero field, the rational root vectors +perpendicular to `h` have rational rank at most seven. They cannot have rank +at most six: a generic real normal to their span would give a perpendicular +root system of rank at most six with at least 42 lines, contradicting the +six-node check. Their rational kernel is therefore one-dimensional. The +field-valued `h` is proportional to a rational generator of that kernel. +Apply the real chamber argument to this generator. Ranks of the resulting +rational direction vectors are unchanged by scalar extension. + +This argument uses the standard Weyl-chamber theorem for a finite root +system. It is not a proof-kernel formalization of that theorem. + +## Pair coverage and rank-preserving symmetries + +The 788,035 flats give 776,805 distinct nonempty P112 masks. Empty masks +cannot qualify a direction: one remaining covering flat, one residual flat +and ten deletions contain at most fifty lines, below the minimum nonzero +P112 support of 53. + +The twelve pinned generators are checked to be binary-label linear and to +permute all 248 direction support masks. For a span bound, support closure +alone does not justify reducing pairs by symmetry. The new signed-Gram check +also assigns signs to all 112 root lines and verifies every pair's Gram +entry after permutation. The P112 root vectors span `Q^8`. Equal Gram +matrices therefore define an invertible rational orthogonal map realizing +each signed permutation. The map carries `Off(h)` to the permuted support +of the transformed direction and preserves rational direction rank. + +Union-find under these checked generators gives 159 first-flat orbits. +One representative from each orbit, paired with every second mask, covers +all pairs. This is 123,511,995 representative pairs. The replay retains +every orbit row; a prefix or inconsistent total is rejected. + +For a fixed first flat, a direction is screened out only if its remaining +support exceeds fifty. For a pair, it is screened out only if its remaining +support exceeds thirty. These are necessary size inequalities from the +twenty-line residual-flat bound and ten-line deletion budget. Every surviving +test is decided by the exact oracle below. No floating-point decision occurs. + +The complete ten-deletion result is span at most four, at most ten directions, +525,718 positive pairs and 16,975,961 deletion-oracle calls. The eight-deletion +control reproduces span three and at most three directions. + +## Deletion and rational-rank oracles + +The deletion oracle is retained from PR3161. If a residual label set has +rank `r>6`, put `k=r-6`, which is at most three. A deletion of at most `p` +lines leaves rank at most six exactly when `k` independent words of the +restricted binary character code have support union at most `p`. In one +direction, take independent annihilating forms of the retained span. In the +other, retain their common kernel. Enumerating all 511 nonzero ambient +characters and deduplicating their restricted words implements the quotient +by the annihilator of the residual span. Every chosen word has weight at +most `p`. Distinct nonzero words are pairwise independent; three are +independent exactly when the third is not the XOR of the first two. + +The native self-test compares all 4,096 subsets of a twelve-line fixture +with literal exhaustive deletion, at every budget zero through ten. This +gives 45,056 comparisons. Positive witnesses retain actual cuts, separately +checked in Python using explicit XOR closure. + +Rational direction rank uses integer elimination, with each row divided by +its coordinate gcd. Stored entries have absolute value at most `10^9`; +each multiplication/subtraction is bounded by `2*10^18`, inside signed +64-bit range. The post-division bound is checked after every reduction; +exhaustion fails rather than returning a rank. Python Fraction elimination +checks 248 literal catalogue triples independently. A determinant-minus-two +triple distinguishes rational rank from binary rank, and its dependent +mutation is a separate control. The sharp witnesses have independently +checked rational ranks three and four. + +## One newly excluded beta shape + +Retain the pinned TWOSIDE low-piece hypotheses. Let `B` be a basis of pieces, +`T=span(B)`, `C` the P112 root code, and `d=dim(T intersect C)>=b`. Every +nonzero element of `C` has support at least 53. Write `|B|=rho+b`. + +If `rho` chosen pieces have combined support below 53, their images in +`T/(T intersect C)` are independent: a nonzero combination cannot be a +codeword with so small a support. The quotient has dimension at most `rho`, +so these images form a quotient basis and `d=b`. + +For each nonbasis piece `q_y`, subtract the unique combination of quotient +basis pieces with the same quotient image. This gives a nonzero element +`c_y` of `C`, supported on the chosen pieces and `q_y`. The `b` elements +`c_y` are independent because their coordinates on the nonbasis elements +of `B` are distinct unit vectors. This proves the fundamental-circuit step +used in the predecessor; the map from directions to `C` is injective since +the live roots span eight dimensions. + +In `(b,t)=(5,4)`, the newly excluded weight multiset is + +``` +B: 2,4,5,6,6,6,6,6,6 +X0: 2,4,5,6 +``` + +Here `rho=4`, and the chosen support cap is `2+8+12+20=42<53`. +The weight-five and weight-six supports lie in two six-flats. The weight-two +and weight-four supports supply one common deletion set of at most ten +lines. Every nonbasis piece has weight six, so the five independent +fundamental-circuit directions all satisfy the finite theorem. Its span +bound of four is a contradiction. + +This exclusion does not depend on the inherited weight-five capacity twelve. +Alternatively choose `X0=(2,4,6,6)`. Since every P112 label has first bit one, +a rank-two or rank-four flat has at most two or eight live labels. Together +with the replayed six-flat capacity twenty, the support cap is fifty, still +below 53. The complement has weights `5,6,6,6,6`, all at most six, and the +same ten-line deletion argument applies. + +The new weight enumeration reproduces the pinned 15 BK/BK7 survivors over +all 4,795 weight multisets of lengths five through nine. The preceding +eight-deletion theorem excludes twelve. The ten-deletion theorem excludes +exactly the additional shape above under this covering rule, leaving + +``` +2,5,5,5,6,6,6,6,6 +3,4,4,6,6,6,6,6,6. +``` + +The minimum extra-line budgets certified by weight-based two-six-flat covers +are ten for the newly excluded shape and fourteen/twelve for the two +remainders. These minima do not rule out covers exploiting the actual +pieces' overlaps. The full weight-cap and necessary-feasibility filter ledger +is inherited from TWOSIDE, not independently re-proved here; the new exclusion +has the alternative capacity argument above. The conservative replacement +of zero-excess weights by two can only enlarge the covers and remains valid +for the exclusions. This is one additional beta exclusion, not full C5 or +`C(P112)>=64`, a supplier admission or a new kappa. diff --git a/research/p112-mixed-rank-anchor/vendor/PREDECESSOR-NOTICE.md b/research/p112-mixed-rank-anchor/vendor/PREDECESSOR-NOTICE.md new file mode 100644 index 0000000000..227999aa6e --- /dev/null +++ b/research/p112-mixed-rank-anchor/vendor/PREDECESSOR-NOTICE.md @@ -0,0 +1,13 @@ +# Source notice + +The TWOSIDE notes and bk2b.py are byte-identical excerpts from +DreamingOfClouds's PR3154 at 708f0ad8928c383de8294aea3c126e9461d2066d. +They retain the original reduction and predecessor credit. PR3161-PROOF.md +is Nick Petalas's proof from PR3161 at a1aba8389b87412e6f72ccf4d11f31e0ea232327. +All are Apache-2.0, with the repository license retained here. + +The successor's census.cpp reuses PR3161's flat enumeration, orbit machinery +and dual-code deletion oracle. geometry.py reuses its root/label reconstruction. +The new work adds Weyl-chamber direction completeness, signed-Gram symmetry, +exact rational-span accounting and the ten-deletion beta application. +UPSTREAM.json records the original paths, commits, blobs and hashes. diff --git a/research/p112-mixed-rank-anchor/vendor/TWOSIDE.md b/research/p112-mixed-rank-anchor/vendor/TWOSIDE.md new file mode 100644 index 0000000000..e3fd3f2b1d --- /dev/null +++ b/research/p112-mixed-rank-anchor/vendor/TWOSIDE.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-mixed-rank-anchor/vendor/census.cpp b/research/p112-mixed-rank-anchor/vendor/census.cpp new file mode 100644 index 0000000000..6e33b5c713 --- /dev/null +++ b/research/p112-mixed-rank-anchor/vendor/census.cpp @@ -0,0 +1,389 @@ +// Rank-six ten-deletion census. Apache-2.0. +// Flat/orbit enumeration and the dual-code oracle descend from Nick Petalas, +// PR3161 a1aba8389b87412e6f72ccf4d11f31e0ea232327. Rational-span accounting +// and the E7/D7 direction fixture are added in this successor. +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +using U = std::uint64_t; +using Vector = std::array; +using Basis = std::array; +using Found = std::array; +struct Mask { + U lo = 0, hi = 0; + bool operator==(const Mask &x) const { return lo == x.lo && hi == x.hi; } + bool operator<(const Mask &x) const { return lo < x.lo || (lo == x.lo && hi < x.hi); } +}; +Mask operator|(Mask a, Mask b) { return {a.lo | b.lo, a.hi | b.hi}; } +Mask operator&(Mask a, Mask b) { return {a.lo & b.lo, a.hi & b.hi}; } +Mask operator^(Mask a, Mask b) { return {a.lo ^ b.lo, a.hi ^ b.hi}; } +Mask minus(Mask a, Mask b) { return {a.lo & ~b.lo, a.hi & ~b.hi}; } +int count(Mask a) { return __builtin_popcountll(a.lo) + __builtin_popcountll(a.hi); } +bool has(Mask a, int i) { return i < 64 ? ((a.lo >> i) & 1U) : ((a.hi >> (i - 64)) & 1U); } +void set(Mask &a, int i) { if (i < 64) a.lo |= U{1} << i; else a.hi |= U{1} << (i - 64); } +constexpr Mask ALL{~U{0}, (U{1} << 48) - 1}; +struct Data { + std::array labels{}; + std::array vectors{}; + std::array off{}; + std::array, 12> generators{}; + std::array parity{}; +}; + +Data read_data(const char *path) { + std::ifstream input(path); + if (!input) throw std::runtime_error("cannot read fixture"); + Data data; + std::array used{}; + for (int &x : data.labels) { + if (!(input >> x) || x < 1 || x > 511 || used[static_cast(x)]) + throw std::runtime_error("invalid label"); + used[static_cast(x)] = true; + } + for (Vector &v : data.vectors) { + std::int64_t norm = 0; + for (auto &x : v) { + if (!(input >> x) || x < -3 || x > 3) throw std::runtime_error("invalid coordinate"); + norm += x * x; + } + if (norm < 1 || norm > 16) throw std::runtime_error("invalid direction norm"); + } + for (Mask &m : data.off) { + if (!(input >> m.lo >> m.hi) || (m.hi >> 48) || (count(m) != 53 && count(m) != 56 && count(m) != 70)) + throw std::runtime_error("invalid support"); + } + for (auto &g : data.generators) { + std::array seen{}; + for (int &x : g) { + if (!(input >> x) || x < 0 || x >= 112 || seen[static_cast(x)]) + throw std::runtime_error("invalid permutation"); + seen[static_cast(x)] = true; + } + } + std::string trailing; + if (input >> trailing) throw std::runtime_error("trailing fixture input"); + for (int x = 0; x < 512; ++x) + for (int i = 0; i < 112; ++i) + if (__builtin_parity(static_cast(x & data.labels[static_cast(i)]))) + set(data.parity[static_cast(x)], i); + return data; +} + +void sort_masks(Mask *rows, Mask *scratch, std::size_t n) { + if (n > 788035) throw std::runtime_error("sort capacity"); + std::size_t width = 1; + for (int pass = 0; pass < 20; ++pass) { + if (width >= n) return; + for (std::size_t start = 0; start < n; start += 2 * width) { + const std::size_t middle = std::min(start + width, n); + const std::size_t end = std::min(start + 2 * width, n); + std::size_t left = start, right = middle; + for (std::size_t out = start; out < end; ++out) { + if (left < middle && (right == end || !(rows[right] < rows[left]))) scratch[out] = rows[left++]; + else scratch[out] = rows[right++]; + } + } + for (std::size_t i = 0; i < n; ++i) rows[i] = scratch[i]; + width *= 2; + } + if (width < n) throw std::runtime_error("sort pass bound"); +} + +std::vector flats(const Data &data) { + std::vector result; + result.reserve(788035); + std::size_t matrices = 0; + for (int p = 0; p < 7; ++p) for (int q = p + 1; q < 8; ++q) + for (int r = q + 1; r < 9; ++r) { + std::array pivot{p, q, r}; + std::array, 3> free{}; + std::array lengths{}; + int nfree = 0; + for (int i = 0; i < 3; ++i) for (int c = 0; c < pivot[static_cast(i)]; ++c) + if (c != p && c != q && c != r) { + free[static_cast(i)][static_cast(lengths[static_cast(i)]++)] = c; + ++nfree; + } + if (nfree > 18) throw std::runtime_error("RREF capacity"); + for (unsigned code = 0; code < (1U << nfree); ++code) { + unsigned bits = code; + Mask excluded{}; + for (int i = 0; i < 3; ++i) { + int row = 1 << pivot[static_cast(i)]; + for (int j = 0; j < lengths[static_cast(i)]; ++j) { + if (bits & 1U) row |= 1 << free[static_cast(i)][static_cast(j)]; + bits >>= 1; + } + excluded = excluded | data.parity[static_cast(row)]; + } + ++matrices; + const Mask mask = minus(ALL, excluded); + if (count(mask)) result.push_back(mask); + } + } + if (matrices != 788035) throw std::runtime_error("RREF coverage"); + std::vector scratch(result.size()); + sort_masks(result.data(), scratch.data(), result.size()); + result.erase(std::unique(result.begin(), result.end()), result.end()); + for (Mask m : result) if (count(m) > 20) throw std::runtime_error("six-flat cap"); + return result; +} + +std::size_t root(std::vector &parent, std::size_t i) { + for (std::size_t step = 0; step < parent.size(); ++step) { + if (parent[i] == i) return i; + parent[i] = parent[parent[i]]; + i = parent[i]; + } + throw std::runtime_error("union-find cycle"); +} + +using Tables = std::array, 14>, 12>; +Tables permutation_tables(const Data &data) { + Tables tables{}; + for (int g = 0; g < 12; ++g) for (int byte = 0; byte < 14; ++byte) + for (int v = 0; v < 256; ++v) for (int bit = 0; bit < 8; ++bit) + if ((v >> bit) & 1) set(tables[static_cast(g)][static_cast(byte)][static_cast(v)], + data.generators[static_cast(g)][static_cast(byte * 8 + bit)]); + return tables; +} + +std::vector representatives(const Data &data, const std::vector &space) { + const Tables tables = permutation_tables(data); + std::vector parent(space.size()); + std::iota(parent.begin(), parent.end(), std::size_t{0}); + for (std::size_t i = 0; i < space.size(); ++i) for (int g = 0; g < 12; ++g) { + Mask image{}; + for (int byte = 0; byte < 14; ++byte) { + const U value = byte < 8 ? space[i].lo >> (8 * byte) : space[i].hi >> (8 * (byte - 8)); + image = image | tables[static_cast(g)][static_cast(byte)][static_cast(value & 255)]; + } + const auto found = std::lower_bound(space.begin(), space.end(), image); + if (found == space.end() || !(*found == image)) throw std::runtime_error("orbit leaves flats"); + const std::size_t j = static_cast(found - space.begin()); + const std::size_t a = root(parent, i), b = root(parent, j); + if (a != b) parent[a] = b; + } + std::vector reps; + for (std::size_t i = 0; i < space.size(); ++i) if (root(parent, i) == i) reps.push_back(i); + if (reps.size() != 159) throw std::runtime_error("orbit coverage"); + return reps; +} + +int binary_rank(const Data &data, Mask mask) { + std::array basis{}; + int rank = 0; + for (int i = 0; i < 112; ++i) if (has(mask, i)) { + int x = data.labels[static_cast(i)]; + for (int bit = 8; bit >= 0; --bit) if ((x >> bit) & 1) { + if (basis[static_cast(bit)]) x ^= basis[static_cast(bit)]; + else { basis[static_cast(bit)] = x; ++rank; break; } + } + } + return rank; +} + +bool deletable(const Data &data, Mask mask, int budget, Mask *cut = nullptr) { + const int need = binary_rank(data, mask) - 6; + if (need <= 0) { if (cut) *cut = {}; return true; } + std::array words{}; + std::size_t n = 0; + for (int x = 1; x < 512; ++x) { + const Mask word = mask & data.parity[static_cast(x)]; + if (count(word) > 0 && count(word) <= budget) words[n++] = word; + } + std::array scratch{}; + sort_masks(words.data(), scratch.data(), n); + n = static_cast(std::unique(words.begin(), words.begin() + static_cast(n)) - words.begin()); + if (need == 1) { if (n && cut) *cut = words[0]; return n > 0; } + for (std::size_t a = 0; a < n; ++a) for (std::size_t b = a + 1; b < n; ++b) { + const Mask joined = words[a] | words[b]; + if (count(joined) > budget) continue; + if (need == 2) { if (cut) *cut = joined; return true; } + for (std::size_t c = b + 1; c < n; ++c) + if (!(words[c] == (words[a] ^ words[b])) && count(joined | words[c]) <= budget) { + if (cut) *cut = joined | words[c]; + return true; + } + } + return false; +} + +bool insert_vector(Basis &basis, Vector row) { + for (std::size_t col = 0; col < 8; ++col) { + if (!row[col]) continue; + if (!basis[col][col]) { basis[col] = row; return true; } + const auto a = basis[col][col], b = row[col]; + // Every stored entry has absolute value <= 10^9. Thus each intermediate + // is <= 2*10^18 in absolute value, strictly inside signed 64-bit range. + for (std::size_t j = col; j < 8; ++j) row[j] = a * row[j] - b * basis[col][j]; + std::int64_t divisor = 0; + for (auto x : row) divisor = std::gcd(divisor, x); + if (divisor) for (auto &x : row) x /= divisor; + for (auto x : row) if (x > 1000000000LL || x < -1000000000LL) + throw std::runtime_error("rational-rank capacity"); + } + return false; +} + +int rational_rank(const Data &data, const Found &found, int n) { + if (n < 0 || n > 248) throw std::runtime_error("direction-count capacity"); + Basis basis{}; + int rank = 0; + for (int i = 0; i < n; ++i) { + const int h = found[static_cast(i)]; + if (h < 0 || h >= 248) throw std::runtime_error("direction index"); + if (insert_vector(basis, data.vectors[static_cast(h)])) ++rank; + } + return rank; +} + +void emit_witness(const Data &data, Mask first, Mask second, + const Found &found, int n, int budget) { + Basis basis{}; + Found independent{}; + int rank = 0; + for (int i = 0; i < n; ++i) { + const int h = found[static_cast(i)]; + if (insert_vector(basis, data.vectors[static_cast(h)])) + independent[static_cast(rank++)] = h; + } + std::cout << "WITNESS " << first.lo << ' ' << first.hi << ' ' << second.lo << ' ' << second.hi << ' ' << rank; + for (int i = 0; i < rank; ++i) { + const int h = independent[static_cast(i)]; + Mask cut{}; + if (!deletable(data, minus(minus(data.off[static_cast(h)], first), second), budget, &cut)) + throw std::runtime_error("lost deletion witness"); + std::cout << ' ' << h << ' ' << cut.lo << ' ' << cut.hi; + } + std::cout << '\n'; +} + +void census(const Data &data, const std::vector &space, + const std::vector &reps, int budget, std::size_t limit) { + std::cout << "flats " << space.size() << " reps " << reps.size() << " budget " << budget << '\n'; + int global_max = 0, global_span = 0; + U calls = 0, positives = 0; + bool have_witness = false; + for (std::size_t ri = 0; ri < std::min(limit, reps.size()); ++ri) { + const Mask first = space[reps[ri]]; + std::array residual{}; + std::array directions{}; + std::size_t nactive = 0; + for (int h = 0; h < 248; ++h) { + const Mask rest = minus(data.off[static_cast(h)], first); + if (count(rest) <= 40 + budget) { directions[nactive] = h; residual[nactive++] = rest; } + } + int maximum = 0, maxspan = 0; + U hits = 0; + for (std::size_t j = 0; j < space.size(); ++j) { + int qualifying = 0; + Found found{}; + for (std::size_t a = 0; a < nactive; ++a) { + const Mask rest = minus(residual[a], space[j]); + if (count(rest) > 20 + budget) continue; + ++calls; + if (deletable(data, rest, budget)) found[static_cast(qualifying++)] = directions[a]; + } + maximum = std::max(maximum, qualifying); + const int span = rational_rank(data, found, qualifying); + maxspan = std::max(maxspan, span); + if (qualifying) ++hits; + if (!have_witness && span >= (budget == 8 ? 3 : 4)) { + have_witness = true; + emit_witness(data, first, space[j], found, qualifying, budget); + } + } + global_max = std::max(global_max, maximum); + global_span = std::max(global_span, maxspan); + positives += hits; + std::cout << "rep " << ri << " flat " << reps[ri] << " lines " << count(first) + << " maxspan " << maxspan << " active " << nactive << " maxdirs " << maximum << " positive_pairs " << hits << '\n'; + std::cout.flush(); + } + std::cout << "TOTAL maxdirs " << global_max << " maxspan " << global_span << " positive_pairs " << positives << " oracle_calls " << calls << '\n'; +} + +void self_test(const Data &data) { + std::array indices{}; + Mask selected{}; + int n = 0; + for (int i = 0; i < 112; ++i) { + Mask trial = selected; + set(trial, i); + if (binary_rank(data, trial) > binary_rank(data, selected)) { + indices[static_cast(n++)] = i; + selected = trial; + } + } + if (n != 9) throw std::runtime_error("label rank control"); + for (int i = 0; i < 112 && n < 12; ++i) if (!has(selected, i)) { + indices[static_cast(n++)] = i; + set(selected, i); + } + if (n != 12) throw std::runtime_error("test capacity"); + std::array masks{}; + std::array ranks{}; + for (unsigned code = 0; code < 4096; ++code) { + for (int bit = 0; bit < 12; ++bit) if ((code >> bit) & 1U) + set(masks[code], indices[static_cast(bit)]); + ranks[code] = binary_rank(data, masks[code]); + } + U checks = 0; + for (unsigned code = 0; code < 4096; ++code) { + int minimum = 12; + for (unsigned keep = 0; keep < 4096; ++keep) + if (!(keep & ~code) && ranks[keep] <= 6) + minimum = std::min(minimum, __builtin_popcount(code) - __builtin_popcount(keep)); + for (int p = 0; p <= 10; ++p) { + Mask cut{}; + const bool answer = deletable(data, masks[code], p, &cut); + if (answer != (minimum <= p) || (answer && (count(cut) > p || binary_rank(data, minus(masks[code], cut)) > 6))) + throw std::runtime_error("dual-code oracle disagrees with exhaustive deletions"); + ++checks; + } + } + std::cout << "PASS_ORACLE " << checks << " subsets 4096 budgets 11\n"; +} + +int parse_integer(const char *argument) { + const std::string text(argument); + std::size_t used = 0; + const int value = std::stoi(text, &used); + if (used != text.size()) throw std::runtime_error("invalid integer"); + return value; +} + +int main(int argc, char **argv) { + try { + if (argc < 3 || argc > 11) throw std::runtime_error("usage: census FIXTURE BUDGET [LIMIT] | --rank INDEX..."); + const Data data = read_data(argv[1]); + if (std::string(argv[2]) == "--self-test" && argc == 3) { self_test(data); return 0; } + if (std::string(argv[2]) == "--rank" && argc >= 4) { + Found found{}; + for (int i = 3; i < argc; ++i) found[static_cast(i - 3)] = parse_integer(argv[i]); + std::cout << "RANK " << rational_rank(data, found, argc - 3) << '\n'; + return 0; + } + if (argc > 4) throw std::runtime_error("too many census arguments"); + const int budget = parse_integer(argv[2]); + if (budget != 8 && budget != 10) throw std::runtime_error("budget must be 8 or 10"); + const int parsed_limit = argc == 4 ? parse_integer(argv[3]) : 159; + if (parsed_limit < 1 || parsed_limit > 159) throw std::runtime_error("invalid orbit limit"); + const auto space = flats(data); + const auto reps = representatives(data, space); + census(data, space, reps, budget, static_cast(parsed_limit)); + return 0; + } catch (const std::exception &error) { + std::cerr << error.what() << '\n'; + return 2; + } +} diff --git a/research/p112-mixed-rank-anchor/vendor/geometry.py b/research/p112-mixed-rank-anchor/vendor/geometry.py new file mode 100644 index 0000000000..3579fa6a78 --- /dev/null +++ b/research/p112-mixed-rank-anchor/vendor/geometry.py @@ -0,0 +1,296 @@ +"""Exact P112 data and Weyl-chamber direction coverage. + +Root/label reconstruction and generator checks descend from Nick Petalas's +PR3161, a1aba8389b87412e6f72ccf4d11f31e0ea232327, Apache-2.0. +The chamber rays and reflection closure are new here. +""" + +from fractions import Fraction +from itertools import combinations, product +from math import gcd, lcm +from pathlib import Path + +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 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) + if not divisor: + raise ValueError("zero projective direction") + return canonical(tuple(x // divisor for x in integers)) + + +def chamber_ray(omitted): + """The rational normal to seven of the eight simple roots.""" + matrix = [ + [Fraction(x) for x in row] for i, row in enumerate(SIMPLE) if i != omitted + ] + pivots = [] + for col in range(8): + rank = len(pivots) + pivot = next((i for i in range(rank, 7) if matrix[i][col]), None) + if pivot is None: + continue + matrix[rank], matrix[pivot] = matrix[pivot], matrix[rank] + scale = matrix[rank][col] + matrix[rank] = [x / scale for x in matrix[rank]] + for i in range(7): + if i != rank: + scale = matrix[i][col] + matrix[i] = [ + x - scale * y for x, y in zip(matrix[i], matrix[rank], strict=True) + ] + pivots.append(col) + if len(pivots) != 7: + raise ValueError("simple-root hyperplane rank") + free = next(col for col in range(8) if col not in pivots) + result = [Fraction(0)] * 8 + result[free] = Fraction(1) + for i, col in enumerate(pivots): + result[col] = -matrix[i][free] + return primitive(result) + + +def reflection(direction, root): + dot = sum(x * y for x, y in zip(direction, root, strict=True)) + return primitive( + tuple(Fraction(4 * x - dot * y) for x, y in zip(direction, root, strict=True)) + ) + + +def weyl_closure(seeds): + active = set(seeds) + pending = sorted(active) + for index in range(1200): + if index == len(pending): + break + for root in SIMPLE: + image = reflection(pending[index], root) + if image not in active: + if len(active) >= 1200: + raise ValueError("Weyl-orbit capacity") + active.add(image) + pending.append(image) + if len(active) != 1200 or any( + reflection(h, r) not in active for h in active for r in SIMPLE + ): + raise ValueError("incomplete Weyl closure") + return active + + +def direction_catalogue(): + """All projective directions with at least 42 perpendicular E8 lines.""" + roots = root_lines() + coefficients = tuple(simple_coefficients(r) for r in roots) + if any( + not (all(x >= 0 for x in c) or all(x <= 0 for x in c)) for c in coefficients + ): + raise ValueError("roots are not positive or negative in the simple basis") + six_counts = tuple( + sum(all(c[i] == 0 for i in omitted) for c in coefficients) + for omitted in combinations(range(8), 2) + ) + if max(six_counts) != 36: + raise ValueError("rank-six parabolic capacity") + rays = tuple(chamber_ray(i) for i in range(8)) + zero_counts = tuple( + sum(sum(x * y for x, y in zip(h, r, strict=True)) == 0 for r in roots) + for h in rays + ) + active = weyl_closure( + h for h, count in zip(rays, zero_counts, strict=True) if count >= 42 + ) + counts = {42: 0, 63: 0} + points = tuple(row for row in roots if row not in frame_lines()) + selected = [] + for h in sorted(active): + zeros = sum(sum(x * y for x, y in zip(h, r, strict=True)) == 0 for r in roots) + if zeros not in counts: + raise ValueError("unexpected perpendicular root system") + counts[zeros] += 1 + off = sum(bool(sum(x * y for x, y in zip(h, r, strict=True))) for r in points) + if off <= 70: + selected.append(h) + if counts != {42: 1080, 63: 120} or len(selected) != 248: + raise ValueError("direction inventory") + return tuple(selected), { + "rank_six_parabolic_counts": six_counts, + "chamber_zero_counts": zero_counts, + "weyl_directions": 1200, + "e7": 120, + "d7": 1080, + "retained": 248, + } + + +def root_lines(): + roots = set() + for i, j in combinations(range(8), 2): + for a, b in product((-2, 2), repeat=2): + row = [0] * 8 + row[i], row[j] = a, b + 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)) + if len(roots) != 120: + raise ValueError("E8 root inventory") + 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 simple_coefficients(row): + matrix = [ + [Fraction(SIMPLE[j][i]) for j in range(8)] + [Fraction(row[i])] + for i in range(8) + ] + for col in range(8): + pivot = next((i for i in range(col, 8) if matrix[i][col]), None) + if pivot is None: + raise ValueError("singular E8 basis") + matrix[col], matrix[pivot] = matrix[pivot], matrix[col] + scale = matrix[col][col] + matrix[col] = [x / scale for x in matrix[col]] + for i in range(8): + if i != col: + scale = matrix[i][col] + matrix[i] = [ + x - scale * y for x, y in zip(matrix[i], matrix[col], strict=True) + ] + coefficients = [matrix[i][8] for i in range(8)] + if any(x.denominator != 1 for x in coefficients): + raise ValueError("nonintegral E8 coordinates") + return tuple(int(x) for x in coefficients) + + +def exact_label(row): + return 1 | sum((x % 2) << (i + 1) for i, x in enumerate(simple_coefficients(row))) + + +def permute(mask, permutation): + return sum(1 << permutation[i] for i in range(112) if mask >> i & 1) + + +def signed_gram(points, permutation): + """Certify that a line permutation lifts to a rational orthogonal map.""" + signs = [0] * 112 + signs[0] = 1 + pending = [0] + for index in range(112): + if index == len(pending): + break + i = pending[index] + for j in range(112): + before = sum(x * y for x, y in zip(points[i], points[j], strict=True)) + after = sum( + x * y + for x, y in zip( + points[permutation[i]], points[permutation[j]], strict=True + ) + ) + if abs(before) != abs(after): + raise ValueError("line permutation changes absolute Gram matrix") + if before: + proposed = signs[i] * (before // after) + if signs[j] and signs[j] != proposed: + raise ValueError("inconsistent Gram signs") + if not signs[j]: + signs[j] = proposed + pending.append(j) + if len(pending) != 112: + raise ValueError("disconnected nonorthogonality graph") + return signs.count(-1) + + +def validate_generators(labels, supports, generators): + support_set = set(supports) + for permutation in generators: + if sorted(permutation) != list(range(112)): + raise ValueError("invalid line permutation") + basis = [0] * 9 + images = [0] * 9 + for index, label in enumerate(labels): + value, image = label, labels[permutation[index]] + for bit in range(8, -1, -1): + if value >> bit & 1: + if basis[bit]: + value ^= basis[bit] + image ^= images[bit] + else: + basis[bit], images[bit] = value, image + break + if value == 0 and image != 0: + raise ValueError("nonlinear label permutation") + if any(permute(mask, permutation) not in support_set for mask in supports): + raise ValueError("permutation fails root-support closure") + + +def fixture(data_path, generators_path): + roots, frame = root_lines(), frame_lines() + points = tuple(row for row in roots if row not in frame) + labels = tuple(exact_label(row) for row in points) + with Path(data_path).open() as stream: + source_labels = tuple(map(int, stream.readline().split())) + source_frame = tuple(map(int, stream.readline().split())) + source_points = tuple( + tuple(map(int, stream.readline().split())) for _ in range(112) + ) + if ( + source_labels != labels + or source_points != points + or source_frame != tuple(exact_label(row) for row in frame) + ): + raise ValueError("predecessor label/coordinate binding") + directions, coverage = direction_catalogue() + supports = tuple( + sum( + 1 << i + for i, row in enumerate(points) + if sum(x * y for x, y in zip(row, direction, strict=True)) + ) + for direction in directions + ) + if ( + sorted(mask.bit_count() for mask in supports) + != [53] * 112 + [56] * 8 + [70] * 128 + ): + raise ValueError("direction-support cardinalities") + generators = tuple( + tuple(map(int, line.split())) + for line in Path(generators_path).read_text().splitlines() + ) + if len(generators) != 12: + raise ValueError("generator count") + validate_generators(labels, supports, generators) + coverage["orthogonal_generator_negative_signs"] = tuple( + signed_gram(points, g) for g in generators + ) + lines = [" ".join(map(str, labels))] + lines += [" ".join(map(str, row)) for row in directions] + lines += [f"{mask & ((1 << 64) - 1)} {mask >> 64}" for mask in supports] + lines += [" ".join(map(str, row)) for row in generators] + return "\n".join(lines) + "\n", coverage diff --git a/research/p112-mixed-rank-anchor/verify.py b/research/p112-mixed-rank-anchor/verify.py new file mode 100644 index 0000000000..e66ab4df0f --- /dev/null +++ b/research/p112-mixed-rank-anchor/verify.py @@ -0,0 +1,519 @@ +"""Replay a mixed-rank P112 theorem and the 3,4^2,6^6 beta exclusion.""" + +import argparse +import hashlib +import json +import os +import shutil +import subprocess +import tempfile +from fractions import Fraction +from itertools import combinations +from pathlib import Path + +from vendor.geometry import chamber_ray, fixture, frame_lines, root_lines, weyl_closure + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +INPUTS = ( + "research/one-sided-six-multisets/data/data.txt", + "research/one-sided-six-multisets/data/gens.txt", +) +FLAGS = ( + "-std=c++17", + "-O3", + "-Wall", + "-Wextra", + "-Wpedantic", + "-Wconversion", + "-Wsign-conversion", + "-Wshadow", + "-Werror", +) + + +def checked(condition, message): + if not condition: + raise ValueError(message) + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def bound_sources(root=ROOT, package=PACKAGE): + manifest = json.loads((package / "SOURCES.json").read_text()) + inputs = [row for row in manifest["files"] if row["usage"] == "input"] + checked( + sorted(row["path"] for row in inputs) == sorted(INPUTS), "live input inventory" + ) + retained = manifest["retained_files"] + checked(len(retained) == 6, "retained input inventory") + hashes = {} + for row, path in [(r, root / r["path"]) for r in inputs] + [ + (r, package / r["copy"]) for r in retained + ]: + checked(path.is_file() and path.stat().st_size <= 2_000_000, "source capacity") + actual = digest(path.read_bytes()) + checked(actual == row["sha256"], "changed source: " + str(path)) + hashes[row.get("copy", row.get("path"))] = actual + return hashes + + +def run(argv, work, name, timeout=180): + output = work / name + with output.open("w") as stream: + subprocess.run( + argv, + check=True, + timeout=timeout, + stdout=stream, + stderr=subprocess.STDOUT, + cwd=ROOT, + ) + checked(output.stat().st_size <= 2_000_000, "native output capacity") + return output.read_text() + + +def build(work, package=PACKAGE): + compiler = shutil.which("c++") + checked(compiler is not None, "a C++17 compiler is required") + binary = work / "scan" + run( + [compiler, *FLAGS, str(package / "scan.cpp"), "-o", str(binary)], + work, + "build.txt", + 60, + ) + return binary + + +def binary_span(values): + result = {0} + for value in values: + result |= {x ^ value for x in result} + return result + + +def binary_rank(values): + basis = [0] * 9 + for value in values: + for bit in range(8, -1, -1): + if value >> bit & 1: + if basis[bit]: + value ^= basis[bit] + else: + basis[bit] = value + break + return sum(bool(x) for x in basis) + + +def rational_rank(rows): + checked(len(rows) <= 248 and all(len(r) == 8 for r in rows), "matrix capacity") + matrix = [[Fraction(x) for x in row] for row in rows] + rank = 0 + for col in range(8): + pivot = next((i for i in range(rank, len(matrix)) if matrix[i][col]), None) + if pivot is None: + continue + matrix[rank], matrix[pivot] = matrix[pivot], matrix[rank] + scale = matrix[rank][col] + matrix[rank] = [x / scale for x in matrix[rank]] + for i in range(rank + 1, len(matrix)): + scale = matrix[i][col] + matrix[i] = [ + x - scale * y for x, y in zip(matrix[i], matrix[rank], strict=True) + ] + rank += 1 + return rank + + +def parse_fixture(text): + lines = text.splitlines() + checked(len(lines) == 509, "fixture coverage") + labels = tuple(map(int, lines[0].split())) + directions = tuple(tuple(map(int, line.split())) for line in lines[1:249]) + off = tuple( + lo | hi << 64 for lo, hi in (map(int, s.split()) for s in lines[249:497]) + ) + checked(len(labels) == 112 and all(x & 1 for x in labels), "odd labels") + parity = tuple( + sum(1 << i for i, x in enumerate(labels) if (x & a).bit_count() % 2) + for a in range(512) + ) + return labels, directions, off, parity + + +def values(mask, labels): + checked(0 <= mask < 1 << 112, "mask capacity") + return [x for i, x in enumerate(labels) if mask >> i & 1] + + +def flat_check(mask, labels): + span = binary_span(values(mask, labels)) + checked(len(span) <= 64, "not a six-flat mask") + checked( + mask == sum(1 << i for i, x in enumerate(labels) if x in span), + "flat not closed", + ) + + +def check_cut(rest, cut, target, labels, budget=12): + checked(type(budget) is int and 0 <= budget <= 14, "cut budget capacity") + checked( + 0 <= cut < 1 << 112 and not cut & ~rest and cut.bit_count() <= budget, + "invalid deletion cut", + ) + checked(binary_rank(values(rest & ~cut, labels)) <= target, "residual rank failed") + + +def anchor_oracle(rest, labels, budget=12): + """Independent explicit binary spans, rather than the native odd-XOR formula.""" + selected = values(rest, labels) + checked(len(selected) <= 20, "anchor oracle capacity") + if len(selected) <= budget: + return True + for subset in combinations(selected, min(4, len(selected))): + span = binary_span(subset) + if sum(x not in span for x in selected) <= budget: + return True + return False + + +def six_oracle(rest, labels, parity): + need = binary_rank(values(rest, labels)) - 6 + if need <= 0: + return True + words = sorted({word for p in parity if 0 < (word := p & rest).bit_count() <= 12}) + if need == 1: + return bool(words) + for a, b in combinations(words, 2): + joined = a | b + if joined.bit_count() > 12: + continue + if need == 2: + return True + if any( + c not in (a, b, a ^ b) and (joined | c).bit_count() <= 12 for c in words + ): + return True + return False + + +def positive_check(parts, first, second, data): + labels, directions, off, parity = data + checked(parts[0] == "POS", "missing positive list") + n = int(parts[1]) + checked(1 <= n <= 248 and len(parts) == 2 + 3 * n, "positive list capacity") + listed = [] + for index in range(n): + h, lo, hi = map(int, parts[2 + 3 * index : 5 + 3 * index]) + checked(0 <= h < 248 and lo >= 0 and hi >= 0, "direction or cut capacity") + check_cut(off[h] & ~(first | second), lo | hi << 64, 6, labels) + listed.append(h) + screened = [h for h in range(248) if (off[h] & ~(first | second)).bit_count() <= 32] + expected = [ + h for h in screened if six_oracle(off[h] & ~(first | second), labels, parity) + ] + checked(listed == expected, "rank-six direction inventory disagrees") + rank = rational_rank([directions[h] for h in listed]) + checked(rank <= 3, "mixed-rank span theorem failed") + return rank, listed, len(screened) + + +def anchor_check(parts, expected_row, data): + checked( + parts and parts[0] == "ANCHOR" and len(parts) == 11, "invalid anchor record" + ) + ri, j, flo, fhi, slo, shi, h, answer, clo, chi = map(int, parts[1:]) + checked( + ri == expected_row and 0 <= j < 776805 and 0 <= h < 248 and answer in (0, 1), + "anchor record range", + ) + checked(min(flo, fhi, slo, shi, clo, chi) >= 0, "negative mask component") + first, second, cut = flo | fhi << 64, slo | shi << 64, clo | chi << 64 + labels, _, off, _ = data + flat_check(first, labels) + flat_check(second, labels) + rest = off[h] & ~(first | second) + checked(bool(answer) == anchor_oracle(rest, labels), "rank-four oracle disagrees") + if answer: + check_cut(rest, cut, 4, labels) + else: + checked(cut == 0, "negative answer has a cut") + proof = { + "first": [flo, fhi], + "second": [slo, shi], + "anchor": h, + "anchor_cut": [clo, chi], + } + return answer, first, second, proof + + +def audit_census(text, data): + lines = text.splitlines() + checked(2 <= len(lines) <= 10_000, "census line capacity") + checked(lines[0] == "COVER 776805 159", "flat/orbit coverage") + rows, anchors, positives, witness = [], 0, 0, None + cursor, maximum, calls = 1, 0, 0 + row_tests, row_hits, row_span = 0, 0, 0 + _, directions, _, _ = data + while cursor < len(lines) - 1: + parts = lines[cursor].split() + cursor += 1 + if parts[0] == "ROW": + row = list(map(int, parts[1:])) + checked( + len(row) == 6 and row[0] == len(rows), "missing or duplicate orbit row" + ) + checked( + row[3:] == [row_span, row_tests, row_hits], "inconsistent orbit row" + ) + rows.append(row) + row_tests, row_hits, row_span = 0, 0, 0 + continue + answer, first, second, proof = anchor_check(parts, len(rows), data) + anchors += 1 + row_tests += 1 + if not answer: + continue + checked(cursor < len(lines) - 1, "missing positive record") + rank, listed, pair_calls = positive_check( + lines[cursor].split(), first, second, data + ) + cursor += 1 + positives += 1 + row_hits += 1 + calls += pair_calls + row_span = max(row_span, rank) + maximum = max(maximum, rank) + if rank == 3 and witness is None: + witness = proof | { + "directions": listed, + "vectors": [directions[x] for x in listed], + "rank": rank, + } + total = census_total(lines[-1], rows, anchors, positives, maximum) + checked(total["rank_six_oracle_calls"] == calls, "oracle call count disagrees") + checked(witness is not None, "missing sharp-span witness") + return { + "rows": rows, + "total": total, + "witness": witness, + "native_stdout_sha256": digest(text.encode()), + "independent_anchor_checks": anchors, + "independent_positive_pairs": positives, + } + + +def census_total(line, rows, anchors, positives, maximum): + parts = line.split() + checked(len(parts) == 6 and parts[0] == "TOTAL", "malformed total") + pairs, tests, hits, calls, span = map(int, parts[1:]) + checked( + len(rows) == 159 and len({r[1] for r in rows}) == 159, + "incomplete first-flat coverage", + ) + checked( + all( + 0 <= r[1] < 776805 + and 1 <= r[2] <= 20 + and 0 <= r[3] <= 3 + and 0 <= r[5] <= r[4] + for r in rows + ), + "orbit row range", + ) + checked( + pairs == 123511995 + and tests == anchors == sum(r[4] for r in rows) + and hits == positives == sum(r[5] for r in rows) + and span == maximum == max(r[3] for r in rows) == 3 + and calls >= hits, + "inconsistent coverage total", + ) + return { + "pairs": pairs, + "anchor_tests": tests, + "positive_pairs": hits, + "rank_six_oracle_calls": calls, + "max_span": span, + } + + +def beta_application(): + weights = (3, 4, 4, 6, 6, 6, 6, 6, 6) + quotient_basis = (3, 4, 6, 6) + complement = list(weights) + for weight in quotient_basis: + complement.remove(weight) + checked(complement == [4, 6, 6, 6, 6], "wrong nonbasis weights") + support_cap = 4 + 8 + 20 + 20 + checked( + support_cap < 53 and len(complement) > 3, "fundamental-circuit contradiction" + ) + return { + "cell": [5, 4], + "weights": weights, + "quotient_basis": quotient_basis, + "support_cap": support_cap, + "common_deletion_cap": 12, + "nonbasis_weights": complement, + "forced_direction_rank": 5, + "finite_upper_bound": 3, + "remaining_from_PR3162": [2, 5, 5, 5, 6, 6, 6, 6, 6], + } + + +def mixed_direction_coverage(data): + points = tuple(r for r in root_lines() if r not in frame_lines()) + checked(rational_rank(points) == 8, "P112 characteristic-zero rank") + orbit = weyl_closure((chamber_ray(0), chamber_ray(7))) + histogram, selected = {}, set() + for h in orbit: + support = sum( + bool(sum(x * y for x, y in zip(h, r, strict=True))) for r in points + ) + histogram[support] = histogram.get(support, 0) + 1 + if support <= 72: + selected.add(h) + checked(histogram == {53: 112, 56: 8, 70: 128, 73: 896, 76: 56}, "mixed cutoff gap") + checked(selected == set(data[1]), "incomplete mixed direction catalogue") + return { + "support_cutoff": 72, + "required_perpendicular_lines": 40, + "orbit_support_histogram": sorted(histogram.items()), + "retained": len(selected), + } + + +def unanchored_control(data): + witness = ( + 298398672570286131, + 52776760246272, + 516232, + 28051596928, + 5, + 2, + 162762907430420484, + 8797703766112, + 7, + 108508605669441600, + 8800924893472, + 221, + 1152930301523001344, + 3367275333632, + 230, + 18577350611437568, + 8830453975040, + 246, + 86704654336, + 73701659770888, + ) + labels, directions, off, _ = data + first, second = witness[0] | witness[1] << 64, witness[2] | witness[3] << 64 + flat_check(first, labels) + flat_check(second, labels) + indices = [] + for offset in range(5, len(witness), 3): + h, lo, hi = witness[offset : offset + 3] + check_cut(off[h] & ~(first | second), lo | hi << 64, 6, labels) + indices.append(h) + checked( + rational_rank([directions[h] for h in indices]) == 5, "unanchored control rank" + ) + return {"source": "PR3162 WITNESS_12", "witness": witness, "rank": 5} + + +def fourteen_control(data, path=PACKAGE / "CONTROL14.json"): + control = json.loads(path.read_text()) + labels = data[0] + points = tuple(r for r in root_lines() if r not in frame_lines()) + first = control["first"][0] | control["first"][1] << 64 + second = control["second"][0] | control["second"][1] << 64 + flat_check(first, labels) + flat_check(second, labels) + checked(len(control["directions"]) == 5, "fourteen control capacity") + union, vectors = 0, [] + for row, target in [(control["anchor"], 5)] + [ + (r, 6) for r in control["directions"] + ]: + vector = row["vector"] + checked( + len(vector) == 8 + and any(vector) + and all(type(x) is int and abs(x) <= 3 for x in vector), + "fourteen direction capacity", + ) + rest = sum( + 1 << i + for i, root in enumerate(points) + if sum(x * y for x, y in zip(vector, root, strict=True)) + ) & ~(first | second) + cut = row["cut"][0] | row["cut"][1] << 64 + check_cut(rest, cut, target, labels, 14) + union |= cut + if target == 6: + vectors.append(vector) + checked(rational_rank(vectors) == 5, "fourteen control direction rank") + checked(union.bit_count() > 14, "fourteen control unexpectedly has a common cut") + return {"witness": control, "rank": 5, "cut_union_size": union.bit_count()} + + +def solve(work): + hashes = bound_sources() + text, coverage = fixture(*(ROOT / name for name in INPUTS)) + data = parse_fixture(text) + mixed_coverage = mixed_direction_coverage(data) + path = work / "fixture.txt" + path.write_text(text) + binary = build(work) + control = run([str(binary), str(path), "--self-test"], work, "oracle.txt") + checked( + control == "PASS_ORACLES 109239 exhaustive20 1048576\n", + "oracle control coverage", + ) + raw = run([str(binary), str(path)], work, "census.txt") + audit = audit_census(raw, data) + return { + "status": "PASS_P112_MIXED_RANK_ANCHOR", + "sources": hashes, + "fixture_sha256": digest(text.encode()), + "coverage": coverage, + "mixed_direction_coverage": mixed_coverage, + "oracle_comparisons": 109239, + "census": audit, + "unanchored_control": unanchored_control(data), + "fourteen_control": fourteen_control(data), + "beta": beta_application(), + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--work", type=Path, help="new external diagnostics directory") + parser.add_argument( + "--output", type=Path, help="new receipt, otherwise compare RESULT.json" + ) + args = parser.parse_args() + checked(args.output is None or not args.output.exists(), "output already exists") + if args.work: + work = args.work.resolve() + checked(not work.is_relative_to(ROOT), "work directory must be external") + work.mkdir(parents=True, exist_ok=False) + result = solve(work) + else: + with tempfile.TemporaryDirectory( + prefix="p112-anchor-", dir=os.environ.get("TMPDIR") + ) as temporary: + result = solve(Path(temporary)) + serialized = json.dumps(result, indent=2) + "\n" + if args.output: + args.output.write_text(serialized) + else: + checked(serialized == (PACKAGE / "RESULT.json").read_text(), "receipt mismatch") + print("PASS_P112_MIXED_RANK_ANCHOR span=3 pinned_beta_exclusions=1") + + +if __name__ == "__main__": + main()