diff --git a/research/complex-rank8-rigidity-p109/PROOF.md b/research/complex-rank8-rigidity-p109/PROOF.md new file mode 100644 index 0000000000..0b47464209 --- /dev/null +++ b/research/complex-rank8-rigidity-p109/PROOF.md @@ -0,0 +1,66 @@ +# Rank-8 rigidity on every P109 unit + +Notation, (E), equations (2), (E0), (E2), and Lemmas 2–8 are those of PR1212 +(`research/complex-rank8-decoder-rigidity/PROOF.md` at head `57099cb5`). Lemma 9 and the "Step 1" argument are +those of PR1399 (`research/complex-rank8-rigidity-p104-admissible/PROOF.md` at head `4e1ba3a1`). Lemma 10 and the +coverage rule are those of PR1419 (`research/complex-rank8-rigidity-extension/PROOF.md` at head `81b8997b`). +The per-unit argument is PR1425's (`research/complex-rank8-rigidity-p110-odd/PROOF.md` at head `4b707c22`), +applied to 19 new units. Finite facts marked **[X]** are recomputed by this package's `verify.py` (check id `X`; +`u` is one of `u01`, …, `u19`). + +**Theorem.** Let X be a 3-subset of P112 and L = P112 \ X. Let K be an L × L matrix over a field of +characteristic 0 with rank K ≤ 8 that satisfies (E). Then K = D (2 G_L) D⁻¹ for an invertible diagonal D. + +**Corollary.** In the E-graph model, every decoder with exactly eight costly terms on a P109 unit has +cst ≥ 61 = 72 − 11. This is PR968's Theorem 4(b) with p = 11, reached through PR1212 §8 verbatim. + +## Reduction to 19 units + +Let H be the group generated by `verify.py`'s 8 generators, each a reflection or a product of two reflections +fixing FRAME0 **[model.generators]**. Its orbits split the 227920 triples of P112 into 24 classes, and whether +a triple lies in a frame inside P112 is constant on each class **[census.triples]**: + +- **5 orbits, 29232 triples, inside a P112 frame.** PR1419's coverage rule applies, so these units are rigid by + PR1419's Theorem, which cites the P104 units of PR1212, PR1389 and PR1399. +- **19 orbits, 198688 triples, not inside one.** 18 of them contain an odd pair; one, of 1792 triples, is + pairwise orthogonal **[census.open-orbits]**. + +Using a subgroup is sound. The orbits can only be finer than those of the full stabiliser, and PR1212 §10 transport +needs only some Weyl element carrying one unit onto another. The 24 orbits match the full stabiliser's count, +which an independent implementation found as well (see README). `UNITS.json` lists one representative per open +orbit, the first triple of each in line order **[units.cover]**, with its pinned pivot frame F inside L. + +## Per-unit argument + +For each representative, the following facts are checked **[u.rigid]**: + +- PR1212 Lemma 2's D4 facts relative to F; +- PR1212's (I3) on every complete class, with live witnesses; +- PR1212's (I4): all 14 blocks carry a complete class, and complete classes glue through every shared pivot pair; +- PR1399's Lemma 9 connectivity for every non-pivot live line outside a complete class, with the sign identity + for every witness; +- **(I2) zero exclusion**: the zero-pattern CNF of PR1425 (families *two*, *four*, *diag*, *trans*), with the + clause "some pattern variable is true", is refuted by the DRUP proof in `PROOFS.json.gz`. That proof is + replayed by `verify.py`'s own two-watched-literal RUP checker and fails without that clause; +- exact rational cross-checks of Lemma 9's rank-3 systems and of the §7 assembly on all 109 live lines; +- the gauge pattern satisfies the CNF. + +Between 18 and 24 classes are complete, depending on the unit, and Lemma 9 carries the remaining 5–29 lines. + +The proof is then PR1425's verbatim: + +- **Step 1** (PR1399): Lemma 5 on each complete class and Lemma 6 on the set of complete classes give the gauge form + a_jf = d′_j ε_jf g_f and b_jf = 4 (d′_j g_f)⁻¹ ε_jf on those lines. +- **Step 2:** Lemma 9 extends that form to every other non-pivot live line. +- **Assembly:** PR1212 §7 gives K = D (2G) D⁻¹. + +Transport carries the result to every triple in the orbit. ∎ + +## Counting + +| triples X of P112 | orbits | triples | rigid by | +|---|---:|---:|---| +| inside a P112 frame | 5 | 29232 | PR1419 (Lemma 10 from P104) | +| not inside, pairwise orthogonal | 1 | 1792 | this package | +| not inside, with an odd pair | 18 | 196896 | this package | +| total | 24 | 227920 | | diff --git a/research/complex-rank8-rigidity-p109/PROOFS.json.gz b/research/complex-rank8-rigidity-p109/PROOFS.json.gz new file mode 100644 index 0000000000..ad242c9b4c Binary files /dev/null and b/research/complex-rank8-rigidity-p109/PROOFS.json.gz differ diff --git a/research/complex-rank8-rigidity-p109/README.md b/research/complex-rank8-rigidity-p109/README.md new file mode 100644 index 0000000000..96fcd45099 --- /dev/null +++ b/research/complex-rank8-rigidity-p109/README.md @@ -0,0 +1,98 @@ +# Rank-8 masked decoders are gauge-rigid on every P109 unit (no new κ) + +**Status: scoped structural result. No κ claim, no construction.** It continues the rank-8 rigidity line of +PR1212 (burntout76, open, head `57099cb5`), PR1399 (`4e1ba3a1`), PR1419 (`81b8997b`) and PR1425 (`4b707c22`). It +answers PR1425's open next question. + +PR1419's extension lemma makes P112 minus X rigid whenever X lies inside a frame of P112. For |X| = 3 that leaves +198688 of the 227920 triples. Under the FRAME0 stabiliser they form 19 orbits: 18 contain an odd pair, and one +(1792 triples) is pairwise orthogonal but extends to no P112 frame. This package proves rigidity on all 19 with +PR1425's per-unit method ([PROOF.md](PROOF.md)): + +- a pivot frame passing PR1212's (I3) and (I4) with gluing; +- PR1399's Lemma 9 connectivity for the lines outside complete classes; +- a new DRUP refutation of the zero-pattern CNF for (I2) zero exclusion, with 1595 to 2945 lemmas per unit. + +**Consequence.** With PR1419, every P109 unit (P112 minus any three lines) is rigid. Every decoder with exactly +eight costly terms in the E-graph model there has cst ≥ 61, which is PR968's 72 − p at p = 11. + +## Reproduce + +From the repository root, Python 3.10+, standard library only, about 15 s: + +```sh +python3 -I -B research/complex-rank8-rigidity-p109/verify.py +``` + +Expected final line: + +```text +PASS_COMPLEX_RANK8_RIGIDITY_P109: checks 25; all 19 open P109 orbits (198688 triples) rigid; with PR1419 every P109 unit is rigid; floor 61 +``` + +`verify.py` is self-contained: + +- **Census.** It recomputes the orbit census of triples and the inside-a-frame split, and checks that the units + hit each open orbit once. +- **Per unit.** It checks the pivot conditions, builds each CNF itself and replays the 19 proofs from + `PROOFS.json.gz` with its own RUP checker. It pins the SHA256 of each decompressed proof and each CNF. +- **Controls.** The gauge pattern satisfies each CNF. Each proof fails without the "some entry vanishes" + clause. An empty-clause-only proof is rejected. + +`UNITS.json` and `PROOFS.json.gz` are regenerated in about 4 s by the command below, which needs python-sat +(python-sat 1.9.dev15, Glucose 4.1, used here). Deletion lines are dropped, since the checker ignores them. + +```sh +python3 -I -B research/complex-rank8-rigidity-p109/make_proof.py --out-dir /some/new/dir +``` + +Two one-time cross-checks were run but are not part of `verify.py`: + +- **PR1212's checker.** PR1212's `rup_check` at head `57099cb5` accepts all 19 proofs on this package's CNFs, + with the same lemma counts, and rejects every one without the zero clause. +- **Independent census.** A separately written census matches the orbit table exactly: 24 orbits and every + (size, odd pairs, inside-a-frame) triple. It was written from a specification only, by OpenAI Codex, and + computed |H| = 344064 with 2025 frames. +- **AI review.** A read-only adversarial review, also by OpenAI Codex, checked the CNF families, the lemma + hypotheses, subgroup coverage and the RUP checker, including 10000 random fuzz formulas. It found no soundness + gap. This is not a human review. + +## Not covered + +- **Inherited steps.** These are cited, not re-derived: + - PR1212's Lemmas 5–6, §7 assembly and §10 transport; + - PR1399's Lemma 9; + - PR1419's Lemma 10 with its P104 inputs, for the 29232 covered triples. + + All of these PRs are open. PR968's premise (F6) is inherited through the floor. Attainment of 61 is not + checked. +- **P108 and deeper.** The same method applies per orbit, but the open orbit count grows: 168 at |X| = 4 (see + below). +- **Nine or more costly terms.** +- The written proof has had no independent human review. There is no construction and no κ change, and every + condition of the selected record is unchanged. + +## Open next questions + +**P108: four-line punctures not inside a P112 frame.** + +- *Why it matters.* P109 is complete with this package. P108 is the next depth: 168 of 180 orbits, 6132952 of + 6210820 quadruples. Both counts were found by this package's code and independently by the census above. +- *A feasible first step.* A trial run of `make_proof.py`'s pivot rule and CNF on all 168 representatives found a + passing pivot and an unsatisfiable CNF for every one. That is 361027 lemmas, or about 5.9 MB gzipped. The run + was outside the package and is not certified here. +- *The blocker.* Shipping per-orbit proofs at that size, plus a pure-Python census of 6.2 million quadruples, is + heavy. Deeper levels grow further, and the bottom level P105 alone has on the order of 10⁵ orbits. A + structural replacement for the DRUP step (I2) would remove that growth. + +## Credit + +- **burntout76 / Brett Halligan (PR1212):** the theorem, (E), the CNF families of Lemmas 4 and 8 (reimplemented + here), the pivot reduction, Lemmas 5–6, §7 and the transport. +- **themilkman216 (PR968):** the floor 72 − p. +- **DreamingOfClouds (PR717):** the E-graph model. +- **PR1399, PR1419, PR1425 (JosieElliston):** Lemma 9, the extension lemma with its coverage rule, and the per-unit + pipeline. + +Prepared by JosieElliston with substantial assistance from Claude Opus 5.5 (Anthropic) via Claude Code, covering +the proof, verifier and write-up. OpenAI Codex independently recomputed the orbit census and reviewed the package. Apache-2.0. diff --git a/research/complex-rank8-rigidity-p109/SOURCES.json b/research/complex-rank8-rigidity-p109/SOURCES.json new file mode 100644 index 0000000000..178b3ca979 --- /dev/null +++ b/research/complex-rank8-rigidity-p109/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "410026dc5513b87db92ae98571d1d5984c69a983", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + } + ] +} diff --git a/research/complex-rank8-rigidity-p109/TASK.json b/research/complex-rank8-rigidity-p109/TASK.json new file mode 100644 index 0000000000..d88faa817e --- /dev/null +++ b/research/complex-rank8-rigidity-p109/TASK.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "task_id": "complex-masked-decoder", + "priority_revision": 2, + "base_commit": "410026dc5513b87db92ae98571d1d5984c69a983", + "original_card": { + "id": "complex-masked-decoder", + "question": "Can one specified masked or overcomplete decoder improve the complete moment budget?", + "starting_points": [ + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "methods": [ + "Synthesize a decoder with exact coefficients and fully priced helper endpoints.", + "Bound the best possible budget for a fixed support alphabet before synthesis." + ], + "acceptance_gate": "Change an assumption of the eight-term all-pairs bound and count all copied information, frames and restoration.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-decoder-field-extension-seed44/verify.py" + ], + "expected": "PASS_COMPLEX_DECODER_FIELD_EXTENSION_S44", + "inspect": "Locate the excluded classes: masked identities, at least nine terms, and deeper punctures.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one finite support alphabet and test exact decoding constraints before building a whole network.", + "bottleneck_link": "A cheaper fully realized decoder could increase deficit or lower recursive cost on the binding complex side.", + "allowed_variations": [ + "Select a specific masked or overcomplete family with exact labels and supports." + ], + "scope_change_triggers": [ + "Repeating the exact eight-term all-pairs search inside its proved scope." + ], + "overlap_terms": [ + "masked decoder", + "overcomplete", + "eight-term" + ] + }, + "scope_status": "refined", + "actual_scope": "Proof obligation inside the masked (E-graph) model: is every rank-<=8 solution of PR1212's system (E) on P112 minus X, for the 198688 triples X not inside a P112 frame (the part of P109 that PR1419's extension lemma cannot reach), equal to D(2G)D^-1, so that decoders with exactly eight costly terms keep PR968's floor 61 on every P109 unit?", + "scope_change_reason": "The card asks whether a masked decoder can beat the floor. PR1212/PR1389/PR1399 answered it for exactly eight costly terms on P120, P112, P111 and every P104 frame complement, PR1419 for punctures inside a frame, and PR1425 for the rest of P110; PR1425's open next question is P109. This closes it; it does not construct a decoder.", + "bottleneck_link": "Side result on the binding complex supplier: masked eight-costly-term decoders cannot beat PR968's floor on any P109 unit, so the remaining masked escape routes are nine or more costly terms or punctures of depth four or more not inside a frame.", + "budget_minutes": 60, + "stop_rule": "Stop at P109 with one PR; P108 (168 open orbits, trial run only) and deeper punctures, and nine or more costly terms, are left as handoffs.", + "outcome": "completed", + "evidence": "verify.py: 25 exact checks in about 15 s (generators; triple orbit census with the inside-a-frame split; one unit per open orbit; per unit the pivot's D4 structure, (I3), (I4) and gluing, Lemma 9 connectivity and algebra, assembly, CNF consistency, DRUP replay of zero exclusion with its own RUP checker and the needs-zero-clause control; one bogus-proof control). PR1212's rup_check independently accepts all 19 proofs, and an independently written census (OpenAI Codex, from a specification) matches the orbit table (both recorded, not run by verify.py); a read-only adversarial review by OpenAI Codex found no soundness gap (not a human review).", + "author": "JosieElliston (with Claude Opus 5.5 via Claude Code)", + "ai_assistance": "Claude Opus 5.5 via Claude Code: proof, verifier, CNF/RUP reimplementation and write-up. OpenAI Codex: independent orbit census from a specification and a read-only adversarial review. Submitted by the account holder.", + "open_questions": [ + { + "question": "Does rank-8 rigidity of (E) hold on P108 units P112 minus X, |X| = 4, where X is not inside a frame of P112 (168 of 180 orbits, 6132952 of 6210820 quadruples)?", + "why_it_matters": "With this package and PR1419 every P109 unit is rigid; P108 is the next depth of the eight-term gap in the masked model.", + "first_step": "A trial run of make_proof.py's pivot rule and CNF on all 168 representatives found a passing pivot and an UNSAT CNF for each (361027 lemmas, about 5.9 MB gzipped); package it with a census of 4-subsets.", + "blocked_by": "Proof volume and a pure-Python census of 6.2 million quadruples; orbit counts keep growing toward P105 (order 1e5 orbits), so a structural replacement for the DRUP zero-exclusion step is needed to go deep." + } + ] +} diff --git a/research/complex-rank8-rigidity-p109/UNITS.json b/research/complex-rank8-rigidity-p109/UNITS.json new file mode 100644 index 0000000000..019f2b685a --- /dev/null +++ b/research/complex-rank8-rigidity-p109/UNITS.json @@ -0,0 +1,2282 @@ +{ + "u01": { + "orbit_size": 672, + "triple": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + 0, + -2 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + 0, + 2 + ] + ], + "pivot": [ + [ + 0, + 0, + 0, + 2, + -2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2, + 2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + -2, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + 2, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + 0, + -2, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + 0, + 2, + 0 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + -2 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ] + ], + "proof_sha256": "d65b89d55aebd179a52b834d2c06f602c54db2b0f0011aff7938469276dfb7f0", + "cnf_sha256": "7a3daeeabbacd81c147b5937c892cacddaa449198cb4c8844b062aec0f6d38a9", + "lemmas": 1739 + }, + "u02": { + "orbit_size": 896, + "triple": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + -2, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + 0, + -2, + 0 + ] + ], + "pivot": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + -2 + ], + [ + 0, + 2, + -2, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + -1, + -1, + -1, + -1, + -1, + 1, + -1 + ], + [ + 1, + -1, + -1, + -1, + 1, + 1, + -1, + 1 + ], + [ + 1, + 1, + 1, + -1, + -1, + 1, + -1, + -1 + ], + [ + 1, + 1, + 1, + -1, + 1, + -1, + 1, + 1 + ], + [ + 2, + 0, + 0, + 2, + 0, + 0, + 0, + 0 + ] + ], + "proof_sha256": "34d520102288f5eae95620bfe2006cd8a457666687967d75e11c672b6d8bf747", + "cnf_sha256": "1bb9533b754445c30890bfa3e75a2ff3046a737741a9dc76ed4bb4ab94ecd96c", + "lemmas": 2241 + }, + "u03": { + "orbit_size": 896, + "triple": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + -2, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + 0, + 2, + 0 + ] + ], + "pivot": [ + [ + 1, + -1, + -1, + -1, + -1, + -1, + -1, + 1 + ], + [ + 1, + -1, + -1, + -1, + 1, + 1, + 1, + -1 + ], + [ + 1, + -1, + 1, + 1, + -1, + -1, + 1, + -1 + ], + [ + 1, + -1, + 1, + 1, + 1, + 1, + -1, + 1 + ], + [ + 1, + 1, + -1, + 1, + -1, + 1, + -1, + -1 + ], + [ + 1, + 1, + -1, + 1, + 1, + -1, + 1, + 1 + ], + [ + 1, + 1, + 1, + -1, + -1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + -1, + 1, + -1, + -1, + -1 + ] + ], + "proof_sha256": "9762cb6b65b1e78139f97132d24b67600a8e1ffb1897d3c817da250a8a9bed0e", + "cnf_sha256": "36d1e3db6c4daee7319a27439cdfbdfcd03e1eac7a0f043396d51288b319137e", + "lemmas": 2313 + }, + "u04": { + "orbit_size": 1792, + "triple": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + 0, + -2 + ], + [ + 0, + 2, + -2, + 0, + 0, + 0, + 0, + 0 + ] + ], + "pivot": [ + [ + 0, + 0, + 0, + 2, + -2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2, + 2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + -2, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + 2, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + 0, + -2, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + 0, + 2, + 0 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + -2 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ] + ], + "proof_sha256": "9e21960639b5807aa3eced75dc1b4b10f30e0c517f508dea91991a404baeb393", + "cnf_sha256": "dfe136eef26a943aa74ff463cc260e9675c77db8984932634df4f6aea55b1cd4", + "lemmas": 2439 + }, + "u05": { + "orbit_size": 1792, + "triple": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 2, + -2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + 0, + 0, + -2 + ] + ], + "pivot": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + -2 + ], + [ + 0, + 2, + -2, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + -1, + -1, + -1, + -1, + -1, + 1, + -1 + ], + [ + 1, + -1, + -1, + -1, + 1, + 1, + -1, + 1 + ], + [ + 1, + 1, + 1, + -1, + -1, + 1, + -1, + -1 + ], + [ + 1, + 1, + 1, + -1, + 1, + -1, + 1, + 1 + ], + [ + 2, + 0, + 0, + 2, + 0, + 0, + 0, + 0 + ] + ], + "proof_sha256": "e53338b0adb66c179291a8399733ad3558136dd8c7cec63234c8a7c7fc43afb5", + "cnf_sha256": "0c7ae980eb336bb68b03f6bcf0d8bdf81254d90221e6bcf75804a02f56a04797", + "lemmas": 1633 + }, + "u06": { + "orbit_size": 2688, + "triple": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + -2, + 0, + 0 + ] + ], + "pivot": [ + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + -2 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + 2 + ], + [ + 0, + 0, + 2, + 0, + 0, + 0, + -2, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + 0, + 2, + 0 + ], + [ + 0, + 2, + 0, + -2, + 0, + 0, + 0, + 0 + ], + [ + 0, + 2, + 0, + 2, + 0, + 0, + 0, + 0 + ], + [ + 2, + 0, + 0, + 0, + 0, + -2, + 0, + 0 + ], + [ + 2, + 0, + 0, + 0, + 0, + 2, + 0, + 0 + ] + ], + "proof_sha256": "8b40fd0a147f1a8c4ebfce4429f6473837f5bf9cd4aa3ad9642c8d6553e9814e", + "cnf_sha256": "fed6f6aed22b085d921dc17b627bd1d78c369dfae7481144664600887859002d", + "lemmas": 2269 + }, + "u07": { + "orbit_size": 3584, + "triple": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + -2, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + -2, + 0, + 0 + ] + ], + "pivot": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + -2 + ], + [ + 0, + 2, + -2, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + -1, + -1, + -1, + -1, + -1, + 1, + -1 + ], + [ + 1, + -1, + -1, + -1, + 1, + 1, + -1, + 1 + ], + [ + 1, + 1, + 1, + -1, + -1, + 1, + -1, + -1 + ], + [ + 1, + 1, + 1, + -1, + 1, + -1, + 1, + 1 + ], + [ + 2, + 0, + 0, + 2, + 0, + 0, + 0, + 0 + ] + ], + "proof_sha256": "8bb4cb8b0e63673741b4a140652068a49a43da877e624091418419c07399fc8d", + "cnf_sha256": "367fd182233855eaf5bc341ade7690e5084f81e498b9a159161f5049eb59d183", + "lemmas": 2162 + }, + "u08": { + "orbit_size": 5376, + "triple": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + 0, + -2 + ], + [ + 0, + 0, + 0, + 2, + -2, + 0, + 0, + 0 + ] + ], + "pivot": [ + [ + 0, + 0, + 0, + 2, + 0, + 0, + -2, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + 0, + 2, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + -2, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + 2, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + -2, + 0, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + 2, + 0, + 0, + 0 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + -2 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ] + ], + "proof_sha256": "2616c129c5ebd2f5cd6b6d0501038d7ba2ded22d1c514e960d3df005ff653071", + "cnf_sha256": "6661a477823f191bcc3480dc839d13d742130a2cbb3fc5a1afe38170695e8708", + "lemmas": 2884 + }, + "u09": { + "orbit_size": 5376, + "triple": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + 0, + -2 + ], + [ + 0, + 0, + 0, + 2, + 0, + -2, + 0, + 0 + ] + ], + "pivot": [ + [ + 0, + 0, + 0, + 2, + 0, + 0, + 0, + 2 + ], + [ + 0, + 0, + 2, + 0, + -2, + 0, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + -2, + 0, + 0 + ], + [ + 1, + -1, + -1, + -1, + -1, + -1, + -1, + 1 + ], + [ + 1, + -1, + 1, + 1, + 1, + -1, + -1, + -1 + ], + [ + 1, + 1, + -1, + 1, + -1, + 1, + -1, + -1 + ], + [ + 1, + 1, + 1, + -1, + 1, + 1, + -1, + 1 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + 2, + 0 + ] + ], + "proof_sha256": "5003c2a39002c788f6163c81b7c959ce2a57d3a5678784a5d9b816a66a00735c", + "cnf_sha256": "bd54818330646e1aafbc987389aed022f8665779d1ce6dfbed383706f437121f", + "lemmas": 1595 + }, + "u10": { + "orbit_size": 5376, + "triple": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 2, + -2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + 0, + -2, + 0 + ] + ], + "pivot": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + -2 + ], + [ + 0, + 2, + -2, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + -1, + -1, + -1, + -1, + -1, + 1, + -1 + ], + [ + 1, + -1, + -1, + -1, + 1, + 1, + -1, + 1 + ], + [ + 1, + 1, + 1, + -1, + -1, + 1, + -1, + -1 + ], + [ + 1, + 1, + 1, + -1, + 1, + -1, + 1, + 1 + ], + [ + 2, + 0, + 0, + 2, + 0, + 0, + 0, + 0 + ] + ], + "proof_sha256": "78402156717e46b8f9f3cc05c9f0715ff8c89fc0f6565a8db0ae4d601eca408d", + "cnf_sha256": "5bc3f2d00365305180395c914bbcc723595cbcb403a25bfddd4e246fcd11d24d", + "lemmas": 1795 + }, + "u11": { + "orbit_size": 5376, + "triple": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 2, + -2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + 0, + 0, + -2 + ] + ], + "pivot": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + 2 + ], + [ + 0, + 2, + -2, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + -1, + -1, + 1, + -1, + -1, + 1, + 1 + ], + [ + 1, + -1, + -1, + 1, + 1, + 1, + -1, + -1 + ], + [ + 1, + 1, + 1, + 1, + -1, + 1, + -1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + -1, + 1, + -1 + ], + [ + 2, + 0, + 0, + -2, + 0, + 0, + 0, + 0 + ] + ], + "proof_sha256": "a8a66cff888dc3ddc81c466cf8903a9d4dc6c99b295567de32c082da8e37148c", + "cnf_sha256": "9be1a9edee025f3c5511639d87c4cdd7be4380608ba272d80cd9a23271e71f91", + "lemmas": 2945 + }, + "u12": { + "orbit_size": 10752, + "triple": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + 0, + -2 + ], + [ + 0, + 0, + 0, + 2, + 0, + 0, + -2, + 0 + ] + ], + "pivot": [ + [ + 0, + 0, + 0, + 2, + -2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2, + 2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + -2, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + 2, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + 0, + -2, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + 0, + 2, + 0 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + -2 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ] + ], + "proof_sha256": "b105ba00aa9c4e3d2f34102346a713b9d7d63e2bf71d360528de752b14c44852", + "cnf_sha256": "d59891e4fad41c96436f36210bac492057e76ca66fc50a777d2eed9d3e4a1a28", + "lemmas": 2257 + }, + "u13": { + "orbit_size": 10752, + "triple": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 0 + ], + [ + 1, + -1, + -1, + -1, + -1, + -1, + -1, + 1 + ] + ], + "pivot": [ + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + -2 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + 2 + ], + [ + 0, + 0, + 0, + 2, + 0, + -2, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + 2, + 0, + 0 + ], + [ + 0, + 2, + -2, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 2, + 2, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + -2, + 0 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + 2, + 0 + ] + ], + "proof_sha256": "c3ffb8711a690b4ca28c970ac6fe45b5afb8b9ff51b7e3dfed251978f191864b", + "cnf_sha256": "87ddde313aaffa0d560ed24bbdbe75a8d70122bd5f6e69e0c17e0c1db5011ff3", + "lemmas": 1914 + }, + "u14": { + "orbit_size": 10752, + "triple": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 2, + -2, + 0, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + -2, + 0, + 0, + 0 + ] + ], + "pivot": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + -2 + ], + [ + 0, + 2, + -2, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + -1, + -1, + -1, + -1, + -1, + 1, + -1 + ], + [ + 1, + -1, + -1, + -1, + 1, + 1, + -1, + 1 + ], + [ + 1, + 1, + 1, + -1, + -1, + 1, + -1, + -1 + ], + [ + 1, + 1, + 1, + -1, + 1, + -1, + 1, + 1 + ], + [ + 2, + 0, + 0, + 2, + 0, + 0, + 0, + 0 + ] + ], + "proof_sha256": "ef65b1ab1c9f57efc4eb0355aadde1cd817351f8f0143dfb4d7a705d088ebc01", + "cnf_sha256": "f2914fc1138b96e56c9d627b5883dafcacf5891130c05ac2064fb726fec586ec", + "lemmas": 2070 + }, + "u15": { + "orbit_size": 10752, + "triple": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + -2, + 0, + 0 + ], + [ + 0, + 2, + 0, + -2, + 0, + 0, + 0, + 0 + ] + ], + "pivot": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + -2 + ], + [ + 0, + 2, + 0, + 2, + 0, + 0, + 0, + 0 + ], + [ + 1, + -1, + 1, + 1, + -1, + -1, + 1, + -1 + ], + [ + 1, + -1, + 1, + 1, + 1, + 1, + -1, + 1 + ], + [ + 1, + 1, + 1, + -1, + -1, + 1, + -1, + -1 + ], + [ + 1, + 1, + 1, + -1, + 1, + -1, + 1, + 1 + ], + [ + 2, + 0, + -2, + 0, + 0, + 0, + 0, + 0 + ] + ], + "proof_sha256": "10507b1e05f51c3ce8a2952fa8fb9a46247441d8ca5895cd2ddf7e93c0e35e75", + "cnf_sha256": "bef69b5311b222e766df51dd2aef6df8b0b4c90e81f44cff184b770fa9c1fbfd", + "lemmas": 1680 + }, + "u16": { + "orbit_size": 14336, + "triple": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + -2, + 0, + 0 + ], + [ + 1, + -1, + -1, + -1, + -1, + 1, + -1, + -1 + ] + ], + "pivot": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + -2 + ], + [ + 0, + 2, + 0, + 2, + 0, + 0, + 0, + 0 + ], + [ + 1, + -1, + 1, + 1, + -1, + -1, + 1, + -1 + ], + [ + 1, + -1, + 1, + 1, + 1, + 1, + -1, + 1 + ], + [ + 1, + 1, + 1, + -1, + -1, + 1, + -1, + -1 + ], + [ + 1, + 1, + 1, + -1, + 1, + -1, + 1, + 1 + ], + [ + 2, + 0, + -2, + 0, + 0, + 0, + 0, + 0 + ] + ], + "proof_sha256": "8a2dfd9dc4433291815c6e965461515e879c352b8000aff871ec94baec618549", + "cnf_sha256": "dcd374726ad477f3eeb3194c8bf3ee5625be115b19806192d699b3e819e6d2ab", + "lemmas": 1764 + }, + "u17": { + "orbit_size": 21504, + "triple": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 2, + -2, + 0, + 0, + 0 + ], + [ + 0, + 2, + 0, + -2, + 0, + 0, + 0, + 0 + ] + ], + "pivot": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + -2 + ], + [ + 0, + 2, + 0, + 2, + 0, + 0, + 0, + 0 + ], + [ + 1, + -1, + 1, + 1, + -1, + -1, + 1, + -1 + ], + [ + 1, + -1, + 1, + 1, + 1, + 1, + -1, + 1 + ], + [ + 1, + 1, + 1, + -1, + -1, + 1, + -1, + -1 + ], + [ + 1, + 1, + 1, + -1, + 1, + -1, + 1, + 1 + ], + [ + 2, + 0, + -2, + 0, + 0, + 0, + 0, + 0 + ] + ], + "proof_sha256": "e9c76b713684479b2e174ef0fab55a711941b64b0dd734c282593e133ebdd91c", + "cnf_sha256": "b70226b06d837f4b0177a7274662ff8e9e5453eccd869f376e7ff0a850fef76f", + "lemmas": 1663 + }, + "u18": { + "orbit_size": 43008, + "triple": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 2, + -2, + 0, + 0, + 0 + ], + [ + 1, + -1, + -1, + -1, + -1, + -1, + 1, + -1 + ] + ], + "pivot": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + -2 + ], + [ + 0, + 2, + 0, + 2, + 0, + 0, + 0, + 0 + ], + [ + 1, + -1, + 1, + 1, + -1, + 1, + -1, + -1 + ], + [ + 1, + -1, + 1, + 1, + 1, + -1, + 1, + 1 + ], + [ + 1, + 1, + 1, + -1, + -1, + -1, + 1, + -1 + ], + [ + 1, + 1, + 1, + -1, + 1, + 1, + -1, + 1 + ], + [ + 2, + 0, + -2, + 0, + 0, + 0, + 0, + 0 + ] + ], + "proof_sha256": "7918752b4dcf525101a98fee0b656a0cf4f14490387ffca3692c0a906cc48fb3", + "cnf_sha256": "e4250a18af2c3e7df08a149d858c62cb1255d9b80db44b17485fda1c4ea6d45e", + "lemmas": 2015 + }, + "u19": { + "orbit_size": 43008, + "triple": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 2, + -2, + 0, + 0, + 0 + ], + [ + 1, + -1, + -1, + -1, + 1, + -1, + 1, + 1 + ] + ], + "pivot": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + -2 + ], + [ + 0, + 2, + 0, + 2, + 0, + 0, + 0, + 0 + ], + [ + 1, + -1, + 1, + 1, + -1, + -1, + 1, + -1 + ], + [ + 1, + -1, + 1, + 1, + 1, + 1, + -1, + 1 + ], + [ + 1, + 1, + 1, + -1, + -1, + 1, + -1, + -1 + ], + [ + 1, + 1, + 1, + -1, + 1, + -1, + 1, + 1 + ], + [ + 2, + 0, + -2, + 0, + 0, + 0, + 0, + 0 + ] + ], + "proof_sha256": "c261c346a4d926e47652925462411873295883786269cba2a580010902953289", + "cnf_sha256": "826418057507d985af768d17d1029d28127d0168ca8f5fee7c18c7ea0a81f00a", + "lemmas": 1674 + } +} diff --git a/research/complex-rank8-rigidity-p109/VERIFY.json b/research/complex-rank8-rigidity-p109/VERIFY.json new file mode 100644 index 0000000000..cb49a665da --- /dev/null +++ b/research/complex-rank8-rigidity-p109/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "25 exact checks: generators; triple orbit census and inside-a-frame split; one unit per open orbit; per unit (19) the pivot's D4 structure, (I3), (I4)/gluing, Lemma 9 connectivity and algebra, assembly, CNF consistency, DRUP zero-exclusion replay with the package's own RUP checker and the needs-zero-clause control; one bogus-proof control." + } + ] +} diff --git a/research/complex-rank8-rigidity-p109/make_proof.py b/research/complex-rank8-rigidity-p109/make_proof.py new file mode 100644 index 0000000000..8391e0faf0 --- /dev/null +++ b/research/complex-rank8-rigidity-p109/make_proof.py @@ -0,0 +1,78 @@ +#!/usr/bin/env python3 +"""Choose the 19 orbit representatives and pivots, and regenerate UNITS.json and PROOFS.json.gz, which +verify.py replays (needs python-sat; verify.py itself does not). + + python3 -I -B research/complex-rank8-rigidity-p109/make_proof.py --out-dir /new/dir + +Representative: the first triple of each open orbit in verify.py's order. Pivot: the first frame inside the +live set, in line order, that passes (I3), (I4), gluing and Lemma 9 connectivity. Deletion lines are dropped +from the solver's DRUP output (verify.py's checker ignores them anyway). Any DRUP-producing solver may be +substituted; verify.py checks the proof, not the solver. +""" +import argparse +import gzip +import hashlib +import itertools +import json +import sys +from multiprocessing import Pool +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import verify as V # noqa: E402 + +SOLVER = 'g4' + + +def unit(X): + from pysat.solvers import Solver + live = [i for i in V.P112 if i not in X] + F = next(F for F in V.frames_inside(live) if V.passes(V.inputs(live, F))) + cnf, zvars = V.build_cnf(live, F) + with Solver(name=SOLVER, bootstrap_with=cnf.clauses + [zvars], with_proof=True) as s: + if s.solve(): + raise SystemExit(f'{X}: UNEXPECTED satisfiable') + proof = [ln for ln in s.get_proof() if not ln.startswith('d')] + text = '\n'.join(proof) + '\n' + return F, text, V.cnf_digest(cnf.clauses + [zvars]) + + +def main(): + global SOLVER + ap = argparse.ArgumentParser() + ap.add_argument('--out-dir', required=True) + ap.add_argument('--solver', default='g4') + ap.add_argument('--jobs', type=int, default=8) + args = ap.parse_args() + SOLVER = args.solver + out = Path(args.out_dir) + for f in ('UNITS.json', 'PROOFS.json.gz'): + if (out / f).exists(): + print(f'refusing to overwrite {out / f}') + return 2 + frames = V.frames_inside(V.P112) + inframe = {X for F in frames for X in itertools.combinations(F, 3)} + open_ = [o for o in V.triple_orbits(V.stabiliser(V.FRAME0)[::V.GEN_STEP]) if o[0] not in inframe] + reps = [o[0] for o in open_] + with Pool(args.jobs, initializer=_init, initargs=(SOLVER,)) as pool: + res = pool.map(unit, reps) + units, proofs = {}, {} + for n, (X, o, (F, text, cdig)) in enumerate(zip(reps, open_, res), 1): + name = f'u{n:02d}' + units[name] = {'orbit_size': len(o), 'triple': [V.LINES[i] for i in X], 'pivot': [V.LINES[i] for i in F], + 'proof_sha256': hashlib.sha256(text.encode()).hexdigest(), 'cnf_sha256': cdig, + 'lemmas': text.count('\n')} + proofs[name] = text + print(f"{name}: orbit {len(o)}, odd pairs {V.odd_pairs(X)}, {text.count(chr(10))} lemmas") + (out / 'UNITS.json').write_text(json.dumps(units, indent=1) + '\n') + (out / 'PROOFS.json.gz').write_bytes(gzip.compress(json.dumps(proofs, sort_keys=True).encode(), mtime=0)) + return 0 + + +def _init(solver): + global SOLVER + SOLVER = solver + + +if __name__ == '__main__': + sys.exit(main()) diff --git a/research/complex-rank8-rigidity-p109/verify.py b/research/complex-rank8-rigidity-p109/verify.py new file mode 100644 index 0000000000..277b9aa07f --- /dev/null +++ b/research/complex-rank8-rigidity-p109/verify.py @@ -0,0 +1,558 @@ +#!/usr/bin/env python3 +"""Rank-8 rigidity of the E-graph system on every P109 unit (P112 minus three lines) outside PR1419's reach. + +Standard library only, exact arithmetic. Independent of PR1212's code: own E8 model, stabiliser orbits on +triples, classes, witnesses, gluing, Lemma 9 propagation, zero-pattern CNF and RUP checker. The 19 DRUP +refutations in PROOFS.json.gz were produced by make_proof.py (python-sat); this file replays them. Run from the +repository root: + + python3 -I -B research/complex-rank8-rigidity-p109/verify.py +""" + +import gzip +import hashlib +import itertools +import json +import sys +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +RESULTS = [] + + +def check(tag, cond, info=''): + RESULTS.append(tag) + print(f"{'PASS' if cond else 'FAIL'} {tag}" + (f': {info}' if info else '')) + if not cond: + print(f'FAIL_COMPLEX_RANK8_RIGIDITY_P109: {tag}') + sys.exit(1) + + +# ---------------------------------------------------------------- E8 model (doubled coordinates, norm 8) + +def lines_e8(): + out = set() + for i, j in itertools.combinations(range(8), 2): + for sj in (2, -2): + v = [0] * 8 + v[i], v[j] = 2, sj + out.add(tuple(v)) + for s in itertools.product((1, -1), repeat=7): + v = (1,) + s + if v.count(-1) % 2 == 0: + out.add(v) + return sorted(out) + + +LINES = lines_e8() +NL = len(LINES) +IDX = {v: n for n, v in enumerate(LINES)} + + +def canon(v): + v = tuple(v) + first = next(a for a in v if a) + return v if first > 0 else tuple(-a for a in v) + + +def ip(x, y): + d = sum(a * b for a, b in zip(x, y)) + assert d % 4 == 0 + return d // 4 + + +G = [[ip(LINES[i], LINES[j]) for j in range(NL)] for i in range(NL)] + + +def lid(v): + return IDX[canon(v)] + + +FRAME0 = frozenset(lid(v) for v in [ + (2, 2, 0, 0, 0, 0, 0, 0), (2, -2, 0, 0, 0, 0, 0, 0), (0, 0, 2, 2, 0, 0, 0, 0), (0, 0, 2, -2, 0, 0, 0, 0), + (0, 0, 0, 0, 2, 2, 0, 0), (0, 0, 0, 0, 2, -2, 0, 0), (0, 0, 0, 0, 0, 0, 2, 2), (0, 0, 0, 0, 0, 0, 2, -2)]) +P112 = [i for i in range(NL) if i not in FRAME0] + +# UNITS.json: the 19 orbit representatives (punctured triple and pivot frame, as root vectors) with pinned SHA256 of each +# decompressed proof and of the CNF it refutes. Chosen by make_proof.py: the first triple of each orbit in +# verify.py's order, and the first frame inside the live set (in line order) that passes (I3), (I4), gluing and +# Lemma 9 connectivity. The verifier rechecks every property it relies on; the pins only detect drift. +UNITS_FILE = HERE / 'UNITS.json' +# Every 29th stabiliser generator (8 of 204). Orbits under any subgroup are sound for transport; this subset +# already gives the 24 orbits that all 204 generators give (checked by census.triples against PR1419's census). +GEN_STEP = 29 + + +def is_frame(S): + return len(S) == 8 and all(G[a][b] == 0 for a in S for b in S if a != b) + + +def reflection_perm(r): + rv = LINES[r] + return tuple(lid(tuple(a - G[i][r] * b for a, b in zip(LINES[i], rv))) for i in range(NL)) + + +def stabiliser(frame): + refl = [reflection_perm(r) for r in range(NL)] + gens = [p for p in refl if frozenset(p[i] for i in frame) == frame] + for p, q in itertools.combinations(refl, 2): + pq = tuple(p[q[i]] for i in range(NL)) + if frozenset(pq[i] for i in frame) == frame: + gens.append(pq) + return gens + + +# ---------------------------------------------------------------- structure relative to a pivot + +def relative(F, lines): + """line -> (T, eps): T the pivot lines (in pivot order) the line is odd to, eps the signs G_if.""" + out = {} + for i in lines: + if i in F: + continue + T = tuple(f for f in F if G[i][f] != 0) + out[i] = (T, tuple(G[i][f] for f in T)) + return out + + +def parity(eps): + return sum(1 for s in eps if s < 0) % 2 + + +def classes_of(rel): + cl = {} + for i, (T, eps) in rel.items(): + cl.setdefault((T, parity(eps)), []).append(i) + return cl + + +def connected(n, edges): + seen, todo = {0}, [0] + while todo: + x = todo.pop() + for p, q in edges: + for y in ((q,) if p == x else (p,) if q == x else ()): + if y not in seen: + seen.add(y) + todo.append(y) + return len(seen) == n + + +def inputs(live, F): + """PR1212's (I3), (I4) and gluing on the complete classes, and PR1399's Lemma 9 connectivity for the + remaining lines. Returns a dict of results (all booleans True means the unit passes).""" + rel = relative(F, live) + cl = classes_of(rel) + complete = {k: v for k, v in cl.items() if len(v) == 4} + known = {i for v in complete.values() for i in v} + rest = [i for i in rel if i not in known] + nwit, wit_ok = 0, True + for (T, _), rows in complete.items(): + for c, c2 in itertools.combinations(range(4), 2): + for i, i2 in itertools.combinations(rows, 2): + if rel[i][1][c] * rel[i][1][c2] != rel[i2][1][c] * rel[i2][1][c2]: + continue + nwit += 1 + wit_ok &= any(set(Tj) & set(T) == {T[c], T[c2]} and G[j][i] == 0 and G[j][i2] == 0 + for j, (Tj, _) in rel.items()) + npair, glue_ok = 0, True + for c1, c2 in itertools.permutations(complete, 2): + if c1[0] == c2[0] or len(set(c1[0]) & set(c2[0])) != 2: + continue + npair += 1 + glue_ok &= all(sum(1 for i in complete[c1] if G[i][j] == 0) == 2 for j in complete[c2]) + prop_ok, sign_ok, pairs, nw = True, True, [], 0 + for i in rest: + T, ei = rel[i] + edges = [] + for c, c2 in itertools.combinations(range(4), 2): + ws = [j for j in known if G[i][j] == 0 and set(rel[j][0]) & set(T) == {T[c], T[c2]}] + for j in ws: + Tj, ej = rel[j] + sign_ok &= ei[c] * ej[Tj.index(T[c])] == -ei[c2] * ej[Tj.index(T[c2])] + if ws: + edges.append((c, c2)) + nw += len(ws) + pairs.append(len(edges)) + prop_ok &= connected(4, edges) + profile = sorted(len(v) for v in cl.values()) + return {'rel': rel, 'complete': complete, 'known': known, 'rest': rest, 'profile': profile, + 'blocks': len({T for T, _ in complete}) == 14, 'witnesses': wit_ok, 'nwit': nwit, + 'glue': glue_ok, 'npair': npair, 'prop': prop_ok and sign_ok, 'pairs': pairs, 'nw': nw} + + +def d4_structure(F): + """PR1212 Lemma 2 facts relative to F, over all 112 non-pivot lines: each is odd to 4 pivot lines; the 14 + blocks form an S(3,4,8); the 28 classes are 4 pairwise orthogonal lines with orthogonal sign vectors; + 2 G_ij is the sum of sign products over T_i n T_j.""" + rel = relative(F, range(NL)) + blocks = sorted({T for T, _ in rel.values()}) + ok = all(len(T) == 4 and all(abs(x) == 1 for x in e) for T, e in rel.values()) + ok &= len(blocks) == 14 and all(sum(1 for B in blocks if set(t) <= set(B)) == 1 + for t in itertools.combinations(F, 3)) + cl = classes_of(rel) + ok &= len(cl) == 28 and all( + len(v) == 4 and all(G[i][j] == 0 for i in v for j in v if i != j) + and all(sum(x * y for x, y in zip(rel[i][1], rel[j][1])) == (4 if i == j else 0) for i in v for j in v) + for v in cl.values()) + for i, j in itertools.combinations(rel, 2): + (Ti, ei), (Tj, ej) = rel[i], rel[j] + ok &= 2 * G[i][j] == sum(ei[Ti.index(f)] * ej[Tj.index(f)] for f in set(Ti) & set(Tj)) + return ok + + +def passes(r): + return r['blocks'] and r['witnesses'] and r['glue'] and r['prop'] + + +# ---------------------------------------------------------------- zero-pattern CNF (Lemma 8 analogue) + +class CNF: + def __init__(self): + self.ids, self.clauses = {}, [] + + def var(self, key): + if key not in self.ids: + self.ids[key] = len(self.ids) + 1 + return self.ids[key] + + def add(self, c): + self.clauses.append(list(c)) + + +def build_cnf(live, F): + """Necessary conditions on the zero pattern of a_i = K[i,F] and b_i = K[F,i] (variable TRUE = entry zero) + for a rank-8 solution of (E), after pivot reduction K = K[:,F] K[F,:] / 4 (rank K = 8, K[F,F] = 4I): + two orthogonal i, j with T_i n T_j = {k, k'}: a_ik b_jk + a_ik' b_jk' = 0, so one product vanishes + iff the other does (both orders i.j and j.i are separate pairs); + four orthogonal i, j with T_i = T_j: sum of four products is 0, so not exactly one is nonzero; + diag a_i . b_i = 16: some product is nonzero; + trans complete class C (4 pairwise orthogonal rows): A_C B_C^T = 16 I, so A_C and B_C are nonsingular + and their zero patterns admit a transversal (some permutation avoids every zero). + Returns the CNF and the pattern variables; the refuted formula adds the clause OR(pattern variables).""" + rel = relative(F, live) + cnf = CNF() + rows = sorted(rel) + za = lambda i, f: cnf.var(('a', i, f)) + zb = lambda i, f: cnf.var(('b', i, f)) + for i in rows: + for f in rel[i][0]: + za(i, f) + for i in rows: + for f in rel[i][0]: + zb(i, f) + for i in rows: + Ti = rel[i][0] + for j in rows: + if j == i or G[i][j] != 0: + continue + ov = [f for f in Ti if f in rel[j][0]] + if len(ov) == 2: + k, kp = ov + for (p, q), (r, s) in (((za(i, k), zb(j, k)), (za(i, kp), zb(j, kp))), + ((za(i, kp), zb(j, kp)), (za(i, k), zb(j, k)))): + cnf.add([-p, r, s]) + cnf.add([-q, r, s]) + elif len(ov) == 4: + prods = [] + for k in ov: + pk = cnf.var(('p', i, j, k)) # pk <-> a_ik != 0 and b_jk != 0 + cnf.add([-pk, -za(i, k)]) + cnf.add([-pk, -zb(j, k)]) + cnf.add([pk, za(i, k), zb(j, k)]) + prods.append(pk) + for pk in prods: + cnf.add([-pk] + [q for q in prods if q != pk]) + ds = [] + for k in Ti: + dk = cnf.var(('d', i, k)) + cnf.add([-dk, -za(i, k)]) + cnf.add([-dk, -zb(i, k)]) + cnf.add([dk, za(i, k), zb(i, k)]) + ds.append(dk) + cnf.add(ds) + for (T, par), lines in sorted(classes_of(rel).items()): + if len(lines) != 4: + continue + for which, zf in (('A', za), ('B', zb)): + perms = [] + for perm in itertools.permutations(range(4)): + v = cnf.var(('perm', which, T, par, perm)) + for p, i in enumerate(lines): + cnf.add([-v, -zf(i, T[perm[p]])]) + perms.append(v) + cnf.add(perms) + zvars = [cnf.ids[('a', i, f)] for i in rows for f in rel[i][0]] + \ + [cnf.ids[('b', i, f)] for i in rows for f in rel[i][0]] + return cnf, zvars + + +def cnf_digest(clauses): + return hashlib.sha256('\n'.join(' '.join(map(str, c)) for c in clauses).encode()).hexdigest() + + +def rup_check(clauses, nvars, proof_text): + """Replay a DRUP refutation with two-watched-literal unit propagation. Every lemma must be RUP with + respect to the original clauses and earlier lemmas; deletions are ignored (sound: the database only + grows); the empty clause must be derived. Returns (ok, lemmas, reason).""" + db, watches, units = [], {}, [] + empty = [False] + + def add(c): + c = list(dict.fromkeys(c)) + if not c: + empty[0] = True + return + if len(c) == 1: + units.append(c[0]) + return + idx = len(db) + db.append(c) + watches.setdefault(c[0], []).append(idx) + watches.setdefault(c[1], []).append(idx) + + def conflict(assume): + val = {} + trail = [] + + def setlit(lit): + v, s = abs(lit), (1 if lit > 0 else -1) + if v in val: + return val[v] == s + val[v] = s + trail.append(lit) + return True + + def value(lit): + s = val.get(abs(lit)) + return None if s is None else (s == 1) == (lit > 0) + + if empty[0]: + return True + for lit in units + assume: + if not setlit(lit): + return True + q = 0 + while q < len(trail): + fl = -trail[q] + q += 1 + wl = watches.get(fl, []) + k = 0 + while k < len(wl): + c = db[wl[k]] + if c[0] == fl: + c[0], c[1] = c[1], c[0] + if value(c[0]) is True: + k += 1 + continue + moved = False + for m in range(2, len(c)): + if value(c[m]) is not False: + c[1], c[m] = c[m], c[1] + watches.setdefault(c[1], []).append(wl[k]) + wl[k] = wl[-1] + wl.pop() + moved = True + break + if moved: + continue + if value(c[0]) is False: + return True + setlit(c[0]) + k += 1 + return False + + for c in clauses: + add(c) + n = 0 + for line in proof_text.splitlines(): + line = line.strip() + if not line or line.startswith('c') or line.startswith('d'): + continue + lits = [int(t) for t in line.split()] + if not lits or lits[-1] != 0 or 0 in lits[:-1] or any(abs(x) > nvars for x in lits): + return False, n, f'malformed lemma {line[:40]}' + lem = lits[:-1] + if not conflict([-x for x in lem]): + return False, n, f'lemma {n} not RUP' + n += 1 + add(lem) + if not lem: + return True, n, 'empty clause derived' + return False, n, 'no empty clause' + + +# ---------------------------------------------------------------- exact algebra for Lemma 9 and assembly + +def rank_q(rows): + M = [[Fraction(x) for x in r] for r in rows] + rk = 0 + for c in range(len(M[0]) if M else 0): + p = next((r for r in range(rk, len(M)) if M[r][c] != 0), None) + if p is None: + continue + M[rk], M[p] = M[p], M[rk] + for r in range(len(M)): + if r != rk and M[r][c] != 0: + f = M[r][c] / M[rk][c] + M[r] = [a - f * b for a, b in zip(M[r], M[rk])] + rk += 1 + return rk + + +def lcg(seed): + x = seed + while True: + x = (6364136223846793005 * x + 1442695040888963407) % (1 << 64) + yield x >> 33 + + +def rand_nonzero(rng): + while True: + n, d = next(rng) % 17 - 8, next(rng) % 7 + 1 + if n: + return Fraction(n, d) + + +def algebra(live, F, r, seed): + """Lemma 9 rank-3 cross-check and the PR1212 section 7 assembly on this unit, for random rational g, d'.""" + rel, known, rest = r['rel'], r['known'], r['rest'] + rng = lcg(seed) + g = {f: rand_nonzero(rng) for f in F} + dd = {i: rand_nonzero(rng) for i in rel} + ok = True + for i in rest: + T, ei = rel[i] + wit = [j for j in known if G[i][j] == 0 and len(set(rel[j][0]) & set(T)) == 2] + rows_a = [[4 / (dd[j] * g[f]) * G[j][f] for f in T] for j in wit] + rows_b = [[dd[j] * G[j][f] * g[f] for f in T] for j in wit] + va = [ei[n] * g[f] for n, f in enumerate(T)] + vb = [ei[n] / g[f] for n, f in enumerate(T)] + ok &= rank_q(rows_a) == 3 and all(sum(x * y for x, y in zip(row, va)) == 0 for row in rows_a) + ok &= rank_q(rows_b) == 3 and all(sum(x * y for x, y in zip(row, vb)) == 0 for row in rows_b) + a = {i: {f: (dd[i] * G[i][f] * g[f] if f in rel[i][0] else Fraction(0)) for f in F} for i in rel} + b = {i: {f: (4 / (dd[i] * g[f]) * G[i][f] if f in rel[i][0] else Fraction(0)) for f in F} for i in rel} + for f in F: + a[f] = {h: Fraction(4 if h == f else 0) for h in F} + b[f] = {h: Fraction(4 if h == f else 0) for h in F} + D = {i: dd[i] / 2 for i in rel} + D.update({f: 1 / g[f] for f in F}) + asm = all(sum(a[i][f] * b[j][f] for f in F) / 4 == 2 * G[i][j] * D[i] / D[j] for i in live for j in live) + eqs = all(sum(a[i][f] * b[j][f] for f in F) == (16 if i == j else 0) + for i in live for j in live if i == j or G[i][j] == 0) + return ok, asm and eqs + + +def gauge_pattern_satisfies(cnf): + """Control: the all-nonzero pattern of a gauge solution (every pattern variable FALSE, every product, + diagonal and permutation variable TRUE) satisfies the CNF without the final 'some zero' clause.""" + truth = {} + for key, v in cnf.ids.items(): + truth[v] = key[0] in ('p', 'd', 'perm') + return all(any((truth[abs(x)] if x > 0 else not truth[abs(x)]) for x in c) for c in cnf.clauses) + + +# ---------------------------------------------------------------- main + +def frames_inside(live): + live = sorted(live) + out = [] + + def grow(cur, cand): + if len(cur) == 8: + out.append(cur) + return + for n, j in enumerate(cand): + grow(cur + [j], [k for k in cand[n + 1:] if G[j][k] == 0]) + + grow([], live) + return out + + +def triple_orbits(gens): + """Union-find orbits of the gens on 3-subsets of P112 (as sorted line-id triples).""" + subs = list(itertools.combinations(P112, 3)) + idx = {s: n for n, s in enumerate(subs)} + par = list(range(len(subs))) + + def find(a): + while par[a] != a: + par[a] = par[par[a]] + a = par[a] + return a + + for g in gens: + for n, s in enumerate(subs): + a, b = find(n), find(idx[tuple(sorted(g[x] for x in s))]) + if a != b: + par[a] = b + orbs = {} + for n, s in enumerate(subs): + orbs.setdefault(find(n), []).append(s) + return sorted(orbs.values(), key=lambda o: (len(o), o[0])) + + +def odd_pairs(X): + return sum(1 for a, b in itertools.combinations(X, 2) if G[a][b] != 0) + + +def main(): + check('model.lines', NL == 120 and len(FRAME0) == 8 and is_frame(sorted(FRAME0)), '120 lines; FRAME0 is a frame') + allgens = stabiliser(FRAME0) + gens = allgens[::GEN_STEP] + check('model.generators', len(allgens) == 204 and all(frozenset(g[i] for i in FRAME0) == FRAME0 for g in gens), + f'{len(gens)} of the {len(allgens)} reflection / reflection-pair generators fixing FRAME0') + frames = frames_inside(P112) + inframe = {X for F in frames for X in itertools.combinations(F, 3)} + orbs = triple_orbits(gens) + split = [all((X in inframe) == (o[0] in inframe) for X in o) for o in orbs] + covered = [o for o in orbs if o[0] in inframe] + open_ = [o for o in orbs if o[0] not in inframe] + check('census.triples', len(frames) == 1260 and sum(map(len, orbs)) == 227920 and len(orbs) == 24 and all(split) + and sum(map(len, covered)) == 29232 and len(open_) == 19 and sum(map(len, open_)) == 198688, + f'227920 triples of P112 in {len(orbs)} orbits; inside-a-frame is constant on orbits; ' + f'{len(covered)} orbits (29232 triples) inside a P112 frame (PR1419), {len(open_)} orbits (198688) not') + nodd = sorted(odd_pairs(o[0]) for o in open_) + check('census.open-orbits', [len(o) for o in open_ if odd_pairs(o[0]) == 0] == [1792], + f'open orbit sizes {[len(o) for o in open_]}; odd pairs per triple {dict((k, nodd.count(k)) for k in sorted(set(nodd)))}; ' + 'the only pairwise-orthogonal open orbit has 1792 triples') + UNITS = json.loads(UNITS_FILE.read_text()) + blob = json.loads(gzip.decompress((HERE / 'PROOFS.json.gz').read_bytes())) + check('units.cover', sorted(UNITS) == sorted(blob) and len(UNITS) == 19 and + sorted(next(n for n, o in enumerate(open_) if tuple(sorted(lid(v) for v in u['triple'])) in o) + for u in UNITS.values()) == list(range(19)), + '19 units, one representative in each open orbit; one proof per unit') + bogus_done = False + for name, u in sorted(UNITS.items()): + X = sorted(lid(v) for v in u['triple']) + F = [lid(v) for v in u['pivot']] + live = [i for i in P112 if i not in X] + orb = next(o for o in open_ if tuple(X) in o) + ok = is_frame(F) and set(F) <= set(live) and len(live) == 109 and d4_structure(F) + r = inputs(live, F) + nc = sum(1 for n in r['profile'] if n == 4) + ok &= r['witnesses'] and r['nwit'] == 12 * nc and r['blocks'] and r['glue'] and r['prop'] + ok9, asm = algebra(live, F, r, 1090 + int(name[1:])) + cnf, zvars = build_cnf(live, F) + clauses = cnf.clauses + [zvars] + text = blob[name] + digest = hashlib.sha256(text.encode()).hexdigest() + good, n, why = rup_check(clauses, len(cnf.ids), text) + nozero, _, _ = rup_check(cnf.clauses, len(cnf.ids), text) + check(f'{name}.rigid', ok and ok9 and asm and gauge_pattern_satisfies(cnf) and good and not nozero + and digest == u['proof_sha256'] and cnf_digest(clauses) == u['cnf_sha256'], + f'orbit {len(orb)}, {odd_pairs(X)} odd pairs; pivot passes D4/(I3)/(I4)/gluing with {nc} complete classes ' + f'and Lemma 9 on {len(r["rest"])} lines; assembly on 109 lines; zero exclusion {n} lemmas ({why}); ' + f'proof fails without the zero clause') + if not bogus_done: + bogus, _, why2 = rup_check(clauses, len(cnf.ids), '0\n') + check('control.bogus-proof', not bogus and 'not RUP' in why2, + 'an empty-clause-only proof is rejected: unit propagation alone does not refute the CNF') + bogus_done = True + print(f'PASS_COMPLEX_RANK8_RIGIDITY_P109: checks {len(RESULTS)}; all 19 open P109 orbits (198688 triples) rigid; ' + f'with PR1419 every P109 unit is rigid; floor 61') + + +if __name__ == '__main__': + main()