diff --git a/research/e8-rank9-realisations/LICENSE b/research/e8-rank9-realisations/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/e8-rank9-realisations/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/e8-rank9-realisations/MANIFEST.sha256 b/research/e8-rank9-realisations/MANIFEST.sha256 new file mode 100644 index 0000000000..72c8453025 --- /dev/null +++ b/research/e8-rank9-realisations/MANIFEST.sha256 @@ -0,0 +1,27 @@ +c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4 LICENSE +1ea58e398f40239c0945d495a807b33bcadeb6d5dcd147a12bf71ff06a9ed7ec NOTICE.md +dd4d1f54ec6e0f41da85c5862304d8bcb8b252f50425f13467f230b69098568a README.md +fe252c53a8dee2cbb39a2d99696a113783ed4556560351ea446aea6b91787c6e SOURCES.json +bc9771ff9898a44b5caa86ee64c490e2b1b7a06822253bebdaca4a828ff032a1 checks/a2e8.py +b1a0339383cc4ae6957caec6a9feffb9fb344679cceeff8eca49996ff21bcf4d checks/e8lib.py +012739ff3dc3421c187ca089b361c0b1d49f808908a5a7efdb0603c20f08ca71 checks/manifest_check.py +c77e3615c6c200c2b0a86e51e6350627a994811b86edb24ca3ef68a559e2a910 checks/modrank.py +d3dbc52a02a3756dca524559324cdc93eaae6f8832d79351f550dca1a20ad535 checks/pframes.py +0f83cfab95ca00a299e01bd7c1ce0d438a0bb95c11cb069ad7480cf361916fa4 checks/pin.py +877ad69dcf484a130bf33416f237d5ac536acfb600e7ea3248dca0c4853a133f checks/rup.py +a612d0c0012888552385cf7b9f28e54588ae7ea44a695100be35dd96488ba953 checks/rupc.c +df457fafeeaa4fcfea4c382725bee1bd58a410dbddf20e729f8689591432de03 checks/s56.py +55010f515a2e37f82a079d4c600c8e6ec4c21e90d11737356f87cb9ca0f6cbd1 checks/soundtest.py +780d373d518e6c1830594d550f408cc7eac9da32a1527504efb6c32afd9e5e0a checks/spans.py +8d5b0c0270c916e9ce5136a2d95f06c4eff4769008534b8d2d83c402694e1d2d checks/spans3.py +6288647aaf299ce13049e66e6d28893373972b6ba7fc1983bbd17d145df9fc04 evidence/BSTAR_THEORY_snapshot.md +97704de7113528a6bfc0cc4614b7fc767dd2414585b23206ff24b9c4bfa6b4a8 evidence/CONJB_THEORY_snapshot.md +2d7526c754b0d826dde33d1393d88b83a7ff3ed7fda167f93b3078e44e863b29 evidence/KSTAR_THEORY_snapshot.md +a3f2c17c3cd98d79f375aed53faccd0282515be7beb9bfb0a779175981b2ebc8 evidence/logs/audit_dratrim_pin3.log.txt +336fd849ad1a66a42228580c054a9474a13127b8c69f74616e7abe1709f4dfbf evidence/logs/dratrim_shipped_pin3.log.txt +a846e55d23a6b8ae867305242ac6fffa69d1cf109a4b7e3e7e29aab4241ebccc evidence/logs/kstar_cert2_E8_pin3_rupc.log.txt +8bfaabe8da458030f80678bcf6a96e5f6eb3a9a92390a0ea852cd45ada132ad1 evidence/logs/kstar_s56_E8_f1_0-15.log.txt +fbfca0129ff45b7bd2ef07ef75f1f1246da39138ef8df1f3eeec9c724c898d73 evidence/pins.tsv +9c8a7a6bc24615a7024567feb300c27a1e16542eb1437a0014152c1f8ca93de8 evidence/proofs/pin3.drat.xz +d6f3dc65ab36e5121fefe6716cdbf86bd47668ed76f569576f241f7646b73dfe requirements.txt +d1cb9409cd09cec1b0efa2ef2d32a4bb3bf0b9c4f56433ac8e9dfe961459fbd8 verify.sh diff --git a/research/e8-rank9-realisations/NOTICE.md b/research/e8-rank9-realisations/NOTICE.md new file mode 100644 index 0000000000..c6f3494c2c --- /dev/null +++ b/research/e8-rank9-realisations/NOTICE.md @@ -0,0 +1,3 @@ +# Notice + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0 (`LICENSE`, copied from the repository root). diff --git a/research/e8-rank9-realisations/README.md b/research/e8-rank9-realisations/README.md new file mode 100644 index 0000000000..62c6efd17a --- /dev/null +++ b/research/e8-rank9-realisations/README.md @@ -0,0 +1,81 @@ +# Rank-9 realisations of the E8 orthogonality pattern are B-form or the A2 family (classification; no κ claim) + +> **Scope, stated first.** Pure matrix classification on the **E8 unit** (120 lines). **No κ claim**, no window, no supplier, no cost of any decoder. It completes the *existence step* that #2784 (*Decoder floors, case (c): the A2 family of non-B-form rank-9 realisations*, open) left open as "Conjecture B\*": #2784 proves floors for the A2 family and says explicitly that it does not prove that every rank-9 pattern realisation is B-form or A2. **P112 / P104 are not claimed here** (see "Not claimed"). +> Labels: **PROVEN** (argument in this README or the shipped card text), **CHECKED** (recomputed by `verify.sh`; SAT steps with a DRAT proof checked by the standard `drat-trim`), **RECORDED** (a run whose log is shipped and whose headline line `verify.sh` asserts, but which the default `verify.sh` does not repeat), **CONDITIONAL [verify]** (an external fact not checkable here). kissat 4.0.4 only, never CaDiCaL. +> **Overlap.** A search of PR bodies for rank-9 / rank-nine realisation classifications found none besides #2784 (this author's, the A2 family) and #1212 (burntout76, merged: rank-8 rigidity; rank 9 stated open). #2338 / #2724 / #2639 are decoder floors, not classifications. + +## 1. Result + +Setting (that of #2338 / #2784): a field `K` of **characteristic 0**; `M` a `120 × 120` matrix over `K` indexed by the E8 root lines, with `M_tt ≠ 0` and, for `t ≠ s`, `M_ts = 0 ⇔ r_t ⊥ r_s` ("iff pattern"); `G` the Gram matrix of chosen roots. +**B-form:** `M = D₁ G D₂ + c βᵀ` with `D₁, D₂` diagonal and `c_u β_s = 0` whenever `u ⊥ s`. **A2 family:** `M` is Gram (up to diagonal scalings) off the three rows of one A2 triangle, and row `u_i` is the Gram row rescaled by one factor on `Nbar(u_i) ∩ O_{u_j}` and another on `Nbar(u_i) ∩ O_{u_k}` (#2784 §2.2; construction `checks/a2e8.py`). + +| # | statement | status | +|---|---|---| +| **C** | **If `rank M = 9`, then `M` is B-form or in the A2 family** (and conversely both occur: exact rank-9 members of both families with the iff pattern exist, `a2e8.py`; A2 members that are not of B-form: #2784's `a2cert.py`, not re-run) | **PROVEN** from the rows below | +| G | Theorem G (CONJB; #2784 §3): rows off a set `X` Gram ⇒ B-form with `supp c ⊆ X`, or A2 | **PROVEN** from CHECKED span facts S1, S2 (`spans.py`) | +| P, A | Theorem P (pinning) and Theorem A (an orthogonal pair in `Σ_a` or `Σ_b`) | **PROVEN** from CHECKED: all 2025 E8 frames are P-compatible and all 3780 orthogonal pairs lie in a frame (`pframes.py`) | +| S | Theorem S: `Σ_a ∩ Σ_b ≠ ∅` ⇒ B-form or A2 | reduction **PROVEN**; finite step (56-line point/line incidence problem) **CHECKED**: kissat UNSAT, standard drat-trim VERIFIED, for `f₁ = 0..15` (all 120 with `FULL=1`); one `f₁` suffices because W(E8) is transitive on lines, the others are redundant checks | +| Σ | Theorem Σ: `Σ_a ≠ ∅` or `Σ_b ≠ ∅` ⇒ B-form or A2 | **PROVEN** from S, A, G and CHECKED (S3′), (W2) (`spans3.py`) | +| R | Theorem R: the residue `Σ_a = Σ_b = ∅` is empty | reduction **PROVEN**; finite step **CHECKED** (proof check under `FULL=1`; default run: CNF regeneration + shipped-proof hash, RECORDED drat-trim log): the CNF `pin3.cnf` (56 784 variables, 3 513 012 clauses) is regenerated byte-identically; kissat UNSAT; standard drat-trim VERIFIED on the shipped proof and on a fresh one (`FULL=1`) | +| rules | the Boolean rules of the pinning model are sound | each rule has a one-line proof (§4); **CHECKED** on true data: 0 violations over A2 members (5 parameter draws on 5 triangles) and B-form members, and a mutation control: one flipped sign is caught (`soundtest.py`). The test is evidence for the rules, not part of the proof | +| audit | independent read-only audit (Opus): re-verified `pin3` and `s56` with the standard drat-trim (VERIFIED), regenerated the CNFs byte-identically, showed the soundness test catches a flipped rule; two fixes applied (this README states characteristic 0, the test now varies the A2 parameter) | **RECORDED** (log shipped; the audit report itself is not) | +| field | all span facts are rank statements about integer matrices, computed mod `2⁶¹ − 1` (a lower bound for the rank over `Q`; the upper bounds are trivial), hence true over every field of characteristic 0. The SAT steps use only the sign/equality logic of §4 (characteristic ≠ 2) | **CHECKED** | + +## 2. The proof chain (E8; pivot coordinates) + +Full text: `evidence/BSTAR_THEORY_snapshot.md` (§2 frame calculus, Theorems P, A), `evidence/CONJB_THEORY_snapshot.md` (Theorem G, A2 family), `evidence/KSTAR_THEORY_snapshot.md` (§1 S, §2 Σ, §7 R). Working-card texts, copies; their status lines are working-time statements. + +* **Pivot coordinates.** For a frame `F` (8 pairwise orthogonal lines), `M = M[:,F] M[F,F]⁻¹ M[F,:] + x yᵀ` with `x_F = y_F = 0`; row `u` is `a_u = (α_u, x_u)` with `supp α_u` the `F`-tetrad of `u`. `D_F = supp x`, `D′_F = supp y`. Schur rule: `x|_T ≠ 0 ⇒ y|_{T^c} = 0`. `Σ_a = {u : dim span a(O_u) = 7}`, `Σ_b` likewise; `f ∈ Σ_a ⇔ D_F ⊆ Nbar(f)` for `f ∈ F`. +* **Theorem P.** If the "unpinned" pairs of a P-compatible frame form a matching, the rows off `D_F` are Gram rows (pair pinning `φ(u) = ψ(s)^⊥`, triangles force `B′ = −B` since char ≠ 2, gauge `μ`, then S1); Theorem G finishes. +* **Theorem A.** `f₁ ⊥ f₂` both in `Σ_a` in a frame ⇒ `D_F` lies in the three tetrads through `{1,2}` ⇒ only `{1,2}` is unpinned ⇒ Theorem P. +* **Theorem S** (`Σ_a ∩ Σ_b ∋ f₁`). Off index 1 everything is Gram-shaped; the only remaining constraint is `P_u · Q_s = 1` for `u ⊥ s` in the 56 lines `Nbar(f₁)`, i.e. points `P̂_u` and lines `Q̂_s` of `P²(K)` incident whenever `u ⊥ s`. The Boolean abstraction keeps only necessary conditions (equalities of points/lines with transitivity; two distinct points share at most one line, and dually) and negates the conclusion; it is UNSAT, so some point class meets `Γ(s)` for every column (or the dual), which makes its rows Gram rows and Theorem G applies. +* **Theorem Σ** (`f₁ ∈ Σ_a`). Columns are Gram-shaped off index 1; for `u ∈ D` the relation `y_s = g_u · r_s` on `E6_u`; the cocycle lemma of Theorem G (using (S2), (S3′), (W2): the 56 vectors `w_u` give 28 directions, no three in a plane) glues the `g_u` to one `g`; then either `f₁ ∈ Σ_b` (Theorem S) or some `s ∈ O_{f₁}` is in `Σ_a` orthogonal to `f₁` (Theorem A). The transposed case is symmetric. +* **Theorem R** (`Σ_a = Σ_b = ∅`). Both sides non-Gram-shaped (else Theorem G and B-form / A2 both have `Σ ≠ ∅`), so `D, D′` meet every `O_s`. The pinning model with ratio equalities (§4) plus these hypotheses is UNSAT on `frames()[0]` (`W(E8)` is transitive on frames). +* **Conclusion.** `Σ_a ∪ Σ_b ≠ ∅` ⇒ Σ ⇒ B-form or A2; `Σ_a = Σ_b = ∅` is impossible by R. Lemma E (CONJB) is not used. + +## 3. What the finite steps are, and what `verify.sh` does + +`bash verify.sh [/fresh/outdir]` (needs `numpy`, `sympy`, kissat 4.0.4, drat-trim, `cc`, `xz`; one heavy process at a time, `nice 10`; missing tools give SKIP lines and exit 1, never PASS): + +0. `MANIFEST.sha256`. +1. Exact finite facts: both families exist (`a2e8.py`); S1, S2 (`spans.py`); S3′ on 1512 pairs and W2 (`spans3.py`); `pframes.py` (2025/2025 frames P-compatible, 3780/3780 orthogonal pairs covered). +2. **Theorem S step, in full by default.** `s56.py` regenerates the 56-problem CNF (sha256 pinned for `f₁ = 0`), kissat `--factor=false --preprocessfactor=false` gives UNSAT in under a second, and the fresh DRAT proof is checked by the standard **drat-trim** and by the auxiliary `rupc` (a C forward RUP checker that honours deletions and rejects RAT; `rup.py` is an older Python variant, shipped, not used by `verify.sh`). `f₁ = 0..15`; `FULL=1`: all 120 lines. +3. **Theorem R step.** `pin.py` regenerates `pin3.cnf`; its sha256 equals the pinned one (byte-identical to the working card's file). The shipped proof `evidence/proofs/pin3.drat.xz` (11.7 MB; 162 608 912 bytes decompressed) is checked against its pinned sha256. **`FULL=1`**: drat-trim on the shipped proof (about 2 to 3 minutes), then a fresh kissat solve (limit 1200 s; about 10 minutes originally) and drat-trim on the fresh proof. Flags as for the shipped proof: without `--factor=false --preprocessfactor=false` kissat adds extension variables, which the auxiliary `rupc` rejects. +4. `soundtest.py` (rules on true data) and the mutation control. +5. Recorded logs (asserted, not re-run): the audit's drat-trim on `pin3` (`s VERIFIED`, 3 513 012 clauses, 125 s) and our own drat-trim run on the decompressed shipped proof (`evidence/logs/dratrim_shipped_pin3.log.txt`, `s VERIFIED`, 137 s), the working card's `rupc` run (`VERIFIED` after 2 382 724 lemmas, 890 s), `s56` for `f₁ = 0..15`. + +The CNF generators are the certificate's trust anchor: the proof is a refutation of *that* formula; the soundness of the formula (§4) is a separate, human-checkable obligation, which is what the soundness test and the audit probe. + +## 4. The pinning model (Theorem R): what each rule asserts + +Variables: `x[u]`, `y[s]` (nonzero status of `x_u`, `y_s`), equalities of the pair ratios `ρ_p(u) = α_u(b)/α_u(a)` (rows) and `τ_p(s) = −β_s(a)/β_s(b)` (columns) over each frame pair `p = {a,b}`, equalities of `rat_i(u) = x_u/α_u(i)`, all transitive. Since `α_u|_p · β_s|_p = α_u(a) β_s(b) (ρ_p(u) − τ_p(s))`: ORTH / NON (orthogonal: `x_u y_s = 0 ⇒ ρ = τ`, `x_u y_s ≠ 0 ⇒ ρ ≠ τ`; non-orthogonal same sign: `x_u y_s = 0 ⇒ ρ ≠ τ`), TRI (triangle products, char ≠ 2), K³ and ZZ (the local lemma: two rows of one ε-class with independent `(φ, x)` force one common direction for the opposite-sign columns), D1, TW, RATIO and the common-partner rule, Schur, rank 9, the residue clauses, and "rows (columns) not Gram-shaped". Each has a one-line proof in `evidence/KSTAR_THEORY_snapshot.md` §7; sanity there: SAT with the residue dropped, SAT with "not Gram-shaped" dropped. **Note** NON uses that non-orthogonal entries are nonzero (the iff pattern). + +## 5. Downstream remark: what this does and does not close (case (c) on E8) + +With #2784 (A2-family decoder floors, E8 ≥ 72) this reduces case (c) (rank-9 square decoders) on E8 to decoders on **B-form** realisations. Exactly what is known about B-form (working cards MASK-RANK9 / MASK9, not shipped here; stated, not claimed): + +* **Proven in the working cards:** a term with `p ∝ c` and `q ∝ β` (Case C) costs ≥ 64; Case A with `|supp c| = 1` (`c = e_t`, the #2321 / #2385 `K_λ` family, and its transpose) costs ≥ 64, modulo a CHECKED single-line puncture census; the generic 8-clique type (random integer `c, β`) is **CHECKED** ≥ 65 for the sampled values. +* **Open there:** B-form with every `x_j, y_j ≠ 0` (Case B) for `|supp c| ≥ 2`; non-generic `c, β` (special values add deficient classes); singular `D`; and `m ≥ 10` on the B-locus (#2784 does not claim it either). + +So **a decoder floor of 72 for all rank-9 square decoders of all rank-9 realisations on E8 is not proven**: A2 family: #2784; B-form: only the cases listed above. Nothing about `m ≥ 10`, `h ≥ 10`, or rank-8 `N` with nine terms (#2724) changes. + +## 6. Relation to philippeVV's open item (R1), Discussion #1587 follow-up 8 + +Their follow-up 8 (artifact `decoder-law/lift-family-2` @ 93766d7d, with expSM / expSG behind it) lists as open (R1): "classification: every rank-9 completion is a lift" (their κ-family normal form; quoted verbatim from the follow-up), and proves credit ≤ 9 (cost ≥ 72) for every lift on a support with independent roots, plus non-concurrent A2 triples. **Credit:** the lift normal form, the credit/cost machinery, and the 28-completion census with tangent dimensions are theirs; nothing here uses them. The exact relation: + +* **Different hypothesis (so R1 does not follow as stated).** Their model (`decoder-law/README.md`, §0): `N = Σ v_k w_kᵀ` over `Q`, `N_aa = 1`, `N_ab = 0` for `a ⊥ b`, and **free when `ip = ±1`**. So a "completion" may have zeros on non-orthogonal pairs. Our theorem assumes the full iff pattern (`M_ts ≠ 0` for non-orthogonal `t ≠ s`). Hence it classifies the completions whose non-orthogonal entries are all nonzero, and says nothing about the rest. Their field is `Q`; ours is characteristic 0, which includes it. +* **"Lift" versus B-form ∪ A2 (unverified identification).** Their lifts are defined relative to a rank-8 completion on `T = V∖S` (their R2, rank-8 rigidity on `T`, which they assume), with `S` independent roots and κ-factors `(A, B)`; their non-concurrent A2 triples correspond plausibly to our A2 family, and `|S| = 1` / clique supports to B-form with small supports. We have **not** compared the normal forms, so we do not claim that every B-form realisation (arbitrary `supp c`, `supp β` with the orthogonality condition) or every A2 member is a κ-lift in their sense; their open (R3) is "lifts on dependent non-clique S"; we do not identify which B-form realisations, if any, it concerns. +* **Therefore:** our result gives R1 *for the iff-pattern subclass, provided B-form ∪ A2 ⊆ lifts*. Two steps remain for R1 itself: (i) show every B-form and A2 realisation fits their κ-family normal form (their R3 for dependent supports); (ii) remove the iff assumption. For (ii) the proof would have to be redone with "maybe zero" non-orthogonal entries: Theorem G survives (it uses non-orthogonality only through `d₁ ≠ 0`, `D₂` invertible, `M_uu ≠ 0`), but Theorem P (supports of `α_u`, `β_s` exact so `φ, ψ ∈ P¹∖{0,∞}`), the NON rule and the S-step reduction use nonzero entries, so the two SAT models would need to be rebuilt and re-certified. Not attempted. + +## 7. Not claimed + +* **P112 and P104.** The working card has Theorem S (112/112 UNSAT with RUP-VERIFIED) and the span facts for P112, and Theorem R on the first P112 frame is UNSAT by plain kissat; the certification of Theorem R on the three P112 frame orbits (frames 0, 2, 26) is **in progress** and nothing about P112 is claimed here. P104 has only 135 of 759 P-compatible frames; not attempted. +* No decoder cost, no κ, no statement for fields of positive characteristic (re-run `spans.py` mod `p` and re-check the sign logic), no formal-kernel check, no claim that the A2 family is a full component of the realisation variety. +* Zeros allowed on non-orthogonal pairs (§6). +* The audit is by the same author's tooling (an independent Opus read-only run), not a human review. + +## 8. Files + +`checks/` `e8lib.py` (lines, frames, tetrads), `a2e8.py`, `spans.py`, `spans3.py`, `pframes.py`, `s56.py`, `pin.py`, `soundtest.py`, `rupc.c` (auxiliary), `rup.py`, `modrank.py`, `manifest_check.py`; `evidence/` card snapshots (BSTAR, CONJB, KSTAR), `pins.tsv` (sha256 of generated objects), `proofs/pin3.drat.xz`, `logs/`; `verify.sh`, `MANIFEST.sha256`, `SOURCES.json`, `requirements.txt`, `LICENSE`, `NOTICE.md`. + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0. diff --git a/research/e8-rank9-realisations/SOURCES.json b/research/e8-rank9-realisations/SOURCES.json new file mode 100644 index 0000000000..d6b61b20a0 --- /dev/null +++ b/research/e8-rank9-realisations/SOURCES.json @@ -0,0 +1,4 @@ +{ + "description": "Provenance for research/e8-rank9-realisations. checks/ = own code (pin.py, s56.py, soundtest.py, spans3.py, rup.py, rupc.c are the working cards' KSTAR scripts with the E8 setup made self-contained and the audit's soundtest fix; spans.py, pframes.py are E8-only restatements of CONJB spans.py / BSTAR pcompat.py + hset3.py; a2e8.py restates CONJB a2fam.py plus a B-form builder). evidence/*_THEORY_snapshot.md = exported card texts (copies, absolute paths stripped). evidence/proofs/pin3.drat.xz = kissat 4.0.4 DRAT proof. Tools (not vendored): kissat 4.0.4, drat-trim.", + "evidence": ["evidence/KSTAR_THEORY_snapshot.md", "evidence/BSTAR_THEORY_snapshot.md", "evidence/CONJB_THEORY_snapshot.md", "evidence/pins.tsv", "evidence/proofs/pin3.drat.xz", "evidence/logs/audit_dratrim_pin3.log.txt", "evidence/logs/dratrim_shipped_pin3.log.txt", "evidence/logs/kstar_cert2_E8_pin3_rupc.log.txt", "evidence/logs/kstar_s56_E8_f1_0-15.log.txt"] +} diff --git a/research/e8-rank9-realisations/checks/a2e8.py b/research/e8-rank9-realisations/checks/a2e8.py new file mode 100644 index 0000000000..7356b7634c --- /dev/null +++ b/research/e8-rank9-realisations/checks/a2e8.py @@ -0,0 +1,74 @@ +# Exact rank-9 realisations of the E8 iff pattern: the A2 family (CONJB 1.2) and B-form (D1 G D2 + c beta^T), with checks. +# A2: rows a_u=(r_u,0) off X, a_{u_i}=(r_i+g_i,1); cols b_s=(r_s,z_s), z_s=-g_i.r_s on O_{u_i}, z free on X (g_1=0, g_2,g_3 in span(r_1,r_2)). +# B : a_u=(d1_u r_u, c_u), b_s=(d2_s r_s, beta_s) with c_u beta_s = 0 on orthogonal pairs. +# usage: python a2e8.py (prints PASS lines). Also imported by soundtest.py (build_a2, build_b). +import random, itertools +from fractions import Fraction as Fr +from e8lib import E,N,G,O,dot +from modrank import rkp +R=[[Fr(x) for x in r] for r in E] +idx={tuple(r):i for i,r in enumerate(R)} +def line_of(w): + t=tuple(w); n=tuple(-x for x in w) + return idx.get(t, idx.get(n)) +def a2_triangles(): + out=set() + for i in range(N): + for j in range(i+1,N): + if G[i][j]==0: continue + s=1 if G[i][j]>0 else -1 + k=line_of([a-s*b for a,b in zip(R[i],R[j])]) + if k is not None and k not in (i,j): out.add(tuple(sorted((i,j,k)))) + return sorted(out) +TRI=a2_triangles() +def build_a2(seed,tri=None): + rnd=random.Random(seed); u=TRI[0] if tri is None else TRI[tri % len(TRI)] + g=[[Fr(0)]*8] + for _ in range(2): + al,be=rnd.randint(-9,9),rnd.randint(-9,9) + g.append([al*a+be*b for a,b in zip(R[u[0]],R[u[1]])]) + z=[None]*N + for s in range(N): + vals={-dot(g[i],R[s]) for i in range(3) if G[u[i]][s]==0} + assert len(vals)<=1,'inconsistent z' + z[s]=vals.pop() if vals else Fr(rnd.randint(-50,50),rnd.randint(1,7)) + A=[R[s]+[Fr(0)] for s in range(N)] + for i in range(3): A[u[i]]=[a+b for a,b in zip(R[u[i]],g[i])]+[Fr(1)] + B=[R[s]+[z[s]] for s in range(N)] + return u,A,B +def build_b(seed,kind='single'): + # redraw the free scalars until no accidental extra zero occurs (a cancellation d1 d2 G + c beta = 0 on a non-orthogonal pair) + for t in range(1000): + S,Sb,A,B=_build_b(seed*1000+t,kind) + M=[[dot(A[i],B[j]) for j in range(N)] for i in range(N)] + if not any((M[i][j]==0)!=(i!=j and G[i][j]==0) for i in range(N) for j in range(N)): return S,Sb,A,B + raise RuntimeError +def _build_b(seed,kind): + rnd=random.Random(seed) + if kind=='single': + u0=rnd.randrange(N); S=[u0]; Sb=[s for s in range(N) if G[u0][s]!=0] # supp c = {u0}, supp beta = Nbar[u0] + else: # clique supp c, common non-neighbours + S=[]; c=list(range(N)); rnd.shuffle(c) + for u in c: + if all(G[u][w]!=0 for w in S): S.append(u) + Sb=[s for s in range(N) if all(G[s][w]!=0 for w in S)] + d1=[Fr(rnd.randint(1,5)) for _ in range(N)]; d2=[Fr(rnd.randint(1,5)) for _ in range(N)] + A=[[d1[u]*x for x in R[u]]+[Fr(rnd.randint(1,9)) if u in S else Fr(0)] for u in range(N)] + B=[[d2[s]*x for x in R[s]]+[Fr(rnd.randint(1,9)) if s in Sb else Fr(0)] for s in range(N)] + return S,Sb,A,B +def check(A,B,label): + M=[[dot(A[i],B[j]) for j in range(N)] for i in range(N)] + bad=[(i,j) for i in range(N) for j in range(N) if (M[i][j]==0)!=(i!=j and G[i][j]==0)] + return M,bad,(rkp(A)==9 and rkp(B)==9) # A,B of full column rank 9 (mod-p rank <= Q rank <= 9) => rank M = 9 +if __name__=='__main__': + print('A2 triangles in E8:',len(TRI)); assert len(TRI)==1120 + for seed,tri in [(1,0),(2,0),(3,17),(4,400),(5,1119)]: + u,A,B=build_a2(seed,tri); M,bad,full=check(A,B,'a2') + assert not bad and full + off=[w for w in range(N) if w not in u]; assert all(M[w][s]==dot(R[w],R[s]) for w in off for s in range(N)) + print('PASS A2 member seed %d triangle %s: iff pattern exact, rank 9, rows off X equal Gram rows'%(seed,list(u))) + for seed,kind in [(1,'single'),(2,'single'),(3,'clique'),(4,'clique')]: + S,Sb,A,B=build_b(seed,kind); M,bad,full=check(A,B,'b') + assert not bad and full and all(G[u][s]!=0 for u in S for s in Sb) + print('PASS B-form member seed %d (%s, |supp c|=%d, |supp beta|=%d): iff pattern exact, rank 9'%(seed,kind,len(S),len(Sb))) + print('PASS a2e8') diff --git a/research/e8-rank9-realisations/checks/e8lib.py b/research/e8-rank9-realisations/checks/e8lib.py new file mode 100644 index 0000000000..d802266a28 --- /dev/null +++ b/research/e8-rank9-realisations/checks/e8lib.py @@ -0,0 +1,40 @@ +# E8 lines (120, in the fixed order used by every card of this series), Gram matrix, orthogonality sets, frames (8 pairwise orthogonal lines), tetrads w.r.t. a frame. +# (Same order as BSTAR/blib.py of the working cards: the CNF regeneration in verify.sh is byte-identical only for this order.) +import itertools +from fractions import Fraction as F +def e8_roots(): + R=[] + for i,j in itertools.combinations(range(8),2): + for si in(1,-1): + for sj in(1,-1): + r=[F(0)]*8; r[i]=F(si); r[j]=F(sj); R.append(tuple(r)) + for s in itertools.product((1,-1),repeat=8): + if s.count(-1)%2==0: R.append(tuple(F(x,2) for x in s)) + return R +def lines(R): + seen=set();L=[] + for r in R: + n=tuple(-x for x in r) + if n in seen: continue + seen.add(r); L.append(r) + return L +E=lines(e8_roots()); N=len(E) +assert N==120 +dot=lambda x,y: sum(a*b for a,b in zip(x,y)) +G=[[dot(E[i],E[j]) for j in range(N)] for i in range(N)] +O=[frozenset(s for s in range(N) if G[u][s]==0) for u in range(N)] +UNITS={'E8':frozenset(range(N))} +def frames(S=None): + S=sorted(S if S is not None else range(N)); out=[] + def rec(cur,cand): + if len(cur)==8: out.append(tuple(cur)); return + for i,c in enumerate(cand): + if cur and c ") must match the file; the manifest must list every file of the package except itself. +import hashlib, os, sys +root = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) +listed = {} +for l in open(os.path.join(root, 'MANIFEST.sha256')): + h, p = l.rstrip('\n').split(' ', 1); listed[p] = h +bad = [p for p, h in listed.items() if not os.path.isfile(os.path.join(root, p)) or hashlib.sha256(open(os.path.join(root, p), 'rb').read()).hexdigest() != h] +allf = {os.path.relpath(os.path.join(d, f), root) for d, _, fs in os.walk(root) for f in fs if '__pycache__' not in d and f != 'MANIFEST.sha256' and not f.endswith('.pyc')} +extra = sorted(allf - set(listed)) +print(('FAIL' if bad else 'PASS') + ' manifest: %d files hash-checked, %d mismatching %s' % (len(listed), len(bad), bad[:3])) +print(('FAIL' if extra else 'PASS') + ' manifest lists every package file (%d unlisted %s)' % (len(extra), extra[:3])) +sys.exit(1 if bad or extra else 0) diff --git a/research/e8-rank9-realisations/checks/modrank.py b/research/e8-rank9-realisations/checks/modrank.py new file mode 100644 index 0000000000..2eb6120da9 --- /dev/null +++ b/research/e8-rank9-realisations/checks/modrank.py @@ -0,0 +1,15 @@ +# rank over GF(p) of a rational matrix (lower bound for the rank over Q); p large prime +P=2**61-1 +def rkp(rows,p=P): + A=[[ (x.numerator*pow(x.denominator,-1,p))%p for x in r] for r in rows] + r=0; n=len(A[0]) if A else 0 + for c in range(n): + piv=next((i for i in range(r,len(A)) if A[i][c]),None) + if piv is None: continue + A[r],A[piv]=A[piv],A[r]; inv=pow(A[r][c],-1,p) + A[r]=[x*inv%p for x in A[r]] + for i in range(len(A)): + if i!=r and A[i][c]: + f=A[i][c]; A[i]=[(x-f*y)%p for x,y in zip(A[i],A[r])] + r+=1 + return r diff --git a/research/e8-rank9-realisations/checks/pframes.py b/research/e8-rank9-realisations/checks/pframes.py new file mode 100644 index 0000000000..013e756b35 --- /dev/null +++ b/research/e8-rank9-realisations/checks/pframes.py @@ -0,0 +1,24 @@ +# BSTAR pcompat.py / hset3.py, E8 only (CHECKED): a frame F is P-compatible if every eps-class (4 lines) at every pair of every F-tetrad has a line in L and every sign pattern (eps_ab,eps_bc) (2 lines) of every triple does (L = E8: always). +# Used by Theorem P / A (BSTAR): every orthogonal pair lies in a P-compatible frame. +import itertools +from e8lib import * +FR=frames(); print('frames',len(FR)); assert len(FR)==2025 +sg=lambda u,a,b: 1 if G[u][a]*G[u][b]>0 else -1 +PC=0; cov=set() +for f in FR: + ok=True + for k,ls in tetrads(f).items(): + kk=sorted(k) + for a,b in itertools.combinations(kk,2): + for e in (1,-1): + if not any(sg(u,a,b)==e for u in ls): ok=False + for a,b,c in itertools.combinations(kk,3): + for e1 in (1,-1): + for e2 in (1,-1): + if not any(sg(u,a,b)==e1 and sg(u,b,c)==e2 for u in ls): ok=False + PC+=ok + if ok: cov.update(itertools.combinations(sorted(f),2)) +allp=[p for p in itertools.combinations(range(N),2) if G[p[0]][p[1]]==0] +print('P-compatible frames',PC,'/',len(FR),'| orthogonal pairs covered',sum(p in cov for p in allp),'/',len(allp)) +assert PC==2025 and len(allp)==3780 and all(p in cov for p in allp) +print('PASS pframes: all 2025 E8 frames are P-compatible; all 3780 orthogonal pairs lie in a frame') diff --git a/research/e8-rank9-realisations/checks/pin.py b/research/e8-rank9-realisations/checks/pin.py new file mode 100644 index 0000000000..34776a4510 --- /dev/null +++ b/research/e8-rank9-realisations/checks/pin.py @@ -0,0 +1,172 @@ +# KSTAR round 2: P^1-valued pinning abstraction (sound) in pivot coordinates w.r.t. a frame F of E8. +# Per pair p={a,b} of F: every row u with p ⊆ T(u) has ratio rho_p(u)=alpha_u(b)/alpha_u(a) in K*, every column s has +# tau_p(s)=-beta_s(a)/beta_s(b) in K*, so that alpha_u|p . beta_s|p = alpha_u(a) beta_s(b) (rho - tau). +# Boolean: x[u] (x_u != 0), y[s]; E[p][(e,e')] equality of values (transitive). +# Rules (each proven in THEORY §6): ORTH, NON, TRI (row-row / col-col / row-col), K3 (local lemma), ZZ, Schur. +import sys, itertools, os +import os as _o; sys.path.insert(0,_o.path.dirname(_o.path.abspath(__file__))) +from e8lib import * +cl=[]; nv=[0] +def new(): nv[0]+=1; return nv[0] +def build(Fr, opts): + Fr=tuple(Fr); TT=tetrads(Fr); tets=list(TT); off=[u for u in range(N) if u not in Fr] + Tof={u:T for T in tets for u in TT[T]} + X={u:new() for u in off}; Y={u:new() for u in off} + sg=lambda u,a,b: 1 if dot(E[u],E[a])*dot(E[u],E[b])>0 else -1 + pairs=[frozenset(p) for p in itertools.combinations(Fr,2)] + EQ={} + for p in pairs: + el=[('r',u) for u in off if p<=Tof[u]]+[('c',u) for u in off if p<=Tof[u]] + V={} + for e1,e2 in itertools.combinations(el,2): V[(e1,e2)]=V[(e2,e1)]=new() + for e1,e2,e3 in itertools.combinations(el,3): + a_,b_,c_=V[(e1,e2)],V[(e2,e3)],V[(e1,e3)] + cl.extend([[-a_,-b_,c_],[-a_,-c_,b_],[-b_,-c_,a_]]) + EQ[p]=V + # Schur + for T in tets: + Tc=frozenset(Fr)-T + for u in TT[T]: + for s in TT[Tc]: cl.append([-X[u],-Y[s]]) + for p in pairs: + a,b=sorted(p); V=EQ[p]; ts=[T for T in tets if p<=T] + # ORTH / NON between different tetrads through p + for T1 in ts: + for T2 in ts: + if T1==T2: continue + for u in TT[T1]: + for s in TT[T2]: + e=V[(('r',u),('c',s))] + if sg(u,a,b)!=sg(s,a,b): # orthogonal + cl.append([X[u],e]); cl.append([Y[s],e]); cl.append([-X[u],-Y[s],-e]) + else: + cl.append([X[u],-e]); cl.append([Y[s],-e]) + # K3 local lemma + ZZ + for eps in (1,-1): + for i,Ti in enumerate(ts): + R=[u for u in TT[Ti] if sg(u,a,b)==eps] + C=[s for T2 in ts if T2!=Ti for s in TT[T2] if sg(s,a,b)==-eps] + Rr=[u for T2 in ts if T2!=Ti for u in TT[T2] if sg(u,a,b)==eps] + Cc=[s for s in TT[Ti] if sg(s,a,b)==-eps] + # rows R in T_i vs columns C: dim U_i>=2 => all C equal value and equal y-status + for u,w in itertools.combinations(R,2): + e=V[(('r',u),('r',w))] + for s,t in itertools.combinations(C,2): + f=V[(('c',s),('c',t))] + for cond in ([e],[-e,-X[u],X[w]],[-e,X[u],-X[w]]): + cl.append(cond+[f]); cl.append(cond+[-Y[s],Y[t]]); cl.append(cond+[Y[s],-Y[t]]) + cl.append([X[u],X[w],e]) # ZZ + # transposed: columns of T_i ((-eps) class) vs rows of other tetrads (eps class) + for s,t in itertools.combinations(Cc,2): + f=V[(('c',s),('c',t))] + for u,w in itertools.combinations(Rr,2): + e=V[(('r',u),('r',w))] + for cond in ([f],[-f,-Y[s],Y[t]],[-f,Y[s],-Y[t]]): + cl.append(cond+[e]); cl.append(cond+[-X[u],X[w]]); cl.append(cond+[X[u],-X[w]]) + cl.append([Y[s],Y[t],f]) + # TRI: triples inside a tetrad + for T in tets: + for tri in itertools.combinations(sorted(T),3): + a,b,c=tri; P3=[frozenset((a,b)),frozenset((b,c)),frozenset((a,c))] + el=[('r',u) for u in TT[T]]+[('c',u) for u in TT[T]] + for e1,e2 in itertools.combinations(el,2): + vs=[EQ[q][(e1,e2)] for q in P3] + same=(e1[0]==e2[0]) + for k in range(3): + o=[vs[j] for j in range(3) if j!=k] + if same: cl.append([-o[0],-o[1],vs[k]]) + else: cl.append([-o[0],-o[1],-vs[k]]) + + # TW (twist rule): dim U_i = 1 at (p,eps) whenever the (-eps) columns of the other two tetrads span >= 2 dims + # (two columns with different psi, or a Z' and a D' column). Then x_u = t*alpha_u(a) on the class. + # Two disjoint pairs p, p' with p ∪ p' = T: rows u,w in a common 1-dim class at p and at p', x_u,x_w != 0 + # => alpha(c)/alpha(a) equal => EQ_{ac}(u,w). Transposed for columns. + if opts.get('tw',1): + D1={}; globals()['D1_']=D1 + for p in pairs: + a,b=sorted(p); V=EQ[p]; ts=[T for T in tets if p<=T] + for eps in (1,-1): + for Ti in ts: + for kind,P_,Q_ in (('r',X,Y),('c',Y,X)): + okind='c' if kind=='r' else 'r' + C=[s for T2 in ts if T2!=Ti for s in TT[T2] if sg(s,a,b)==-eps] + d=new(); D1[(kind,p,eps,Ti)]=d + for s,t in itertools.combinations(C,2): + cl.append([V[((okind,s),(okind,t))],d]) # different psi => d + cl.append([-Q_[s],Q_[t],d]); cl.append([Q_[s],-Q_[t],d]) # Z'/D' mix => d + for T in tets: + Ts=sorted(T) + for a,b in itertools.combinations(Ts,2): + c,dd=[i for i in Ts if i not in (a,b)] + p=frozenset((a,b)); q=frozenset((c,dd)) + for kind,P_ in (('r',X),('c',Y)): + for u,w in itertools.combinations(TT[T],2): + if sg(u,a,b)!=sg(w,a,b) or sg(u,c,dd)!=sg(w,c,dd): continue + e1=D1[(kind,p,sg(u,a,b),T)]; e2=D1[(kind,q,sg(u,c,dd),T)] + tgt=EQ[frozenset((a,c))][((kind,u),(kind,w))] + cl.append([-e1,-e2,-P_[u],-P_[w],tgt]) + + # RATIO rules: rat_i(u) := x_u/alpha_u(i) (rows with x_u != 0, i in T(u)); columns likewise with y. + if opts.get('ratio',1): + RQ={}; globals()['RQ_']=RQ + for kind,P_ in (('r',X),('c',Y)): + for i in Fr: + el=[u for u in off if i in Tof[u]]; Vr={} + for u,w in itertools.combinations(el,2): Vr[(u,w)]=Vr[(w,u)]=new() + for u,w,z in itertools.combinations(el,3): + a_,b_,c_=Vr[(u,w)],Vr[(w,z)],Vr[(u,z)] + cl.extend([[-a_,-b_,c_],[-a_,-c_,b_],[-b_,-c_,a_]]) + RQ[(kind,i)]=Vr + for p in pairs: + a,b=sorted(p); V=EQ[p]; ts=[T for T in tets if p<=T] + for kind,P_,Q_ in (('r',X,Y),('c',Y,X)): + okind='c' if kind=='r' else 'r' + el=[u for u in off if p<=Tof[u]] + # Q2: two of {rat_a, rat_b, eq_ab} => third (x != 0 on both) + for u,w in itertools.combinations(el,2): + t=[RQ[(kind,a)][(u,w)],RQ[(kind,b)][(u,w)],V[((kind,u),(kind,w))]] + for k in range(3): + o=[t[j] for j in range(3) if j!=k] + cl.append([-P_[u],-P_[w],-o[0],-o[1],t[k]]) + for eps in (1,-1): + for Ti in ts: + Rcl=[u for u in TT[Ti] if sg(u,a,b)==eps] + d=D1[(kind,p,eps,Ti)] + for u,w in itertools.combinations(Rcl,2): + cl.append([-d,V[((kind,u),(kind,w))]]) + cl.append([-d,-P_[u],P_[w]]); cl.append([-d,P_[u],-P_[w]]) + for i in (a,b): cl.append([-d,-P_[u],-P_[w],RQ[(kind,i)][(u,w)]]) + # common D' (resp. D) partner: u in T_i, w in T_k (eps), s in T_j (-eps), j != i,k + for Ti,Tk in itertools.permutations(ts,2): + if Ti>Tk: continue + Tj=[T for T in ts if T not in (Ti,Tk)][0] + Rs=[u for u in TT[Ti] if sg(u,a,b)==eps]; Rk=[u for u in TT[Tk] if sg(u,a,b)==eps] + Cs=[s_ for s_ in TT[Tj] if sg(s_,a,b)==-eps] + for u in Rs: + for w in Rk: + for s_ in Cs: + for i in (a,b): cl.append([-P_[u],-P_[w],-Q_[s_],-V[((kind,u),(kind,w))],RQ[(kind,i)][(u,w)]]) + # residue hypotheses + if opts.get('residue',1): + for s in range(N): + cl.append([X[u] for u in O[s] if u in X]); cl.append([Y[u] for u in O[s] if u in Y]) + # not row-Gram-shaped and not column-Gram-shaped + for kind,Z in (('r',X),('c',Y)): + if not opts.get('notgram',1): break + opt=[] + for p in pairs: + a,b=sorted(p); V=EQ[p]; el=[u for u in off if p<=Tof[u]] + for u,w in itertools.combinations(el,2): + e=V[((kind,u),(kind,w))] + if sg(u,a,b)==sg(w,a,b): opt.append(-e) + else: opt.append(e) + cl.append(opt) + cl.append([X[u] for u in off]); cl.append([Y[u] for u in off]) + return X,Y,EQ +if __name__=='__main__': + opts={k:int(v) for k,v in (a.split('=') for a in sys.argv[2:])} + build(frames()[0],opts) + with open(sys.argv[1],'w') as f: + f.write(f'p cnf {nv[0]} {len(cl)}\n') + for c in cl: f.write(' '.join(map(str,c))+' 0\n') + print(nv[0],len(cl)) diff --git a/research/e8-rank9-realisations/checks/rup.py b/research/e8-rank9-realisations/checks/rup.py new file mode 100644 index 0000000000..dbffb47bbc --- /dev/null +++ b/research/e8-rank9-realisations/checks/rup.py @@ -0,0 +1,71 @@ +# Minimal independent RUP checker (deletions ignored: sound, every kept clause is implied). Usage: rup.py F.cnf P.drat +import sys +def read(fn): + out=[] + for l in open(fn): + if l[0] in 'pc': continue + t=l.split(); + if not t: continue + d=t[0]=='d' + lits=[int(x) for x in (t[1:] if d else t)]; assert lits[-1]==0 + out.append((d,lits[:-1])) + return out +F=[c for _,c in read(sys.argv[1])]; P=read(sys.argv[2]) +clauses=[]; watch={} +val={} +def addc(c): + c=list(dict.fromkeys(c)); k=len(clauses); clauses.append(c) + for l in c[:2]: watch.setdefault(l,[]).append(k) + return k +units=[] +def propagate(assign,trail,start): + i=start + while i1 and c[1]!=fl: keep.append(k); continue + if assign.get(c[0]) is True: keep.append(k); continue + found=False + for m in range(2,len(c)): + if assign.get(c[m]) is not False: + c[1],c[m]=c[m],c[1]; watch.setdefault(c[1],[]).append(k); found=True; break + if found: continue + keep.append(k) + if assign.get(c[0]) is False: + keep.extend(ws[j:]); watch[fl]=keep; return False + if assign.get(c[0]) is None: + assign[c[0]]=True; assign[-c[0]]=False; trail.append(c[0]) + watch[fl]=keep + return True +def check(c): + # RUP: assign negation, propagate (with unit clauses), expect conflict + assign={}; trail=[] + for l in c: + if assign.get(-l) is True: continue + if assign.get(l) is True: return True + assign[-l]=True; assign[l]=False; trail.append(-l) + for u in unitlits: + if assign.get(u) is False: return True + if assign.get(u) is None: assign[u]=True; assign[-u]=False; trail.append(u) + return not propagate(assign,trail,0) +unitlits=[] +for c in F: + if len(c)==1: unitlits.append(c[0]) + else: addc(c) +n=0 +for d,c in P: + if d: continue + if not check(c): print('FAIL lemma',n,c); sys.exit(1) + n+=1 + if len(c)==0: print('VERIFIED: empty clause derived by RUP after',n,'lemmas'); sys.exit(0) + if len(c)==1: unitlits.append(c[0]) + else: addc(c) +print('no empty clause'); sys.exit(2) diff --git a/research/e8-rank9-realisations/checks/rupc.c b/research/e8-rank9-realisations/checks/rupc.c new file mode 100644 index 0000000000..06e7b0bf56 --- /dev/null +++ b/research/e8-rank9-realisations/checks/rupc.c @@ -0,0 +1,92 @@ +/* rupc: minimal independent forward RUP checker for text DRAT proofs (KSTAR). + Usage: rupc F.cnf P.drat + Every added lemma must be RUP w.r.t. all clauses present (original + earlier lemmas, deletions honoured lazily). + Top-level implied literals are kept across deletions (sound: every clause ever present is implied by F). + RAT lemmas are NOT accepted. Prints VERIFIED only if the empty clause is reached (or a top-level conflict arises). */ +#include +#include +#include +#include + +static int nvars; +static int *lits; static long nl, capl; /* literal arena */ +static long *cstart; static int *csize; static char *cdel; static long nc, capc; +static long **W; static int *wn, *wc; /* watches indexed by lit code */ +static signed char *val; /* per var: 0 unassigned, 1 true, -1 false */ +static int *trail; static long tn; +#define CODE(l) ((l)>0 ? 2*(l) : -2*(l)+1) +static int litval(int l){ int v=val[abs(l)]; return l>0? v : -v; } +static void addw(int l,long c){ int k=CODE(l); if(wn[k]==wc[k]){ wc[k]=wc[k]?2*wc[k]:4; W[k]=realloc(W[k],sizeof(long)*wc[k]); } W[k][wn[k]++]=c; } +static void assign(int l){ val[abs(l)]= l>0?1:-1; trail[tn++]=l; } +/* hash table for deletion lookup */ +static long *ht; static long hcap; +static uint64_t hclause(const int *a,int n){ uint64_t h=1469598103934665603ULL; uint64_t s=0,x=0; for(int i=0;i=0) h=(h+1)%hcap; ht[h]=c; } +static int sameset(const int *a,int n,long c){ if(csize[c]!=n) return 0; for(int i=0;i=0 && !cdel[c] && sameset(a,n,c)){ cdel[c]=1; ht[h]=-2; return; } h=(h+1)%hcap; } } +/* propagate from trail position q; return 1 on conflict */ +static int propagate(long q){ + while(qcapl){ capl=capl?2*capl:1<<24; lits=realloc(lits,sizeof(int)*capl); } + long c=nc++; cstart[c]=nl; csize[c]=n; cdel[c]=0; memcpy(lits+nl,a,sizeof(int)*n); nl+=n; + if(nc*2>hcap*1){ /* rehash */ long old=hcap; hcap=hcap?4*hcap:1<<22; free(ht); ht=malloc(sizeof(long)*hcap); for(long i=0;i=2){ addw(cl[0],c); addw(cl[1],c);} assign(cl[0]); if(propagate(tn-1)) topconflict=1; return c; } + addw(cl[0],c); addw(cl[1],c); return c; +} +static int *buf; static int bcap; +static int readclause(FILE *f,int *isdel,int *n){ + int c,l; *n=0; *isdel=0; + for(;;){ c=fgetc(f); if(c==EOF) return 0; if(c=='c'||c=='p'){ while((c=fgetc(f))!='\n'&&c!=EOF); continue; } if(c=='d'){ *isdel=1; break; } if(c=='-'||(c>='0'&&c<='9')){ ungetc(c,f); break; } } + for(;;){ if(fscanf(f,"%d",&l)!=1) return 0; if(l==0) return 1; if(*n==bcap){ bcap=bcap?2*bcap:64; buf=realloc(buf,sizeof(int)*bcap);} buf[(*n)++]=l; if(abs(l)>nvars){ fprintf(stderr,"var out of range\n"); exit(3);} } +} +int main(int argc,char **argv){ + FILE *f=fopen(argv[1],"r"); char line[256]; long ncl; + while(fgets(line,256,f)) if(line[0]=='p'){ sscanf(line,"p cnf %d %ld",&nvars,&ncl); break; } + val=calloc(nvars+1,1); trail=malloc(sizeof(int)*(nvars+1)); W=calloc(2*nvars+2,sizeof(long*)); wn=calloc(2*nvars+2,sizeof(int)); wc=calloc(2*nvars+2,sizeof(int)); + int isdel,n; long cnt=0; + while(readclause(f,&isdel,&n)){ addclause(buf,n); cnt++; } + fclose(f); fprintf(stderr,"read %ld clauses, top-level trail %ld, conflict %d\n",cnt,tn,topconflict); + if(topconflict){ printf("VERIFIED: formula refuted by unit propagation alone\n"); return 0; } + FILE *p=fopen(argv[2],"r"); long lem=0,dels=0; + while(readclause(p,&isdel,&n)){ + if(isdel){ hdel(buf,n); dels++; continue; } + /* RUP check */ + long save=tn; int ok=0; + for(int i=0;isave){ val[abs(trail[--tn])]=0; } + if(!ok){ printf("FAIL at lemma %ld (size %d)\n",lem,n); return 1; } + lem++; + if(n==0){ printf("VERIFIED: empty clause derived by RUP after %ld lemmas (%ld deletions)\n",lem,dels); return 0; } + addclause(buf,n); + if(topconflict){ printf("VERIFIED: top-level conflict after %ld lemmas (%ld deletions)\n",lem,dels); return 0; } + } + printf("no empty clause\n"); return 2; +} diff --git a/research/e8-rank9-realisations/checks/s56.py b/research/e8-rank9-realisations/checks/s56.py new file mode 100644 index 0000000000..f5ea3c74cb --- /dev/null +++ b/research/e8-rank9-realisations/checks/s56.py @@ -0,0 +1,44 @@ +# 56-problem: rows u -> points P_u, columns s -> lines l_s in a projective plane, P_u on l_s whenever u ⊥ s (u,s in Nbar(f1)). +# Abstraction (sound): equality vars f[u,u'] (same point), e[s,s'] (same line); transitivity; incidence axiom: +# distinct points u,u' with two common lines s,s' (both in Γ(u)∩Γ(u')) => e[s,s']; dually. +# Negated conclusion: no point-class A0 meeting Γ(s) for every column s, and no line-class B0 meeting Γ(u) for every row u. +import sys, itertools, os as _o; sys.path.insert(0,_o.path.dirname(_o.path.abspath(__file__))) +from e8lib import * +f1=int(sys.argv[2]) if len(sys.argv)>2 else 0 +import os +LU=UNITS[os.environ.get('UNIT','E8')] +assert f1 in LU +S=[u for u in sorted(LU) if G[u][f1]!=0 and u!=f1]; n=len(S) +Gam=[[j for j in range(n) if S[j] in O[S[i]]] for i in range(n)] +nv=[0]; cl=[] +def new(): nv[0]+=1; return nv[0] +def eqvars(): + V={} + for i in range(n): + for j in range(i+1,n): V[(i,j)]=V[(j,i)]=new() + for i,j,k in itertools.combinations(range(n),3): + a,b,c=V[(i,j)],V[(j,k)],V[(i,k)] + cl.extend([[-a,-b,c],[-a,-c,b],[-b,-c,a]]) + return V +Fp=eqvars(); El=eqvars() +for P,Q in ((Fp,El),(El,Fp)): + for i in range(n): + for j in range(i+1,n): + com=sorted(set(Gam[i])&set(Gam[j])) + for s,t in itertools.combinations(com,2): cl.append([P[(i,j)],Q[(s,t)]]) +def negdom(P): + # for every row-class representative i: exists column s with no Γ(s)-row equal to i (and i not in Γ(s)) + for i in range(n): + opts=[] + for s in range(n): + if i in Gam[s]: continue + w=new(); opts.append(w) + for u in Gam[s]: cl.append([-w,-P[(i,u)]]) + cl.append(opts) +import os +if os.environ.get("SIDE","both") in ("both","rows"): negdom(Fp) +if os.environ.get("SIDE","both") in ("both","cols"): negdom(El) +with open(sys.argv[1],'w') as fh: + fh.write(f'p cnf {nv[0]} {len(cl)}\n') + for c in cl: fh.write(' '.join(map(str,c))+' 0\n') +print(nv[0],len(cl)) diff --git a/research/e8-rank9-realisations/checks/soundtest.py b/research/e8-rank9-realisations/checks/soundtest.py new file mode 100644 index 0000000000..670d238b57 --- /dev/null +++ b/research/e8-rank9-realisations/checks/soundtest.py @@ -0,0 +1,86 @@ +# Soundness test of pin.py's clauses: evaluate every clause on the true Boolean data of actual rank-9 realisations +# (E8 A2 instance, B-form instances), for many frames. Any violated clause = unsound rule. +import sys, os, random, itertools, numpy as np +sys.path.insert(0,os.path.dirname(os.path.abspath(__file__))); import pin +from pin import * +rng=np.random.default_rng(int(sys.argv[1]) if len(sys.argv)>1 else 0) +Rr=np.array(E,float); Gm=Rr@Rr.T +def bform(S,Sb): + A=np.hstack([Rr,np.zeros((N,1))]); B=np.hstack([Rr,np.zeros((N,1))]) + A[S,8]=rng.normal(size=len(S)); B[Sb,8]=rng.normal(size=len(Sb)) + d1=np.exp(rng.normal(size=N)*0.3); d2=np.exp(rng.normal(size=N)*0.3) + return (A*d1[:,None])@(B*d2[:,None]).T +def a2(seed,tri): + import a2e8 + for t in range(1000): # redraw until the exact iff pattern holds (an unlucky draw creates an extra zero: not a realisation) + u,A,B=a2e8.build_a2(seed+1000*t,tri); _,bad,full=a2e8.check(A,B,'a2') + if not bad and full: break + else: raise RuntimeError + A=np.array([[float(x) for x in r] for r in A]); B=np.array([[float(x) for x in r] for r in B]) + return A@B.T, u +def cliques8(): + # greedy random clique + for _ in range(1000): + S=[]; c=list(range(N)); random.shuffle(c) + for u in c: + if all(Gm[u,w]!=0 for w in S): S.append(u) + if len(S)>=6: return S +insts=[] +u0=0; insts.append(('B single row',bform([u0],[s for s in range(N) if Gm[u0,s]!=0]))) +S=cliques8(); comn=[s for s in range(N) if all(Gm[s,w]!=0 for w in S)] +insts.append(('B clique %d/%d'%(len(S),len(comn)),bform(S,comn))) +for sd,tri in [(3,0),(11,150),(12,611),(13,900),(14,1119)]: # several A2 parameter draws on several triangles (audit fix) + Ma,tu=a2(sd,tri); insts.append(('A2 seed %d triangle %s'%(sd,tu),Ma)) +FR=frames(); tol=1e-7 +def assign(M,Fr): + off=[u for u in range(N) if u not in Fr] + Mt=sum(np.outer(M[:,f],M[f,:])/M[f,f] for f in Fr); R=M-Mt + U,s_,Vt=np.linalg.svd(R); x=U[:,0]*s_[0]; y=Vt[0] + assert s_[1]<1e-8*max(1,s_[0]), s_[:3] + sc=np.abs(M).max() + xb={u:bool(abs(x[u])>tol*max(1,np.abs(x).max())) for u in off}; yb={u:bool(abs(y[u])>tol*max(1,np.abs(y).max())) for u in off} + al=lambda u,f: M[u,f]/M[f,f]; be=lambda s,f: M[f,s] + return off,x,y,xb,yb,al,be +def close(a,b): return bool(abs(a-b)<=1e-6*max(1,abs(a),abs(b))) +bad_total=0 +for name,M in insts: + s_=np.linalg.svd(M,compute_uv=False); print(name,'rank9 ratio %.1e'%(s_[8]/s_[0]), 'orth max %.1e'%np.abs(M[(Gm==0)&~np.eye(N,dtype=bool)]).max()) + for Fr in [FR[i] for i in rng.choice(len(FR),int(sys.argv[2]) if len(sys.argv)>2 else 8,replace=False)]: + pin.cl.clear(); pin.nv[0]=0 + X,Y,EQ=pin.build(Fr,dict(residue=0,notgram=0)) + D1=pin.D1_; RQ=pin.RQ_ + off,x,y,xb,yb,al,be=assign(M,Fr) + val={} + for u in off: val[X[u]]=xb[u]; val[Y[u]]=yb[u] + TT=tetrads(Fr); Tof={u:T for T in TT for u in TT[T]} + for p,V in EQ.items(): + a,b=sorted(p) + def v_(e): + k,u=e + return al(u,b)/al(u,a) if k=='r' else -be(u,a)/be(u,b) + done=set() + for (e1,e2),var in V.items(): + if var in done: continue + done.add(var); val[var]=close(v_(e1),v_(e2)) + for (kind,i),Vr in RQ.items(): + for (u,w),var in Vr.items(): + if kind=='r': r1=x[u]/al(u,i) if xb[u] else 0; r2=x[w]/al(w,i) if xb[w] else 0 + else: r1=y[u]/be(u,i) if yb[u] else 0; r2=y[w]/be(w,i) if yb[w] else 0 + val[var]=close(r1,r2) + for key,d in D1.items(): val[d]=False + # D1 true iff its forcing condition holds: easiest: set True if any forcing clause would be violated + for c in pin.cl: + pos=[l for l in c if l>0 and l in D1.values()] if False else None + dset=set(D1.values()) + for c in pin.cl: + ds=[l for l in c if l in dset] + if ds and all((val.get(abs(l)) if l>0 else not val.get(abs(l))) is False for l in c if abs(l) not in dset): + for l in ds: val[l]=True + nb=0 + for c in pin.cl: + if not any((val[abs(l)] if l>0 else not val[abs(l)]) for l in c): + nb+=1 + if nb<=3: print(' VIOLATED',c[:8]) + bad_total+=nb + print(' frame',Fr[:3],'|D|',sum(xb.values()),'|D\'|',sum(yb.values()),'violated',nb,flush=True) +print('TOTAL violated',bad_total) diff --git a/research/e8-rank9-realisations/checks/spans.py b/research/e8-rank9-realisations/checks/spans.py new file mode 100644 index 0000000000..1c2f761597 --- /dev/null +++ b/research/e8-rank9-realisations/checks/spans.py @@ -0,0 +1,11 @@ +# CONJB (S1)/(S2) for E8: r(O_u) spans r_u^perp (rank 7) for every u; r(O_u cap O_u') spans ^perp (rank 6) for u != u'. Ranks mod 2^61-1 (lower bounds over Q; the upper bounds 7, 6 are trivial), hence over every field of characteristic 0. +import itertools +from e8lib import E,N,O +from modrank import rkp +from fractions import Fraction as Fr +R=[[Fr(x) for x in r] for r in E] +s1=min(rkp([R[s] for s in O[u]]) for u in range(N)) +s2=min(rkp([R[s] for s in O[u]&O[w]]) for u,w in itertools.combinations(range(N),2)) +print('E8 lines',N,'S1 min rank',s1,'(need 7)','S2 min rank',s2,'(need 6)') +assert s1==7 and s2==6 +print('PASS spans E8') diff --git a/research/e8-rank9-realisations/checks/spans3.py b/research/e8-rank9-realisations/checks/spans3.py new file mode 100644 index 0000000000..db00d69635 --- /dev/null +++ b/research/e8-rank9-realisations/checks/spans3.py @@ -0,0 +1,30 @@ +# (S3') for E8: f fixed; u,u' in Nbar(f), u' not in {u, antipode(u)}: r(O_f ∩ O_u ∩ O_u') spans ^perp (dim 5). +# (W2) max number of directions w_u = proj_{f^perp} r_u (u in Nbar(f)) in a 2-plane. +import sys, os as _o; sys.path.insert(0,_o.path.dirname(_o.path.abspath(__file__))) +from e8lib import * +from fractions import Fraction as Fr +import sympy, itertools +def rank(rows): + return sympy.Matrix(rows).rank() if rows else 0 +f=0; S=[u for u in range(N) if G[u][f]!=0 and u!=f] +bad=0; cnt=0 +for u,v in itertools.combinations(S,2): + if G[u][v]!=0 and abs(G[u][v])!=0: + # antipode test: f,u,v span 2 dims + if rank([E[f],E[u],E[v]])==2: continue + com=[s for s in O[f] if s in O[u] and s in O[v]] + cnt+=1 + if rank([E[s] for s in com])!=5: bad+=1 +print('S3prime pairs',cnt,'bad',bad) +W=[[Fr(x)-Fr(dot(E[u],E[f]),dot(E[f],E[f]))*Fr(y) for x,y in zip(E[u],E[f])] for u in S] +dirs=[] +for w in W: + if not any(rank([w,d])==1 for d in dirs): dirs.append(w) +print('directions',len(dirs)) +mx=0 +for a,b in itertools.combinations(range(len(dirs)),2): + c=sum(1 for d in dirs if rank([dirs[a],dirs[b],d])==2) + mx=max(mx,c) +print('max directions in a 2-plane',mx) +assert bad==0 and len(dirs)==28 and mx==2 +print('PASS spans3: (S3prime) over %d pairs and (W2): 28 directions, no 3 in a 2-plane'%cnt) diff --git a/research/e8-rank9-realisations/evidence/BSTAR_THEORY_snapshot.md b/research/e8-rank9-realisations/evidence/BSTAR_THEORY_snapshot.md new file mode 100644 index 0000000000..85912719d4 --- /dev/null +++ b/research/e8-rank9-realisations/evidence/BSTAR_THEORY_snapshot.md @@ -0,0 +1,136 @@ +# BSTAR: towards Conjecture B* (rank-9 realisations of the P112 / P104 / E8 iff pattern) + +Labels: **PROVEN** (written proof here) · **CHECKED** (exact script in this folder) · **NUMERICAL** (floating point, evidence only) · **OPEN**. +python = W/venv/bin/python; run scripts from this folder. Inputs used: CONJB Theorem G, Lemma E, (S1)/(S2); UNIQ8 Theorem U and §1 coordinates. +Setting: M is a rank-9 pattern realisation on L ∈ {E8, P112, P104} over a field K of char ≠ 2 (iff pattern: M_tt ≠ 0, M_ts = 0 ⟺ t ⊥ s). +Factor M = ABᵀ with rows a_t, b_t ∈ K⁹. ρ_a(S) := dim span a(S), ρ_b(S) likewise. O_u = lines ⊥ u, Nbar(u) = lines not ⊥ u, u excluded. + +## §0 Status (BSTAR, Oct 15, final) +**E8 is the primary target** (P120: W(E8)-transitive; per coordinator, all floors are now equivalent to C(P120) ≥ 72). Every result below holds verbatim for E8. +- **Theorem P (pinning), PROVEN (§3).** Fix a P-compatible frame F ⊆ L and put D_F := {u : a_u ∉ span a(F)}. Call a pair {a,b} *unpinned* if, for some sign ε, + at most one of the three ε-classes at {a,b} (one per F-tetrad through {a,b}) meets L ∖ D_F. If the unpinned pairs form a matching, then + M[L∖D_F, :] consists of Gram rows, and by CONJB Theorem G **M is B-form (supp c ⊆ D_F) or A2 family (triangle ⊆ D_F)**. The transposed statement uses D′_F and columns. + P-compatible frames: E8 2025/2025, P112 1260/1260, P104 135/759 (CHECKED, pcompat.py). +- **Theorem A, PROVEN (§4).** Let Σ_a = {u : ρ_a(O_u) = 7} and Σ_b = {u : ρ_b(O_u) = 7}. **If Σ_a or Σ_b contains an orthogonal pair, M is B-form or A2.** + This covers all of E8 and all of P112: every orthogonal pair lies in a P-compatible frame (CHECKED: 3780/3780 and 3304/3304). For P104 it covers 1404 of 2860 pairs. +- **Lemma 0, PROVEN (§1).** B\* ⟺ some rigid sub-unit L′ (with S1′) has rank M[L′,L′] ≤ 8 (Sylvester). +- **OPEN, the sticking point: Case B.** Here Σ_a and Σ_b are both pairwise non-orthogonal, i.e. cliques of size ≤ 8 (CHECKED: clique number 8). The A2 family and the clique-type B-form (8,8) live here. + With the transposed Theorem P available, the residue is exactly + **(K′): if F is a P-compatible frame avoiding Σ_b and D′_F fails Theorem P's condition, then D_F satisfies it.** + Frames avoiding a clique exist: at least 945 in E8 and at least 384 of the 896 H-compatible frames of P112 (CHECKED). So (K′) ⇒ B\* for E8 and P112. + NUMERICAL: on all 21 converged samples, every frame avoiding Σ_b has D_F ⊆ Σ_b (hence good in Case B), and D_F is bad iff F meets Σ_b. + **Why it is still open:** the tetrad-level constraints are Schur (x|_T ≠ 0 ⇒ y|_{T^c} = 0), ∩𝒯y = ∅ (F avoids Σ_b), and both sides bad. + These admit 3 227 764 (𝒯x, 𝒯y) configurations (kprime.py), so the Schur rule alone is far too weak. + A proof needs the ε-class-level propagation of the local K³ lemma (§5) from the bad pair {1,2} to the pairs {3,4}, {5,6}, and from there to the tetrads through one endpoint. Not done. +- **P104:** Theorem P and Theorem A apply only through its 135 P-compatible frames (1404 of 2860 orthogonal pairs). Lemma E's H-set route fails for most small deviation sets (§6, §7). +- **No new family found.** All converged samples are B-form with the predicted frame-class structure. A targeted construction against a surviving (K′) configuration is the way to look for a third family (not started). + +## §1 Lemma 0 (Sylvester reformulation): PROVEN +For S ⊆ L: rank M[S,S] = rank(A_S B_Sᵀ) ≥ ρ_a(S) + ρ_b(S) − 9. So rank M[S,S] ≤ 8 ⇒ ρ_a(S) ≤ 8 or ρ_b(S) ≤ 8. +Hence, if a rigid sub-unit L′ (Theorem U applies, and r(L′ ∩ O_s) spans r_s^⊥ for all s ∈ L) has rank M[L′,L′] ≤ 8, then rows L′ or +columns L′ span ≤ 8 dimensions. Lemma E (rows or columns) and Theorem G then give B-form or A2. The converse is trivial. +So **B\* fails only if every rigid sub-unit L′ ⊆ L has rank M[L′,L′] = 9.** + +## §2 Frame calculus: PROVEN +**Pivot coordinates.** A frame F ⊆ L gives a basis: a_f = e_f, b_f = e_f (after rescaling column f), plus e₉. Then a_u = (α_u, x_u) and +b_s = (β_s, y_s), where supp α_u = T(u) is exactly the F-tetrad of u (α_u(f) = M_uf). Likewise supp β_s = T(s). +For u ⊥ s: α_u·β_s + x_u y_s = 0. M − M[:,F]M[F,F]⁻¹M[F,:] = x yᵀ, with x = x_F, y = y_F (HELPER §1). +D_F = supp x, D′_F = supp y, Z_F = L ∖ D_F ⊇ F. D_F depends only on the hyperplane H_F = span a(F). Frames F′ ⊆ Z_F have H_{F′} = H_F. +**Schur rule.** For complementary F-tetrads T, T^c: x|_T ≠ 0 ⇒ y|_{T^c} = 0. Equivalently, Lemma 1₉: ρ_a(Δ_T) + ρ_b(Δ_{T^c}) ≤ 9. +**(Σ0)** ρ_a(O_u), ρ_b(O_u) ∈ {7, 8}. The upper bound is ρ_a(O_u) + ρ_b({u}) ≤ 9. The lower bound holds because O_u contains 7 orthogonal lines. +**(Σ1)** For f ∈ F: **f ∈ Σ_a ⟺ D_F ⊆ Nbar(f)**. This holds because a(O_f) ⊆ {v_f = 0}, and it spans that hyperplane iff x ≢ 0 on O_f. + If u ∈ Σ_a, every frame through u has the same hyperplane H_u = span a(O_u) ⊕ ⟨a_u⟩: span a(F∖u) is 7-dimensional and lies in the 7-dimensional span a(O_u). + Its deviation set lies in Nbar(u). +**(Σ2)** If u, w ∈ Σ_a with u ⊥ w lie in a common frame F, then H_u = H_w = H_F and D_F ⊆ Nbar(u) ∩ Nbar(w). + That is the set of lines of the three F-tetrads through the pair {u,w}. Three orthogonal lines of Σ_a in F confine D_F to one tetrad, since each triple lies in exactly one tetrad. + Five orthogonal lines are impossible, since they would give D_F = ∅ and rank 8. +**(Σ3)** For v ∈ D_F: on O_v, y_s = −α_v·β_s / x_v, so b(O_v) is the injective linear image of β(O_v) and ρ_b(O_v) = rank β(O_v). + So v ∈ Σ_b iff β(O_v) lies in a hyperplane of K⁸. +**(Σ4)** For any frame hyperplane H, every line s with O_s ∩ D_H = ∅ is in Σ_a. Proof: a(O_s) ⊆ H ∩ b_s^⊥, which is 7-dimensional, because H = b_s^⊥ would put a frame inside O_s. + +## §3 Theorem P (pinning): PROVEN +**P-compatible frames.** Call F ⊆ L *P-compatible* if every ε-class (4 lines) at every pair of every F-tetrad has ≥ 1 line in L, and every pattern (ε_ab, ε_bc) (2 lines) of every triple of every F-tetrad has ≥ 1 line in L. +H-compatible ⇒ P-compatible. CHECKED (pcompat.py): E8 2025/2025 frames, P112 1260/1260, P104 135/759. These are the only uses of L's missing lines in the proof. +**Statement.** Let F ⊆ L be a P-compatible frame, with Z = Z_F and D = D_F. For a pair {a,b} and sign ε, call {a,b} *ε-pinned* if at least two of the +three tetrads through {a,b} have an ε-class meeting Z. Let 𝒰 be the set of pairs that are not both +pinned and −pinned. If 𝒰 is a matching +(possibly empty), then M[Z, :] = D₁G[Z,:]D₂ with D₂ invertible. By CONJB Theorem G with X = D, M is then **B-form (supp c ⊆ D) or A2 family (triangle ⊆ D)**. +The transposed statement holds with D′_F and columns. +**Proof.** Use pivot coordinates. For u with {a,b} ⊆ T(u) put φ(u) = [α_u(a) : α_u(b)], and for columns ψ(s) = [β_s(a) : β_s(b)]. Both are points of P¹ ∖ {0, ∞}, because the supports are exact. +(i) *Pair pinning.* Let u ∈ Z lie in the ε-class of T_i, and let s be a column of T_j, j ≠ i, with T_i ∩ T_j = {a,b}. Then M_us = α_u(a)β_s(a) + α_u(b)β_s(b), since x_u = 0. + Also u ⊥ s ⟺ ε_ab(s) ≠ ε (UNIQ8 §1). So ψ(s) = φ(u)^⊥ for every (−ε)-column s outside T_i. + Let u_i, u_k be such rows in two different tetrads. A (−ε)-column of the third tetrad exists: the class has 4 lines in E8, and P-compatibility (below) leaves at least 1 in L. + That column forces φ(u_i) = φ(u_k) =: Π_ab(ε), and every (−ε)-column s at {a,b} has ψ(s) = Π_ab(ε)^⊥. + Π_ab(+) ≠ Π_ab(−): otherwise a +column s of T_j would satisfy M_{u s} = 0 for a +row u ∈ Z of some T_i (i ≠ j), but u, s are not orthogonal. + So for a pinned pair, ρ_ab(ε) := β_s(b)/β_s(a) depends only on ε = ε_ab(s), and ρ_ab(+) ≠ ρ_ab(−). +(ii) *Triangles.* Take {a,b,c} ⊆ T with all three pairs pinned. The columns of T realise all four patterns (ε_ab, ε_bc), each by 2 lines, and at least one survives H-compatibility. + ε_ac = ε_abε_bc, and β(c)/β(a) = (β(b)/β(a))(β(c)/β(b)). Write A = ρ_ab(+), A′ = ρ_ab(−), and so on. This gives C = AB = A′B′ and C′ = AB′ = A′B. + So B² = B′², and since char ≠ 2 and B ≠ B′, B′ = −B. Likewise A′ = −A and C′ = −C. Also ρ_ac(+) = ρ_ab(+)ρ_bc(+). +(iii) *Gauge.* 𝒰 is a matching. So every pinned pair {a,b} lies in a triple whose three pairs are pinned: choose c avoiding the at most two partners of a and b in 𝒰. + Fix a vertex a₀ and define μ_{a₀} = 1. For b with {a₀,b} pinned put μ_b = ρ_{a₀b}(+). Because 𝒰 is a matching, b₀ is the only vertex with {a₀,b₀} ∈ 𝒰 (if any). Put μ_{b₀} = ρ_{a₀c}(+)ρ_{cb₀}(+), where c is not a₀, b₀ or a partner in 𝒰. Then {a₀,c}, {c,b₀} and every triangle {a₀,c,b}, {c,b₀,b} used below are all-pinned. + The triangle relation (ii) makes ρ_ab(+) = μ_b/μ_a on every pinned pair. Two applications of (ii) through a third index show this for pairs not containing a₀. The definition of μ_{b₀} is independent of c by the same relation. + Every tetrad T meets 𝒰 in at most 2 disjoint pairs, so its pinned graph is connected. Hence for every column s: β_s(i) = κ_s σ^s_i μ_i (i ∈ T(s)), κ_s ≠ 0, i.e. **β_s ∝ D_μ r_s**. + This includes the pairs in 𝒰, via a path of pinned pairs inside T(s). Frame columns are e_f = Gram. +(iv) *Rows.* For u ∈ Z, α_u·β_s = M_us = 0 on O_u ∩ L. Here β(O_u ∩ L) = D_μ r(O_u ∩ L) spans D_μ(r_u^⊥), by (S1) for L (CONJB spans.py). + So α_u ∝ D_μ⁻¹ r_u, and M_us = λ_u κ_s G_us on Z × L. The vectors r(Z) ⊇ r(F) span K⁸. Theorem G applies with X = D. ∎ +**Remarks.** (1) Only the rows in Z and the column vectors β are used. y and D′ never enter. (2) In the A2 family with F avoiding X, and in B-form with F avoiding supp c, we get D = X or supp c, |D| ≤ 13, and the condition holds. +(3) The failure mode is the **star**: F ∋ t, where t carries the deviation. Then D_F ⊇ every line of the seven tetrads through t's coordinate, every pair {i, t} is unpinned, and the coordinate β(t) is twisted. + NUMERICAL: these are exactly the |D_F| = 52 frames in all samples. + +## §4 Theorem A (an orthogonal pair in Σ): PROVEN +Let f₁ ⊥ f₂ in Σ_a, lying in a P-compatible frame F ⊆ L. By (Σ2), D_F ⊆ the lines of T₁ ∪ T₂ ∪ T₃, the three F-tetrads through {1,2}. +An unpinned pair {a,b} needs two tetrads through {a,b} whose ε-class (nonempty in L, by P-compatibility) lies inside D. Only T₁, T₂, T₃ qualify, +and two of them meet exactly in {1,2}. So 𝒰 ⊆ {{1,2}}, which is a matching, and Theorem P gives B-form or A2. Transpose for Σ_b. ∎ +CHECKED (hset3.py, hcompat.py): in E8 all 3780 orthogonal pairs lie in frames, and all 2025 frames are H-compatible. In P112, 896 of the 1260 frames are H-compatible, +and they cover 3136 of the 3304 orthogonal pairs. Superseded by pcompat.py: every P112 frame is P-compatible, and all 3304 orthogonal pairs are covered. P104: 1404 of 2860 pairs are covered. +NUMERICAL: the (1,52), (52,1), (13,4), (5,11) and (6,9) samples have orthogonal pairs in Σ_a or Σ_b, so they fall under Theorem A. +The clique type (8,8), the (7,7) sample and the A2 family have both Σ's pairwise non-orthogonal (Case B). + +## §5 Case B: what is missing (OPEN), and the evidence +Case B: Σ_a and Σ_b each have no orthogonal pair. Then |Σ_a|, |Σ_b| ≤ 8 (CHECKED: the clique number of the non-orthogonality graph is 8 for E8, P112 and P104). +Some H-compatible frame avoids Σ_b. Each frame meets a clique in ≤ 1 line, so in E8 at most 8·135 = 1080 of the 2025 frames meet it, and in P112 at most 512 of the 896 (CHECKED, cliqueavoid.py). +**Lemma (K), OPEN:** if F avoids Σ_b, then 𝒰_F is a matching. NUMERICAL, stronger: D_F ⊆ Σ_b. +In Case B that rules out any ε-class in D, because an ε-class contains orthogonal pairs, so it gives 𝒰_F = ∅. +(K) ⇒ B\* for E8 and P112. The weaker (K′) of §0 suffices. +Evidence (lemK.py, bad.py, bad2.py; NUMERICAL on the 21 converged samples, all B-form; and orientA2.py, exact A2 instance converted to float): +- Every frame avoiding Σ_b has D_F ⊆ Σ_b, and all such frames lie in one hyperplane class. The dual statement for Σ_a holds too (21/21). +- D_F fails Theorem P's condition iff F ∩ Σ_b ≠ ∅, on every sample tested (5 types). +- B-form: Σ_b = supp c and Σ_a = supp β exactly. A2: Σ_a = Σ_b = X. Frames through X give |D_F| = 52 (stars), and the other frames give D_F = X. +**Where the proof attempt stops.** Schur's rule only controls y on complementary tetrads. A bad pair {1,2} puts x ≠ 0 on two ε-classes (in T₁ = 1234 and T₂ = 1256). +That forces y = 0 on the lines of 5678 and 3478, but y = 0 is needed on all of O_{f₁} (or all of O_{f₂}), which also contains 3456 and four tetrads through 2. +In the pair configuration {1,2}, the vectors (φ, x) and (ψ, y) live in K³, and the local lemma below gives only "row excess at (i, ε) ⇒ column ψ̂ constant on the (−ε)-classes j ≠ i". +The missing ingredient is propagation of that constancy to the pairs {3,4} and {5,6}, and from there to the tetrads through one endpoint. +**Local lemma (pair configuration), PROVEN.** Let U_i = span{(φ_u, x_u) : u in the ε-class of T_i} ⊆ K³ and V_j = span{(ψ_s, y_s) : s in the (−ε)-class of T_j}. +Then U_i ⊥ V_j for i ≠ j. dim U_i = 2 ⇒ V_j = V_k is a single line ⟨v⟩ with U_i = v^⊥. x ≡ 0 on the class ⇒ dim U_i = 1, since otherwise V_j = ⟨e₃⟩ contradicts ψ ≠ 0. + +## §6 P104 (OPEN) +No frame of P104 is H-compatible. Every frame F ⊆ P104 has some F-tetrad missing ≥ 2 lines of E8 ∖ L. +Theorem P's steps need: (i) a (−ε)-column in the third tetrad, (ii) all four sign patterns per triple among columns, and (iii) S1 for L (true). +Steps (i)/(ii) can fail where 2 lines of the same pattern are missing. A P104 version must either choose F so that the missing pairs never hit a needed pattern, or use #1399's P104 rigidity. Not attempted. + +## §7 CHECKED finite facts (exact integer arithmetic on E8 roots; scripts here) +- hset.py / hset2.py: E8 and P112 minus any single line or any A2 triangle contain an H-set. P104: 32 of 104 lines and 480 of 704 triangles fail. +- hset3.py: E8 minus the 8 lines of any frame-tetrad contains an H-set (9450/9450). P112: 6300 of 7308 do. P104: 28 of 5550 do. +- hset4.py: L minus Nbar(u) ∩ Nbar(w) for u ⊥ w (the (Σ2) set): never contains an H-set. That is why Theorem A goes through Theorem P rather than Lemma E. +- s1p.py: S1′ holds for L′ = L ∖ D for every D tested: single lines, A2 triangles, tetrad line-sets (E8 10690 sets, P112 8316, P104 6358; min rank 7). +- hcompat.py, cliqueavoid.py: H-compatible frame counts, orthogonal-pair coverage, clique number 8, frames avoiding a clique. +NUMERICAL only: orient.py, orient2.py, orientA2.py, lemK.py, bad.py, bad2.py. + +## §8 Files +blib.py (E8 lines, units, frames, tetrads w.r.t. any frame), hset*.py, s1p.py, hcompat.py, cliqueavoid.py (CHECKED); +orient*.py, lemK.py, bad*.py (NUMERICAL orientation on MASK-RANK9 / CONJB samples and the exact A2 instance). + +## §9 Follow-up on (K′) (coordinator round 2; E8 focus) +- **Sharpened residue, PROVEN reduction.** Theorem P already handles the case where the unpinned-pair set 𝒰_F is a matching. So (K′) is equivalent to + **(K″): in Case B, if a P-compatible frame F avoids Σ_b, then 𝒰_F has maximum degree ≤ 1.** + The obstruction is a vertex a with two unpinned pairs {a,b}, {a,c}. This is the "star" mechanism of §3 Remark (3): column coordinate a can twist freely. +- **The Case B hypothesis is essential (infinitesimal, NUMERICAL, inf.py).** Take c generic on E₁ ∪ E₂ (two full +classes at {1,2}). Then F avoids Σ_b, D_F is bad, + and the first-order solution space has exactly the B-form dimension 14. So these deformations are B-form with f₁, f₂ ∈ Σ_a (Case A). A proof of (K″) must use "Σ_a has no orthogonal pair". +- **Targeted construction: no third family at first order with small row support (NUMERICAL, inf3.py).** + Setup: first-order rank-9 deformations of the E8 Gram matrix, a_u = (r_u + εV_u, √ε c_u), b_s = (r_s + εU_s, √ε β_s). + The condition c_uβ_s + r_u·U_s + V_u·r_s = 0 on orthogonal pairs is linear in (β, U, V) for fixed c. + For every W(E8) orbit type of support S with |S| ≤ 4 (21 types) and both random and all-ones c on S, dim{β} equals the B-form prediction + dim(col R + ⟨e_t : t ∈ comNbar(S)⟩). The only exception is the A2 triangle, which has 1 extra dimension (12 vs 11): the A2 family, as expected. + Larger supports tested (8-line tetrad, E₁+E₂, E₁+E₂+E₃, two tetrads): B-form dimension exactly. + Caveat: c is only defined modulo col R. A third family whose row deviation has no small-support representative is not excluded by this scan. +- **Proof attempt, where it stops.** Bad at {1,2} gives y = 0 on 5678 and 3478 (Schur). The Z′-columns there pin all rows at pairs {3,4}, {5,6} and {7,8} (transposed pinning, PROVEN). + The step still missing is to show that a second bad pair through 1 (or 2) forces y ≡ 0 on O_{f₁} (or O_{f₂}), i.e. f₁ ∈ Σ_b, using the clique property of Σ_a. diff --git a/research/e8-rank9-realisations/evidence/CONJB_THEORY_snapshot.md b/research/e8-rank9-realisations/evidence/CONJB_THEORY_snapshot.md new file mode 100644 index 0000000000..1a6ba4e16f --- /dev/null +++ b/research/e8-rank9-realisations/evidence/CONJB_THEORY_snapshot.md @@ -0,0 +1,140 @@ +# CONJB: rank-9 realisations of the P112 / P104 / E8 orthogonality pattern + +Labels: **PROVEN** (written proof here) · **CHECKED** (exact script in this folder) · **NUMERICAL** (floating point, evidence only) · **OPEN**. +python = W/venv/bin/python; run scripts from this folder. Setting: MASK-RANK9 §0/§4 (Conjecture B), UNIQ8 Theorem U (= special case of #1212). +"Pattern" = the full iff pattern: M_tt ≠ 0, and for t ≠ s, M_ts = 0 ⟺ t ⊥ s. G = Gram matrix of the chosen root representatives r_t. +O_u = lines of L orthogonal to u; Nbar[u] = lines not orthogonal to u (u included). + +## §0 Status (CONJB, Oct 15) +- **Conjecture B is FALSE as stated (CHECKED, exact).** On P112, P104 and E8 there are rank-9 pattern realisations that are not + D₁·G·D₂ + c βᵀ for any diagonal D₁, D₂ (singular allowed) and any rank-one c βᵀ with no orthogonal pair in supp c × supp β (generic parameters; for special parameters an A2-family member can be B-form, Theorem G(b)). The "no orthogonal-pair condition" variant is supported by the audit's restricted-D numerical test only, not certified. + They form the **A2 family** (§1): Gram everywhere except the three rows of one A2 triangle {u₁,u₂,u₃}, and row u_i is the Gram row + rescaled by one factor on Nbar(u_i) ∩ O_{u_j} and by a different factor on Nbar(u_i) ∩ O_{u_k}. Exact certificate: a2cert.py (§1.3). + NUMERICAL (not proven): at these points the tangent space of the realisation variety has dimension 310 = 81 (GL9) + 229 (family dimension, + a2dim.py), with singular-value gap 1e0 against 1e-14 (a2tang.py). So numerically the A2 family is locally a whole component, not a degenerate + limit of B. The random-start searches of MASK-RANK9 did not reach it. +- **Theorem G (one-sided classification), PROVEN (§2), using CHECKED span facts (spans.py).** If the rows outside some set X are + Gram rows (M[L∖X, :] = D₁G[L∖X, :]D₂ with D₂ invertible and r(L∖X) spanning K⁸), then M is of B-form with supp c ⊆ X and no + orthogonal pair in supp c × supp β, **or** M is in the A2 family on an A2 triangle inside X. The transposed statement holds for columns. + The A2 triangle is the only obstruction. It arises because the only line sets spanning a 2-plane are A1, A1×A1 and A2. +- **Lemma E (extension), PROVEN (§3).** "Rows off X are Gram rows" follows from rank M[L∖X, :] ≤ 8 when L∖X contains a sub-unit + L′ on which rank-8 rigidity is known (#1212 / UNIQ8 Thm U and the swarm's extensions #1389 #1399 #1419 #1425 #1469 #1474 #1616 #1650), + provided r(L′ ∩ O_s) spans r_s^⊥ for every s ∈ L. This is a finite check per (L, L′). +- **Corrected conjecture B\* (OPEN).** Every rank-9 pattern realisation on P112 / P104 / E8 has a row set or a column set of corank ≤ 8 + whose complement contains a rank-8-rigid sub-unit. Equivalently, by Theorem G + Lemma E, every such realisation is B-form or A2 family + (rows or columns). The gap is the existence step: find X with rank M[L∖X, :] = 8. The "shared extra direction" of the tetrad spans + (MASK-RANK9 §4) is one route to it. Evidence: §4. I do not have a proof of the existence step. +- **What this means downstream (MASK9 case (c)).** The decoder analysis of rank-9 realisations must also cover the A2 family, which has + no rank-one biclique term. Its deviation from Gram has rank 2 (§1.2), supported on 3 rows. Case A/C of MASK-RANK9 §1–§2 do not apply + as written. Decoder costs on this family were not computed here. +- **Prior art.** No swarm PR classifies rank ≥ 9 realisations (searched Oct 15: "rank 9", "rank nine", "rank-nine realisation", + "masked correction rank nine", "A2 triangle", "piecewise"). #1212 states rank ≥ 9 as open. #2277 excludes "realisations of rank above T". + #2021 is a different object (two-column rank-two corrections). #1212's frame-pivot method is rank-8 specific (K = ¼K[:,F]K[F,:]). + At rank 9 it gives K = K[:,F]K[F,F]⁻¹K[F,:] + x yᵀ (§5), which is where any proof of B\* would have to start. + +## §1 The A2 family +### §1.1 Two facts about A2 in E8 (PROVEN) +(a) The lines of E8 in a 2-dimensional plane form a simply-laced rank ≤ 2 root system: A1, A1×A1 or A2. So there are at most 3, + and exactly 3 only for an A2 triangle (pairwise non-orthogonal). +(b) Let r₁, r₂ be roots with r₁·r₂ = 1 and r₃ = r₁ − r₂. Every root r ∉ {±r₁, ±r₂, ±r₃} is orthogonal to at least one of r₁, r₂, r₃. + *Proof.* r·r₃ = r·r₁ − r·r₂. If r·r₁, r·r₂ ∈ {±1}, then r·r₃ ∈ {0, ±2}, and r·r₃ = ±2 forces r = ±r₃. ∎ + So L ∖ X = ∪_i (O_{u_i}), and the three sets O_{u_i} ∩ O_{u_j} all equal the E6 of lines orthogonal to the triangle. + +### §1.2 Construction (PROVEN, and CHECKED on instances) +Let X = {u₁,u₂,u₃} be an A2 triangle in L. Take g₁ = 0 and g₂, g₃ ∈ span(r₁, r₂). For s ∈ O_{u_i}, set z_s = −g_i·r_s. This is +consistent on overlaps, because O_{u_i} ∩ O_{u_j} ⊥ span(r₁, r₂) ∋ g_i − g_j. Choose z on X freely. Put a_u = (r_u, 0) and +b_s = (r_s, z_s) for u ∉ X, and a_{u_i} = (r_i + g_i, 1). Then M = ABᵀ has rank ≤ 9, and M equals G off rows X. On s ∈ O_{u_i}, +M_{u_i s} = r_i·r_s + g_i·r_s + z_s = 0. On s ∈ Nbar(u_i) ∩ O_{u_j}, M_{u_i s} = (r_i + g_i − g_j)·r_s. +Here g_i − g_j ∈ span(r₁, r₂), and r_s ⊥ r_j, so this is κ_{ij}·G_{u_i s} with a scalar κ_{ij}. That is the piecewise rescaling. +M − G = (rows X) has rank 2 modulo the Gram row space. Proof: with p, q, r the restrictions of Gram rows to the three parts, +G_{u₁} ≡ p+q, G_{u₂} ≡ r+q, G_{u₃} ≡ p−r, so every piecewise rescaling lies in the Gram span plus one vector. This is why +6 scale factors survive at rank 9. General D₁, D₂ are added by diagonal scaling. +a2fam.py builds exact rational instances. For P112, P104 and E8 it checks, for 3 random parameter choices per unit, that the zeros of M +are exactly the orthogonal pairs and that rank M = 9. + +### §1.3 Not of B-form: exact certificate (CHECKED, a2cert.py; argument PROVEN) +Suppose rank M = 9 and M = D₁GD₂ + c βᵀ with c_uβ_s = 0 on orthogonal pairs. Write M = ABᵀ with rows a_u, b_s ∈ K⁹. +Then col M = col(D₁R) ⊕ ⟨c⟩, so c = Aπ and β = Bν for some π, ν. For u ∈ supp c, β vanishes on O_u, so ν lies in +N_u := b(O_u)^⊥. Let Σ := {u : dim N_u ≥ 2}. There are two cases. +- **Some u ∈ supp c has dim N_u = 1.** Then ν ∝ a_u, so β ∝ M[u, :], which has support Nbar[u]. supp c must avoid every line + orthogonal to some line of Nbar[u]. CHECKED: for every line of P112, P104 and E8 that leaves only u. So c = c_u e_u, and the + rows L∖{u} of M are rows of D₁GD₂, which has rank ≤ 8. CHECKED: every 111-row (103-, 119-row) submatrix has rank 9. Contradiction. +- **supp c ⊆ Σ.** Then the rows off Σ lie in π^⊥. CHECKED: they span exactly 8 dimensions, so π is unique up to scale, and + supp(Aπ) = X. Then ν annihilates b(∪_{u∈X} O_u). CHECKED: rank 9, so ν = 0, so β = 0. Contradiction. +Ranks are computed mod p = 2⁶¹−1. Those are lower bounds for the rational ranks, and every inference above uses only lower bounds, or +upper bounds that hold by construction. The pattern check is exact over Q. Output: P112 Σ = X = {0,4,25}; P104 {0,3,22}; E8 {0,2,15}. + +## §2 Theorem G (one-sided classification): PROVEN +**Span facts (CHECKED, spans.py, exact).** For L ∈ {P112, P104, E8}: (S1) r(O_u) spans r_u^⊥ for every u. +(S2) r(O_u ∩ O_{u′}) spans ⟨r_u, r_{u′}⟩^⊥ for every u ≠ u′. + +**Theorem G.** Let L ∈ {P112, P104, E8}, and let M be a rank-9 pattern realisation on L over a field K with char K ≠ 2. Let X ⊆ L +be such that M[w, :] = d₁_w (G D₂)[w, :] for all w ∉ X, with D₂ invertible, d₁_w ≠ 0, and r(L∖X) spanning K⁸. Then one of the following holds: +(a) M = D₁′ G D₂ + x z′ᵀ with supp x ⊆ X and x_u z′_s = 0 whenever u ⊥ s (B-form, D₁′ = D₁ off X); +(b) X′ := {u ∈ X : M[u, :] ∉ rowspace(G D₂)} is an A2 triangle, and M is in the A2 family of §1.2 (with D₁, D₂ and scalars x_i on the three rows). M can also be B-form + here, but only for special parameters. +*Proof.* rowspace(G D₂) = rowspace(Rᵀ D₂) has dimension 8 and is spanned by the rows off X. Since rank M = 9, rowspace M = rowspace(RᵀD₂) ⊕ ⟨z⟩. +Write M[u, :] = w_uᵀRᵀD₂ + x_u z for u ∈ X; this is unique, since Rᵀ has full row rank. The zeros of row u give d₂_s(w_u·r_s) + x_u z_s = 0 for s ∈ O_u. +If x_u = 0, then w_u ⊥ r(O_u), so w_u ∝ r_u by (S1), and row u is a Gram row. X′ is nonempty because rank M = 9. +For u ∈ X′ put g_u = w_u / x_u. Then z_s = −d₂_s g_u·r_s on O_u. For u, u′ ∈ X′ this gives (g_u − g_{u′})·r_s = 0 on O_u ∩ O_{u′}, +so **g_u − g_{u′} ∈ ⟨r_u, r_{u′}⟩** by (S2). +*Cocycle lemma.* If |X′| ≤ 2, or r(X′) spans at least 3 dimensions, there is a g with g − g_u ∈ ⟨r_u⟩ for all u ∈ X′. +For |X′| = 1 take g = g_u. Otherwise fix u₁ ≠ u₂. Write g₁ − g₂ = μr₁ + νr₂, which is unique since r₁, r₂ are independent. +Then g := g₁ − μr₁ = g₂ + νr₂ is the unique vector that works for u₁ and u₂. Take u₃ with r₃ ∉ ⟨r₁, r₂⟩. +Then g − g₃ ∈ (g₁ − g₃ + ⟨r₁⟩) ∩ (g₂ − g₃ + ⟨r₂⟩) ⊆ ⟨r₁, r₃⟩ ∩ ⟨r₂, r₃⟩ = ⟨r₃⟩. +Now take u₃ with r₃ ∈ ⟨r₁, r₂⟩. By hypothesis some u₄ ∈ X′ has r₄ ∉ ⟨r₁, r₂⟩, and g works for u₄ by the previous step. +The pair (u₁, u₄) determines g uniquely in the same way, and r₃ ∉ ⟨r₁, r₄⟩, because ⟨r₁, r₂⟩ ∩ ⟨r₁, r₄⟩ = ⟨r₁⟩ and r₃ ∦ r₁. +Applying the previous step to the pair (u₁, u₄) gives g − g₃ ∈ ⟨r₃⟩. +Given such a g, put z′ = z + gᵀRᵀD₂. Then z′ vanishes on every O_u with u ∈ X′, and M[u, :] = x_u(g_u − g)ᵀRᵀD₂ + x_u z′. +Here x_u(g_u − g) = d₁′_u r_u, so this is (a). The condition x_u z′_s = 0 on orthogonal pairs is automatic. +Otherwise |X′| ≥ 3 and r(X′) spans a 2-plane, so X′ is an A2 triangle by §1.1(a). Rows off X′ are Gram rows, and rows u ∈ X′ have exactly +the form a_u = (d₁_u r_u + x_u g_u, x_u), b_s = (d₂_s r_s, z_s) of §1.2. Normalise g₁ = 0 by replacing z with z + g₁ᵀRᵀD₂. This is (b). ∎ +**Remark (fields).** The proof uses no characteristic assumption beyond (S1)/(S2). Those are rank statements about integer matrices, +CHECKED mod 2⁶¹−1, hence true over Q and so over every field of characteristic 0. For a field of characteristic p, re-run spans.py mod p. + +## §3 Lemma E (rank 8 on a row set ⇒ Gram rows): PROVEN +Let rank M[L∖X, :] ≤ 8, and let L′ ⊆ L∖X be such that M[L′, L′] = D₁GD₂ on L′ (for example, L′ a unit where rank-8 rigidity is proven) +and r(L′) spans K⁸. Assume (S1) for L, and (S1′): r(L′ ∩ O_s) spans r_s^⊥ for every s ∈ L. Then M[L∖X, :] = D₁G[L∖X, :]D₂ with D₂ invertible. +*Proof.* Factor M[L∖X, :] = A′B′ᵀ in K⁸. a(L′) spans K⁸ (M[L′, L′] has rank 8), so we may take a_u = d₁_u r_u on L′. +Each column s satisfies b_s ⊥ r(L′ ∩ O_s), so b_s = d₂_s r_s by (S1′). d₂_s ≠ 0 because some u ∈ L′ is non-orthogonal to s and M_us ≠ 0. +Each row u ∉ X satisfies a_u ⊥ b(O_u) = r(O_u) (rescaled), so a_u ∝ r_u by (S1), and the factor is nonzero since M_uu ≠ 0. ∎ +Applying Theorem G then needs only the existence of X (Conjecture B\*, §0). + +## §4 Evidence and checks +- **Census (NUMERICAL, census.py) on MASK-RANK9's 15 converged realisations (all B-form).** + Σ := {u : dim span b(O_u) = 7} equals supp c exactly: the clique type has 8, and the other types have 5, 6, 13 and 1. + The rows off Σ span 8 dimensions, and in every case with |Σ| ≥ 2 the N_u (u ∈ Σ) meet in exactly ⟨ν⟩. + (sol_rand_7 / 24 and sol_sparse_1 / 6 are unconverged, with orthogonal residual up to 2e-3, and are excluded.) + In the A2 family Σ = X, but the N_u meet in 0. That is the certificate of §1.3. +- **Theorem G hypotheses on the B samples.** MASK-RANK9/ana6.py found the rows off supp c in Gram form on all 15. +- **New random-start search (NUMERICAL, search.py seed 7, 40 starts, jobs/conjb_search.log).** 6 starts reached rank 9, and all 6 are + B-form by the classifier, which finds a side with rank b(∪O_u) ≤ 8. Their (|supp c|, |supp β|) are (7,7), (1,53) ×2, (8,8) ×2, (5,10). + The other 34 starts collapsed to rank 8. Random starts do not reach the A2 component. Saved as sol_7_*.npy. +- **Sonnet helper (HELPER.md; excess.py, pivot.py, switch.py).** On the 15 B samples, the 5-dim tetrad spans share one direction + (NUMERICAL). It also has a frame-switch lemma (hand proof, M_ee ≠ 0). The frame-pivot Schur complement is rank one on all 1260 frames. + These are tools for the existence step of B\*. They do not bear on the A2 counterexample, where the shared direction exists but ν does not. +- **Audit (Sonnet, independent, read-only).** PASS on §1.1, §1.2 (re-ran a2cert.py on P112 and E8, and spans.py), §1.3, §2 (cocycle + lemma) and §3. It also ran an independent numpy check on E8: with D free on X, M − D₁GD₂ has σ₂ ≈ 40 (no rank-one fit). + Three §0 wording fixes were applied: generic parameters only, the "without the orthogonal-pair condition" claim dropped, and the + NUMERICAL tag kept. One Lemma E step is now spelled out: the basis change is well defined because r(L′) spans and the form is nondegenerate. + +## §5 What a proof of B\* has to do (OPEN, scoped) +- Pivot on a frame F ⊆ L (#1212's method): M = M[:, F]M[F, F]⁻¹M[F, :] + x yᵀ with x_F = y_F = 0. For F-complementary blocks T, T^c, + x|_T = 0 or y|_{T^c} = 0, from zeros alone. The two-term equations become α_u(a)β_s(a) + α_u(b)β_s(b) = −x_u y_s. + B\* asks for a frame-independent hyperplane. In B-form it is π^⊥ = span a(L ∖ supp c), and in the A2 family it is the Gram row span. + The frame pivot gives the hyperplane U_F, which is the right one only when F avoids supp c (and when F avoids X for A2). +- The tetrad route (MASK-RANK9 §4, "all 5-dim U_T share one extra direction") is **false for the A2 family as a route to B**, but it can + still give the existence step. In the A2 family the extra direction is shared (the a-side hyperplane is the Gram span). What fails is + the second half: no ν with the support condition. +- **Non-iff patterns (STRAYS case (c), zeros allowed on non-orthogonal pairs).** + - Theorem G uses "non-orthogonal ⇒ nonzero" only through d₁_w ≠ 0, d₂ invertible, and M_uu ≠ 0. (S1)/(S2) are statements about roots, + so with extra zeros the theorem still holds whenever its hypothesis holds. + - Lemma E uses non-orthogonal entries only to get d₂_s ≠ 0 and a_u ≠ 0. With singular D (the K_λ case) it fails as stated. + - The §1.3 certificate uses the exact pattern (supp β = Nbar[u] in case 1). + - Theorem U itself needs the iff pattern. #1212 removes that need by a DRUP zero-exclusion, but only for its listed units and at rank 8. + - With M_tt = 0 allowed, nothing here transfers. + +## §6 Files +a2fam.py (exact A2 construction; UNIT=P112|P104|E8), a2cert.py (non-B certificate, exact pattern + mod-p ranks), a2tang.py and a2dim.py +(NUMERICAL tangent / family dimension 310 = 81 + 229), spans.py (S1/S2 CHECKED), census.py (NUMERICAL per-line census of the +MASK-RANK9 samples), modrank.py (GF(p) rank), search.py (NUMERICAL random-start search + classifier). diff --git a/research/e8-rank9-realisations/evidence/KSTAR_THEORY_snapshot.md b/research/e8-rank9-realisations/evidence/KSTAR_THEORY_snapshot.md new file mode 100644 index 0000000000..ce4bcb97f9 --- /dev/null +++ b/research/e8-rank9-realisations/evidence/KSTAR_THEORY_snapshot.md @@ -0,0 +1,133 @@ +# KSTAR: closing Case B of Conjecture B* (lemma (K″)) — E8 first, then P112 +Labels: **PROVEN** · **CHECKED** (exact script here) · **NUMERICAL** · **OPEN**. Setting and notation: BSTAR/THEORY.md (§2 pivot coordinates, §3 Theorem P, §5 local lemma). + +## STATE +- 16:45 KSTAR: started; read BSTAR/CONJB/UNIQ8/ZEROS. Plan: class-level propagation rules from the local K³ lemma + Schur + Σ facts, then a tiny certified kissat step for (K″) on E8. +- 17:20 KSTAR: class-level SAT abstraction (Schur + mixed-class homogeneity + Σ facts) is SAT even for the joint residue (full tetrads in D and D′) → value-level coupling needed. Pivoting to Σ_a ∩ Σ_b ≠ ∅ ⇒ reduces to a 56-line point/line incidence problem; certifying that by kissat. +- 17:50 KSTAR: Theorem S (Σ_a ∩ Σ_b ≠ ∅ ⇒ B/A2) CHECKED for E8 (56-line incidence problem, kissat UNSAT + independent RUP checker). Theorem Σ (Σ_a ≠ ∅ or Σ_b ≠ ∅ ⇒ B/A2) PROVEN from it + Theorem A + span facts (S2), (S3′) CHECKED. (K″) is no longer needed: B* on E8 reduces to excluding Σ_a = Σ_b = ∅. + +- 18:45 KSTAR: P112 checks done (112/112 UNSAT+RUP, spans 0 bad); Theorem Σ holds on P112. Advisor fixes applied (antipodes in cocycle, g_u projection). Residue Σ_a=Σ_b=∅ OPEN. Handing back. + +- 19:00 KSTAR: round 2 started (residue Σ_a = Σ_b = ∅). E7 recursion scoped and set aside (§4.1). Working on the extremal-frame + twist route; numerical residue probe running (job kstar_probe). +- 19:35 KSTAR: P¹-valued pinning SAT model (pin.py: equalities of pair ratios, ORTH/NON/TRI/K³/ZZ/Schur + residue + both sides non-Gram) is SAT (pin1.out: x on the 11 tetrads not through {1,2}, y on the 3 tetrads avoiding {1,2}). Corrected the round-1 joint-pinning 'only if'. Generic residue probe killed (too slow on efficiency cores); running a targeted numerical realisability test of pin1's support pattern (job kstar_cfg). +- 20:05 KSTAR: **residue killed (pending certificate).** P¹-valued pinning model + ratio rules (pin.py, §7) is UNSAT on E8 with residue + both sides non-Gram (kissat < 100 s); SAT without either hypothesis (sanity); 0 clause violations on true data of A2 and B-form instances over many frames incl. stars (soundtest.py). DRAT + rup.py certificate running (job kstar_cert). P112 frame 0 also UNSAT. +- 20:55 KSTAR: **Theorem R CERTIFIED on E8.** kissat 4.0.4 (--factor=false --preprocessfactor=false, so no extension variables) DRAT proof pin3.drat (163 MB) checked by rupc.c, an independent forward RUP checker that honours deletions and rejects RAT: "VERIFIED: top-level conflict after 2 382 724 lemmas (2 761 873 deletions)", 890 s. (The first proof used kissat's default factor/BVA with new variables, and rupc rejected it as "var out of range". Hence the flags.) rupc also re-verifies s56 and rejects a bogus empty-clause proof. **So B* holds on E8, PROVEN modulo two CHECKED finite steps (s56 incidence, pin3 UNSAT), each with an independent certificate.** P112: frames 0, 2, 26 (one per orbit of 2⁸:AGL(3,2)) are running in job kstar_cert2 (log jobs/kstar_cert2.log; frame 0 had already been UNSAT by plain kissat); soundtest rerun is queued in the same job. + +## §0 Status +- **Round 2: Theorem R (§7), the residue Σ_a = Σ_b = ∅ is empty on E8. Together with S and Σ this gives Conjecture B\* on E8: every rank-9 iff-realisation is B-form or A2.** + Reduction PROVEN; finite step = one kissat UNSAT on a sound Boolean model (pin.py), CERTIFIED by rupc (STATE 20:55). P112: Theorem R running on the 3 frame orbits (job kstar_cert2; frame 0 UNSAT, uncertified). +- **Theorem Σ (E8), PROVEN (§2), using Theorem S (CHECKED, §1), BSTAR Theorem A, CONJB Theorem G, spans (S2) and (S3′) (CHECKED).** + If Σ_a ≠ ∅ or Σ_b ≠ ∅, then M is B-form or in the A2 family. This covers Case B whenever either Σ is nonempty, with no use of (K″). +- **P112: Theorem Σ also holds (CHECKED, §3).** +- **Residue for B\* on E8 and P112: Σ_a = Σ_b = ∅** (every b(O_u) and every a(O_u) spans 8 dims). OPEN, see §4. +- Every known rank-9 realisation has Σ ≠ ∅ (B-form: Σ_a ⊇ supp β, Σ_b ⊇ supp c; A2: Σ_a = Σ_b = X). + +## §1 Theorem S: Σ_a ∩ Σ_b ≠ ∅ ⇒ B-form or A2 (E8). Reduction PROVEN, finite step CHECKED +Let f₁ ∈ Σ_a ∩ Σ_b and take any frame F ∋ f₁ (pivot coordinates, BSTAR §2). By (Σ1) on both sides, x ≡ 0 and y ≡ 0 on O_{f₁}. +(i) *Everything off index 1 is Gram-shaped.* For a pair p = {j,k} ⊆ {2..8} the three tetrads through p are T_a, T_b (avoiding 1) and T_c ∋ 1. +Rows of T_a, T_b are in Z and their columns in Z′, so every orthogonal pair (u,s) at p with u or s in T_a ∪ T_b has M̃_us = M_us = 0. +The row-column graph of BSTAR §3 (i) is connected, so all rows and all columns at p are pinned, Π_p(+) ≠ Π_p(−) (witness: a +row of T_a against a +column of T_b). +Triangles ⊆ {2..8} lie in one tetrad whose columns realise all 4 patterns, so BSTAR §3 (ii)–(iii) give a gauge μ on {2..8}. +Hence α_u|_{T(u)∖1} ∝ D_μ⁻¹σ^u and β_s|_{T(s)∖1} ∝ D_μσ^s for all u, s; lines avoiding 1 are Gram rows and columns. +(ii) *The 56-problem.* Choose representatives with σ₁ = +1 on the 56 lines of Nbar(f₁). Rescale e₁ freely. Write α_u(1) = κ_u p_u, x_u = κ_u x̂_u, P_u = (p_u, x̂_u), +and Q_s = (q_s, ŷ_s) for columns. For u, s ∈ Nbar(f₁): M_us = κ_uκ′_s (g_us − 1 + P_u·Q_s), g_us = Σ_{T(u)∩T(s)} σσ′ = 2 r_u·r_s. +All other entries are Gram (×κκ′) except row f₁ (M_{f₁s} = κ′_s q_s) and column f₁ (M_{uf₁} = κ_u p_u). So the only constraint left is +**P_u·Q_s = 1 whenever u ⊥ s (u, s ∈ Nbar(f₁))**. Projectively P̂_u = (P_u, 1) is a point and Q̂_s = (Q_s, −1) a line of P²(K), incident whenever u ⊥ s. +(iii) *Finite step (CHECKED, s56.py + rup.py; W(E8) is transitive on lines so one f₁ suffices; run for f₁ = lines 0–15, identical 4863-lemma proofs: jobs/kstar_s56_E8.log).* Encode equality of points (resp. lines) by Boolean variables with transitivity, +plus the incidence axiom "two distinct points have at most one common line" (and dually), applied to every pair of rows u, u′ and every pair of common Γ-neighbours. +Negate the conclusion: "no point class A₀ meets Γ(s) for every column s, and no line class B₀ meets Γ(u) for every row u" (Γ = orthogonality inside Nbar(f₁); +|Γ(u)| = 27, common neighbours 10 (u ⊥ u′), 16 (r_u·r_{u′} = 1), 0 (antipodes)). kissat: UNSAT; the DRAT proof (4863 lemmas) is re-verified by rup.py, +an independent 90-line RUP checker (tested to reject a bogus empty-clause proof and a satisfiable formula). The abstraction only keeps necessary conditions, so UNSAT is sound. +(iv) *Conclusion.* Say A₀ = {u : P_u = P₀} meets Γ(s) for every s ∈ Nbar(f₁). Then P₀·Q_s = 1 for all such s, so every row of A₀ is a Gram row +(M_us = κκ′g_us for all s, M_{uf₁} = κ_u p₀). Rows of O_{f₁} are Gram rows. With X := {f₁} ∪ (Nbar(f₁) ∖ A₀) the rows off X are Gram rows (D₂ = diag(κ′) with entry p₀ at f₁), +and r(L ∖ X) ⊇ r(O_{f₁}) ∪ {r_u} (u ∈ A₀) spans K⁸. CONJB Theorem G gives B-form or A2. The case B₀ is the transpose. ∎ + +## §2 Theorem Σ: Σ_a ≠ ∅ ⇒ B-form or A2 (E8). PROVEN +Let f₁ ∈ Σ_a and F ∋ f₁ any frame. By (Σ1), x ≡ 0 on O_{f₁}, i.e. D := D_F ⊆ Nbar(f₁). D ≠ ∅, otherwise rank ≤ 8. +(i) *Columns are Gram-shaped off index 1.* As in §1 (i), but using rows only (BSTAR Theorem P (i)): at p = {j,k} ⊆ {2..8} the rows of T_a, T_b are in Z, so every column at p is pinned +(old Theorem P sense), with a nonzero witness from a Z-row; triangles and gauge as before. So β_s|_{T(s)∖1} ∝ D_μσ^s. Rescale columns: b_s = (D_μ r_s, y_s) for s ∈ O_{f₁}. +(ii) *Remark (not used below).* Rows of O_{f₁} are Gram: α_u(1) = 0 and x_u = 0, so (D_μα_u, 0)·r_s = 0 for s ∈ O_u; since r_u has no f₁-component, (S1) gives α_u ∝ D_μ⁻¹r_u. +(iii) *Rows through 1.* Let u ∈ Nbar(f₁) and E6_u := O_u ∩ O_{f₁}. For s ∈ E6_u: α_u·D_μ r_s + x_u y_s = 0 (coordinate 1 does not meet s). +If u ∈ D this says y_s = g_u·r_s on E6_u, with g_u := proj_{f₁^⊥}(−D_μα_u/x_u) (only the projection matters, since r_s ⊥ f₁ on E6_u). +(iv) *Cocycle.* For u, u′ ∈ D: (g_u − g_{u′})·r_s = 0 on E6_u ∩ E6_{u′}. Let w_u := proj_{f₁^⊥} r_u. Antipodes (r_ū = f₁ − r_u) have E6_u = E6_ū and w_ū = −w_u. +**(S3′) CHECKED (spans3.py):** for u, u′ ∈ Nbar(f₁) not equal or antipodal, r(O_{f₁} ∩ O_u ∩ O_{u′}) spans ⟨r_{f₁}, r_u, r_{u′}⟩^⊥ (all 1512 pairs). With (S2) for antipodes, +g_u − g_{u′} ∈ ⟨w_u, w_{u′}⟩ for all u, u′ ∈ D. **(W2) CHECKED (spans3.py):** the 56 vectors w_u give 28 directions and no 3 of them lie in a 2-plane. +Apply the cocycle lemma of CONJB Theorem G to one representative per direction: with ≤ 2 directions its first case applies; with ≥ 3 directions, (W2) says no direction lies in the plane of two others, so its exceptional branch never occurs. This gives g ∈ f₁^⊥ with g − g_u ∈ ⟨w_u⟩ for each representative; for an antipode ū ∈ D, g_u − g_ū ∈ ⟨w_u⟩ by (S2) (E6_u = E6_ū spans ⟨f₁,u⟩^⊥), so g − g_ū ∈ ⟨w_ū⟩ too. +Since w_u ⊥ r_s on E6_u, **y_s = g·r_s on ∪_{u∈D} E6_u.** +(v) *Dichotomy.* Case 1: every s ∈ O_{f₁} is orthogonal to some u ∈ D. Then y = g·r on O_{f₁}, so b(O_{f₁}) ⊆ {(D_μρ, g·ρ) : ρ ∈ f₁^⊥} has dimension ≤ 7, i.e. f₁ ∈ Σ_b. + Theorem S applies. Case 2: some s ∈ O_{f₁} has O_s ∩ D = ∅. By (Σ4), s ∈ Σ_a. Then f₁ ⊥ s are both in Σ_a, and BSTAR Theorem A applies. ∎ +The transposed statement (Σ_b ≠ ∅) follows by symmetry (Theorem S and Theorem A are symmetric). +**Remark.** This is the mechanism BSTAR's (K″) was after: a star at f₁ makes f₁ a deviation line. (K″) itself is not needed. + +## §3 P112: Theorems S and Σ hold verbatim (CHECKED) +The proofs of §1–§2 use only: frames through every line inside L, P-compatibility (pinning at pairs avoiding index 1, the P ≠ Q witness, all 4 patterns per triple), +(S1), (S2_L) r(O_{f₁} ∩ O_u ∩ L) spans ⟨f₁,u⟩^⊥, (S3′_L) the triple version inside L, (W2) (a property of directions, inherited by subsets), Theorem A and Theorem G for L, +and the finite step §1 (iii) on the 52 lines Nbar(f₁) ∩ L. All P112 frames are P-compatible (BSTAR pcompat.py), Theorem A covers all P112 orthogonal pairs, Theorem G holds for P112. +CHECKED (job kstar_p112, jobs/kstar_p112.log): spansL.py P112, (S2_L) and (S3′_L) for every f₁ ∈ P112: 151648 span checks, 0 bad; runall.sh P112: §1 (iii) UNSAT + RUP-VERIFIED for all 112 choices of f₁. +So **Theorem Σ holds on P112**: Σ_a ∪ Σ_b ≠ ∅ ⇒ B-form or A2. The same residue Σ_a = Σ_b = ∅ remains (OPEN). + +## §4 The residue Σ_a = Σ_b = ∅ (OPEN) +Then every a(O_u) and b(O_u) spans 8 dims: a(O_u) spans b_u^⊥ and b(O_u) spans a_u^⊥, and this pairing is nondegenerate (its kernel would be ⟨a_u⟩, but a_u·b_u ≠ 0), so M[O_u, O_u] is a rank-8 realisation of the E7 pattern (Gram rank 7, plus one) for every u. +**This residue is where a third family would have to live. It is far from Gram (Gram has Σ_a = L), so BSTAR's first-order scan (inf3.py) says nothing about it.** +Consequences (PROVEN): for every frame F, D_F and D′_F meet O_s for every line s (Σ4), and Theorem P fails on both sides (otherwise Theorem G gives B-form or A2, and both have Σ ≠ ∅; +in B-form supp β ⊆ Σ_a). So every frame has a star in 𝒰_F and in 𝒰′_F. +**Class-level combinatorics cannot close it (CHECKED, kenc3.py):** Schur + mixed-class homogeneity (§5) + (Σ4) domination + stars on both sides is satisfiable, +e.g. x full on 11 tetrads and y full on 5 (k3.out). Value-level coupling is needed. Suggested route: the E7 recursion (B\* for rank-8 E7 realisations would give +M[O_u,O_u] B-form/A2 for every u, and the E7 Σ-lines then lift to E8 Σ-lines), or an anchor argument like §2 with D ∩ O_{f₁} small instead of empty. + +### §4.1 Why the E7 recursion is not a short route (scoping, round 2) +- In E7 = O_{f₁} each pair {j,k} ⊆ {2..8} lies in only two tetrads (the third tetrad through {j,k} contains 1). Theorem P (i) needs three: + two rows in different tetrads are equated through a column of the third. So neither rank-7 E7 rigidity nor an E7 Theorem P comes from the existing cards. +- Even a full E7 classification does not lift: an E7-Σ line v of the slice O_u means a(O_u ∩ O_v) spans 6 inside b_u^⊥ ∩ b_v^⊥ (7-dim). + That says nothing about ρ_a(O_v) in K⁹, so a gluing argument across all 120 slices would still be needed. +- The E7 residue (all E7-Σ empty) recurs one level down. The recursion only pays if it bottoms out in something computable, and that chain is unscoped. + +## §5 Side results (PROVEN) +- **Mixed-class homogeneity.** At a pair p, sign ε, if the row class R^ε_{T_i}(p) contains a Z-row and a D-row, then dim U_i = 2, so V_j = V_k = ⟨v⟩ (BSTAR §5 local lemma): + the columns of C^{−ε}_{T_j} ∪ C^{−ε}_{T_k} are all multiples of one vector v, hence all in Z′ (e₃ ∈ U_i) or all in D′. Transposed likewise. + An all-Z row class has dim U_i = 1 (constant φ). +- **Joint pinning (sharper Theorem P), corrected in round 2.** M̃ = M − xyᵀ has the correct zero pattern off D × D′. At (p, ε) the rows of R_1 ∪ R_2 ∪ R_3 are pinned + to one value iff the bipartite graph (edges R_i–C_j, i ≠ j, orthogonal, not both in D × D′) joins them. Sufficient: every C_j^{−ε} has a Z′ column + (each such column is adjacent to all rows of the other two tetrads). So if D′ contains no full ε-class, all rows are pinned, the gauge argument of Theorem P (ii)–(iii) + applies to rows, columns in Z′ are Gram, and transposed Theorem G gives B-form or A2. (The round-1 "only if R_i ⊆ D and C_j ∪ C_k ⊆ D′" was wrong: + pin1.out has rows of T₁ in Z, rows of T₂, T₃ in D, columns of T₁ in Z′, columns of T₂, T₃ in D′, and the graph splits into two components.) +- **The SAT abstraction of (K″)** (kenc.py/kenc2.py: Schur + homogeneity + Σ facts + Case B + F avoiding Σ_b + star) is satisfiable (k1.out, k2.out), so (K″) + cannot be proved at the class level either. Theorem Σ bypasses it. + +## §6 Files +Round 2: pin.py / pinL.py (P¹-valued pinning model; UNIT, FRAME env), soundtest.py (rule soundness on true data), p112orb.py (P112 frame orbits: 28 + 336 + 896, reps 0, 2, 26), +rupc.c (independent forward RUP checker in C, deletions honoured, RAT rejected; also re-verifies s56), certjob2.sh, num/probe.py and num/cfg.py (NUMERICAL, inconclusive: did not converge). + +s56.py (56-problem CNF; UNIT=E8|P112), rup.py (independent RUP checker), runall.sh (kissat + RUP for every f₁), spans3.py (S3′, W2 on E8, sympy exact), +spansL.py (S2_L, S3′_L mod 2³¹−1, ranks are at their maxima so exact), kenc.py, kenc2.py, kenc3.py, dec.py (class-level SAT abstractions; negative results). + +## §7 Round 2: the residue Σ_a = Σ_b = ∅ is empty (E8). Rules PROVEN, finite step CHECKED (certificate: see STATE) +**Theorem R.** On E8 there is no rank-9 iff-realisation with Σ_a = Σ_b = ∅. With Theorems S, Σ: **every rank-9 iff-realisation on E8 is B-form or in the A2 family (Conjecture B\* for E8).** +*Reduction (PROVEN).* Fix any frame F (W(E8) is transitive on frames, so frames()[0] suffices) and pivot coordinates. Call the rows *Gram-shaped* if for every pair p = {a,b} ⊆ F +the ratio ρ_p(u) = α_u(b)/α_u(a) takes one value on rows with ε_p = + and a different value on rows with ε_p = −. Then BSTAR §3 (ii)–(iii) (all triples, rows of a tetrad realise +all four patterns) give a gauge with α_u ∝ D_μ⁻¹σ^u; for s ∈ Z′ (y_s = 0), β_s ⊥ α(O_s), and (S1) gives β_s ∝ D_μ r_s, so the columns Z′ ⊇ F are Gram columns and +transposed Theorem G gives B-form or A2. Columns likewise (columns Gram-shaped ⇒ rows Z Gram ⇒ Theorem G). B-form and A2 both have Σ ≠ ∅ +(B: a line of supp β has c ≡ 0 on its O, so it is in Σ_a; A2: z is linear on O_{u_i}, so u_i ∈ Σ_b). So the residue forces: **neither rows nor columns are Gram-shaped**, and by (Σ4) +(H_F ≠ b_s^⊥ since no line is orthogonal to all of F) **D and D′ meet O_s for every line s.** +*Boolean model (pin.py).* Variables: x[u] (x_u ≠ 0), y[s]; for each pair p, equality of the values ρ_p(u) (rows) and τ_p(s) := −β_s(a)/β_s(b) (columns), all in K*; for each index i, +equality of rat_i(u) := x_u/α_u(i) (rows with x ≠ 0) and of y_s/β_s(i) (columns). Transitivity throughout. Since α_u|_p·β_s|_p = α_u(a)β_s(b)(ρ_p(u) − τ_p(s)), each rule below is a one-line proof: +- ORTH: u ∈ T_i, s ∈ T_j (T_i ∩ T_j = p), u ⊥ s: x_u y_s = 0 ⇒ ρ = τ; x_u y_s ≠ 0 ⇒ ρ ≠ τ (M_us = 0). NON: same sign at p (not orthogonal): x_u y_s = 0 ⇒ ρ ≠ τ. +- TRI: in a tetrad ⊇ {a,b,c}: ρ_abρ_bc = ρ_ac and τ_abτ_bc = −τ_ac. So row-row (col-col): two equalities ⇒ the third; row-col: two equalities ⇒ the third is unequal (char ≠ 2). +- K³ (BSTAR §5 local lemma): two rows of R^ε_{T_i}(p) with (φ, x) independent (ρ differs, or one has x = 0 and the other not) ⇒ dim U_i = 2 ⇒ V_j = V_k = ⟨v⟩: all columns of + C^{−ε}_{T_j} ∪ C^{−ε}_{T_k} have equal τ and equal y-status. ZZ: two x = 0 rows of one class have equal ρ (else V ⊆ ⟨e₃⟩, ψ = 0). Transposed versions. +- D1: if C^{−ε}_{T_j} ∪ C^{−ε}_{T_k} contains two independent (ψ, y) (τ differs, or a y = 0 and a y ≠ 0 column), then dim U_i = 1: the class rows are multiples of one (P, ξ), so + equal ρ_p, equal x-status, and equal rat_a, rat_b (a, b ∈ p). +- TW: rows u, w of T in a common 1-dim class at p = {a,b} and at the complementary pair {c,d}, x ≠ 0: equal rat_a and rat_c, hence ρ_ac(u) = ρ_ac(w). (Subsumed by the next two once encoded.) +- RATIO: rat_a/rat_b = ρ_ab, so two of {rat_a eq, rat_b eq, ρ_ab eq} ⇒ the third. Common partner: u ∈ R^ε_{T_i}, w ∈ R^ε_{T_k}, s ∈ C^{−ε}_{T_j} ({i,j,k} = {1,2,3}), x_u x_w y_s ≠ 0 and ρ_p(u) = ρ_p(w): + φ_u = λφ_w gives x_u = λx_w, so rat_a, rat_b equal. Transposed versions for columns. +- Schur; rank 9 (x, y ≢ 0); residue (D, D′ meet every O_s); "rows not Gram-shaped" and "columns not Gram-shaped" (a pair p and two rows with equal sign and different ρ, or opposite sign and equal ρ). +*Result (CHECKED).* kissat 4.0.4 with `--factor=false --preprocessfactor=false --no-binary`: UNSAT on pin3.cnf (56 784 vars, 3 513 012 clauses, frames()[0]). +pin3.drat (163 MB) is kept; it can be regenerated deterministically with exactly these flags (the default flags add bounded-variable-addition variables, which rupc rejects). +rupc pin3.cnf pin3.drat → "VERIFIED: top-level conflict after 2 382 724 lemmas". Every lemma up to that point was RUP-checked; after it, F ∧ lemmas already derives ⊥ by unit propagation. +So the proof is complete, not truncated. +**Audit targets:** (a) the reduction "Gram-shaped ⇒ B/A2 ⇒ Σ ≠ ∅"; (b) the rule proofs above (TRI row-column sign, D1, common partner); (c) rupc.c. Suggested: rerun soundtest.py with fresh seeds and rupc on pin3. Sanity: SAT with residue dropped, SAT with "not Gram-shaped" dropped. +*Soundness test (soundtest.py, NUMERICAL check of the rules, not part of the proof):* every clause (residue and non-Gram clauses off) is satisfied by the true Boolean data of +an exact E8 A2 instance and two B-forms (single-row; 8-clique), on random frames including star frames (|D| = |D′| = 56): 0 violations. +*How the earlier models failed and what kills them.* pin1.out (x on the 11 tetrads not through {1,2}, y on 3456, 3478, 5678) dies by TW: at {3,4} and {5,6} the 3456 rows are +twisted (x = t α(3) on each ε₃₄-class, x = t′α(5) on each ε₅₆-class), forcing equal ρ₃₅ on two rows of opposite ε₃₅, which the Z′ columns of 1357 and 2358 separate. +pin2.out (x, y on 1357, 2358, 2367, 2457) dies by RATIO: x/α(5) is constant on 1357, so ρ₃₅ cannot depend on ε₃₅. diff --git a/research/e8-rank9-realisations/evidence/logs/audit_dratrim_pin3.log.txt b/research/e8-rank9-realisations/evidence/logs/audit_dratrim_pin3.log.txt new file mode 100644 index 0000000000..dddbe4bb09 --- /dev/null +++ b/research/e8-rank9-realisations/evidence/logs/audit_dratrim_pin3.log.txt @@ -0,0 +1,8 @@ + c parsing input formula with 56784 variables and 3513012 clauses + c finished parsing + c detected empty clause; start verification via backward checking + c 111806 of 3513012 clauses in core + c 55104 of 2396186 lemmas in core using 21432804 resolution steps + c 0 RAT lemmas in core; 162570 redundant literals in core lemmas + s VERIFIED + c verification time: 124.806 seconds diff --git a/research/e8-rank9-realisations/evidence/logs/dratrim_shipped_pin3.log.txt b/research/e8-rank9-realisations/evidence/logs/dratrim_shipped_pin3.log.txt new file mode 100644 index 0000000000..2f38848a5f --- /dev/null +++ b/research/e8-rank9-realisations/evidence/logs/dratrim_shipped_pin3.log.txt @@ -0,0 +1,11 @@ + c parsing input formula with 56784 variables and 3513012 clauses + c finished parsing + c detected empty clause; start verification via backward checking + c 111806 of 3513012 clauses in core + c 55104 of 2396186 lemmas in core using 21432804 resolution steps + c 0 RAT lemmas in core; 162570 redundant literals in core lemmas + s VERIFIED + c verification time: 137.062 seconds +real 137.10 +user 134.15 +sys 0.89 diff --git a/research/e8-rank9-realisations/evidence/logs/kstar_cert2_E8_pin3_rupc.log.txt b/research/e8-rank9-realisations/evidence/logs/kstar_cert2_E8_pin3_rupc.log.txt new file mode 100644 index 0000000000..615ae599bf --- /dev/null +++ b/research/e8-rank9-realisations/evidence/logs/kstar_cert2_E8_pin3_rupc.log.txt @@ -0,0 +1,5 @@ +== E8 pin3 +s UNSATISFIABLE +162608912 +read 3513012 clauses, top-level trail 0, conflict 0 +VERIFIED: top-level conflict after 2382724 lemmas (2761873 deletions) diff --git a/research/e8-rank9-realisations/evidence/logs/kstar_s56_E8_f1_0-15.log.txt b/research/e8-rank9-realisations/evidence/logs/kstar_s56_E8_f1_0-15.log.txt new file mode 100644 index 0000000000..93822cb576 --- /dev/null +++ b/research/e8-rank9-realisations/evidence/logs/kstar_s56_E8_f1_0-15.log.txt @@ -0,0 +1,16 @@ +E8 f1=0 s UNSATISFIABLE | VERIFIED: empty clause derived by RUP after 4863 lemmas +E8 f1=1 s UNSATISFIABLE | VERIFIED: empty clause derived by RUP after 4863 lemmas +E8 f1=2 s UNSATISFIABLE | VERIFIED: empty clause derived by RUP after 4863 lemmas +E8 f1=3 s UNSATISFIABLE | VERIFIED: empty clause derived by RUP after 4863 lemmas +E8 f1=4 s UNSATISFIABLE | VERIFIED: empty clause derived by RUP after 4863 lemmas +E8 f1=5 s UNSATISFIABLE | VERIFIED: empty clause derived by RUP after 4863 lemmas +E8 f1=6 s UNSATISFIABLE | VERIFIED: empty clause derived by RUP after 4863 lemmas +E8 f1=7 s UNSATISFIABLE | VERIFIED: empty clause derived by RUP after 4863 lemmas +E8 f1=8 s UNSATISFIABLE | VERIFIED: empty clause derived by RUP after 4863 lemmas +E8 f1=9 s UNSATISFIABLE | VERIFIED: empty clause derived by RUP after 4863 lemmas +E8 f1=10 s UNSATISFIABLE | VERIFIED: empty clause derived by RUP after 4863 lemmas +E8 f1=11 s UNSATISFIABLE | VERIFIED: empty clause derived by RUP after 4863 lemmas +E8 f1=12 s UNSATISFIABLE | VERIFIED: empty clause derived by RUP after 4863 lemmas +E8 f1=13 s UNSATISFIABLE | VERIFIED: empty clause derived by RUP after 4863 lemmas +E8 f1=14 s UNSATISFIABLE | VERIFIED: empty clause derived by RUP after 4872 lemmas +E8 f1=15 s UNSATISFIABLE | VERIFIED: empty clause derived by RUP after 4863 lemmas diff --git a/research/e8-rank9-realisations/evidence/pins.tsv b/research/e8-rank9-realisations/evidence/pins.tsv new file mode 100644 index 0000000000..83ff958834 --- /dev/null +++ b/research/e8-rank9-realisations/evidence/pins.tsv @@ -0,0 +1,4 @@ +# sha256 of the generated objects (CNFs are byte-identical to the working cards' files; pin3.drat = decompressed evidence/proofs/pin3.drat.xz) +7e5351721bf838d9f7d1b27d6849219b96a1fdc3cee8bc236b21c6e15525235a pin3.cnf checks/pin.py (no arguments); 56784 variables, 3513012 clauses +3cf289978f9f7c249fbe9204db935d9f50f584f43a8568f7eefdcc2299b7c621 pin3.drat kissat 4.0.4 --factor=false --preprocessfactor=false --no-binary; 162608912 bytes +a541edbb7b6b13a0171eced5d77fc73be73f2fe1b82e4378a9261b0ddfeae7a2 s56_0.cnf checks/s56.py s56_0.cnf 0 ; 6328 variables, 503608 clauses diff --git a/research/e8-rank9-realisations/evidence/proofs/pin3.drat.xz b/research/e8-rank9-realisations/evidence/proofs/pin3.drat.xz new file mode 100644 index 0000000000..4e6a4bb1f8 Binary files /dev/null and b/research/e8-rank9-realisations/evidence/proofs/pin3.drat.xz differ diff --git a/research/e8-rank9-realisations/requirements.txt b/research/e8-rank9-realisations/requirements.txt new file mode 100644 index 0000000000..1eb1d2ffdc --- /dev/null +++ b/research/e8-rank9-realisations/requirements.txt @@ -0,0 +1,4 @@ +# Tested with Python 3.14.7. Steps 1 and 4 need: +numpy>=1.26 +sympy>=1.12 +# Tools (not vendored): kissat 4.0.4 (KISSAT=/path), drat-trim (DRAT_TRIM=/path; the standard checker), a C compiler (CC=cc) for the auxiliary rupc.c, xz. Never CaDiCaL. diff --git a/research/e8-rank9-realisations/verify.sh b/research/e8-rank9-realisations/verify.sh new file mode 100755 index 0000000000..7d5ed97157 --- /dev/null +++ b/research/e8-rank9-realisations/verify.sh @@ -0,0 +1,82 @@ +#!/usr/bin/env bash +# Verification of research/e8-rank9-realisations (no kappa claim). usage: bash verify.sh [/fresh/output/dir] PYTHON= KISSAT= DRAT_TRIM= CC= +# 0 MANIFEST.sha256 +# 1 exact finite facts: both families exist on E8 (a2e8.py); span facts S1/S2 (spans.py), S3' and W2 (spans3.py); P-compatible frames and orthogonal-pair coverage (pframes.py) +# 2 Theorem S finite step (56-line incidence problem): CNF regenerated (sha256 pinned for f1 = 0), kissat UNSAT, standard drat-trim VERIFIED, auxiliary rupc VERIFIED; f1 = 0..15 (FULL=1: all 120 lines) +# 3 Theorem R finite step (pin.py ratio-equality model): CNF regenerated, sha256 equal to the pinned one (byte-identical to the working card's CNF); shipped DRAT (xz) decompresses to the pinned sha256. +# FULL=1 additionally: standard drat-trim on the shipped proof (about 2-3 min), then a fresh kissat solve (flags as for the shipped proof; limit 1200 s) and drat-trim on the fresh proof. +# 4 soundness test of the pin.py rules on true data (A2 family: 5 parameter/triangle draws; B-form), and a mutation control (one flipped sign in the TRI row-column rule must be caught) +# 5 recorded logs (not re-run): the audit's drat-trim VERIFIED on pin3, the working card's rupc runs +# One heavy process at a time, run under nice 10. Missing numpy/sympy/kissat/drat-trim/cc/xz => SKIP lines (never PASS) and exit 1. +set -uo pipefail +HERE=$(cd "$(dirname "$0")" && pwd) +OUT=${1:-$(mktemp -d "${TMPDIR:-/tmp}/e8rank9.XXXXXX")} +mkdir -p "$OUT"; OUT=$(cd "$OUT" && pwd) +case "$OUT/" in "$HERE"/*) echo "output dir must be outside the package"; exit 2;; esac +PY="${PYTHON:-python3}"; KISSAT="${KISSAT:-kissat}"; DT="${DRAT_TRIM:-drat-trim}"; CC="${CC:-cc}" +export PYTHONDONTWRITEBYTECODE=1 OMP_NUM_THREADS=1 VECLIB_MAXIMUM_THREADS=1 OPENBLAS_NUM_THREADS=1 +NICE="nice -n 10"; C="$HERE/checks"; EV="$HERE/evidence"; W="$OUT/work"; mkdir -p "$W" "$OUT/logs"; : > "$OUT/all.out"; T0=$SECONDS +note() { echo "$@" | tee -a "$OUT/all.out"; } +sha() { shasum -a 256 "$1" 2>/dev/null | cut -d' ' -f1 || sha256sum "$1" | cut -d' ' -f1; } +pin() { awk -F'\t' -v n="$1" '$2==n{print $1}' "$EV/pins.tsv"; } +echo "== 0. manifest" +if ! "$PY" -B "$C/manifest_check.py" | tee -a "$OUT/all.out" | sed 's/^/ /' || grep -q '^FAIL' "$OUT/all.out"; then echo "step 0 FAILED"; exit 1; fi +HAVE=1 +"$PY" -c "import numpy, sympy" 2>/dev/null || { note "SKIP python needs numpy and sympy"; HAVE=0; } +for t in "$KISSAT" "$DT" "$CC" xz; do command -v "$t" >/dev/null 2>&1 || { note "SKIP tool missing: $t"; HAVE=0; }; done +[ "$HAVE" = 0 ] && { echo "INCOMPLETE: tools missing"; exit 1; } +runpy() { local n=$1; shift; ( cd "$W" && $NICE "$PY" -B "$C/$1" "${@:2}" > "$OUT/logs/$n.log" 2>&1 ); local rc=$? + grep '^PASS' "$OUT/logs/$n.log" | sed 's/^/ /' | tee -a "$OUT/all.out" >/dev/null + if [ $rc = 0 ] && grep -q '^PASS' "$OUT/logs/$n.log"; then note "PASS ran $n"; else note "FAIL ran $n (exit $rc)"; tail -3 "$OUT/logs/$n.log" | sed 's/^/ /'; fi; } +echo "== 1. exact finite facts" +runpy a2e8 a2e8.py; runpy spans spans.py; runpy spans3 spans3.py; runpy pframes pframes.py +echo "== 2. Theorem S finite step: 56-line incidence problem" +$CC -O2 -o "$W/rupc" "$C/rupc.c" 2>/dev/null || note "FAIL compile rupc.c" +if [ "${FULL:-0}" = 1 ]; then F1S=$(seq 0 119); else F1S=$(seq 0 15); fi +ok=0; n=0 +for f in $F1S; do + n=$((n+1)); ( cd "$W" && $NICE "$PY" -B "$C/s56.py" s56_$f.cnf $f > /dev/null ) + if [ $f = 0 ]; then [ "$(sha "$W/s56_0.cnf")" = "$(pin s56_0.cnf)" ] && note "PASS s56_0.cnf regenerated: sha256 equals the pinned value" || note "FAIL s56_0.cnf sha256"; fi + r=$(cd "$W" && timeout 1200 $NICE "$KISSAT" -q --factor=false --preprocessfactor=false s56_$f.cnf s56_$f.drat --no-binary | head -1) + d=$(cd "$W" && timeout 1200 $NICE "$DT" s56_$f.cnf s56_$f.drat 2>&1 | tr '\r' '\n' | grep -E '^s ') + a=$("$W/rupc" "$W/s56_$f.cnf" "$W/s56_$f.drat" 2>&1 | grep -c '^VERIFIED') + if [ "$r" = "s UNSATISFIABLE" ] && [ "$d" = "s VERIFIED" ] && [ "$a" = 1 ]; then ok=$((ok+1)); else note "FAIL s56 f1=$f: kissat '$r' drat-trim '$d' rupc $a"; fi + rm -f "$W/s56_$f.cnf" "$W/s56_$f.drat" +done +[ $ok = $n ] && note "PASS Theorem S finite step: $n/$n choices of f1: kissat UNSAT, standard drat-trim VERIFIED, rupc VERIFIED" || note "FAIL Theorem S finite step: $ok/$n" +echo "== 3. Theorem R finite step: pinning model" +( cd "$W" && $NICE "$PY" -B "$C/pin.py" pin3.cnf > "$OUT/logs/pin_gen.log" 2>&1 ) +[ "$(sha "$W/pin3.cnf")" = "$(pin pin3.cnf)" ] && note "PASS pin3.cnf regenerated: sha256 equals the pinned value ($(cat "$OUT/logs/pin_gen.log"))" || note "FAIL pin3.cnf sha256" +[ "$(xz -dc "$EV/proofs/pin3.drat.xz" | shasum -a 256 | cut -d' ' -f1)" = "$(pin pin3.drat)" ] && note "PASS shipped proof decompresses to the pinned sha256 (pin3.drat)" || note "FAIL shipped proof sha256" +if [ "${FULL:-0}" = 1 ]; then + xz -dc "$EV/proofs/pin3.drat.xz" > "$W/pin3_shipped.drat" + r=$(cd "$W" && timeout 1200 $NICE "$DT" pin3.cnf pin3_shipped.drat 2>&1 | tee "$OUT/logs/dt_shipped.log" | tr '\r' '\n' | grep -E '^s ') + [ "$r" = "s VERIFIED" ] && note "PASS standard drat-trim: shipped pin3 proof VERIFIED" || note "FAIL drat-trim on shipped pin3 proof: '$r'" + rm -f "$W/pin3_shipped.drat" + s=$SECONDS; r=$(cd "$W" && timeout 1200 $NICE "$KISSAT" -q --factor=false --preprocessfactor=false pin3.cnf pin3_fresh.drat --no-binary | head -1) + if [ "$r" = "s UNSATISFIABLE" ]; then + note "PASS fresh kissat solve: UNSAT in $((SECONDS-s))s" + r=$(cd "$W" && timeout 1200 $NICE "$DT" pin3.cnf pin3_fresh.drat 2>&1 | tee "$OUT/logs/dt_fresh.log" | tr '\r' '\n' | grep -E '^s ') + [ "$r" = "s VERIFIED" ] && note "PASS standard drat-trim: fresh pin3 proof VERIFIED" || note "FAIL drat-trim on fresh pin3 proof: '$r'" + else note "FAIL fresh kissat solve of pin3.cnf: '$r'"; fi + rm -f "$W/pin3_fresh.drat" +else note "SKIP-FULL pin3 re-solve and drat-trim (set FULL=1; shipped proof, its sha256 and the recorded checker logs are checked in steps 3 and 5)"; fi +echo "== 4. soundness test of the pin.py rules" +mkdir -p "$W/mut"; cp "$C"/*.py "$W/mut/" +( cd "$W" && $NICE "$PY" -B "$C/soundtest.py" 0 3 > "$OUT/logs/soundtest.log" 2>&1 ) +grep -q '^TOTAL violated 0$' "$OUT/logs/soundtest.log" && [ "$(grep -c '^A2 seed' "$OUT/logs/soundtest.log")" = 5 ] && note "PASS soundtest: 0 clause violations on true data (5 A2 draws on 5 triangles, 2 B-form instances, 3 random frames each)" || note "FAIL soundtest" +sed -i.bak 's/else: cl.append(\[-o\[0\],-o\[1\],-vs\[k\]\])/else: cl.append([-o[0],-o[1],vs[k]])/' "$W/mut/pin.py" +if cmp -s "$W/mut/pin.py" "$W/mut/pin.py.bak"; then note "FAIL mutation control: pattern not found"; else + ( cd "$W/mut" && $NICE "$PY" -B soundtest.py 0 1 > "$OUT/logs/soundtest_mut.log" 2>&1 ) + v=$(grep '^TOTAL violated' "$OUT/logs/soundtest_mut.log" | awk '{print $3}') + [ -n "$v" ] && [ "$v" -gt 0 ] && note "PASS mutation control: flipping the TRI row-column sign is caught ($v violated clauses)" || note "FAIL mutation control: not caught"; fi +echo "== 5. recorded logs (not re-run here)" +crlf() { tr '\r' '\n' < "$1"; } +crlf "$EV/logs/dratrim_shipped_pin3.log.txt" | grep -q '^s VERIFIED' && note "PASS recorded: drat-trim on the decompressed shipped proof: s VERIFIED" || note "FAIL recorded shipped-proof drat-trim log" +crlf "$EV/logs/audit_dratrim_pin3.log.txt" | grep -q '^s VERIFIED' && grep -q '56784 variables and 3513012 clauses' "$EV/logs/audit_dratrim_pin3.log.txt" && note "PASS recorded: independent audit's standard drat-trim run on pin3: s VERIFIED (3513012 clauses)" || note "FAIL recorded audit drat-trim log" +grep -q 'VERIFIED: top-level conflict after 2382724 lemmas' "$EV/logs/kstar_cert2_E8_pin3_rupc.log.txt" && note "PASS recorded: working card's rupc run on pin3: VERIFIED after 2382724 lemmas" || note "FAIL recorded rupc log" +[ "$(grep -c 'VERIFIED: empty clause derived by RUP' "$EV/logs/kstar_s56_E8_f1_0-15.log.txt")" = 16 ] && note "PASS recorded: s56 for f1 = 0..15 all UNSAT + RUP-VERIFIED" || note "FAIL recorded s56 log" +npass=$(grep -c '^PASS' "$OUT/all.out"); nfail=$(grep -c '^FAIL' "$OUT/all.out"); nskip=$(grep -c '^SKIP' "$OUT/all.out") +echo "== done in $((SECONDS - T0))s: $((npass + 2)) PASS (2 in step 0), $nskip SKIP, $nfail FAIL; logs in $OUT" +if [ "$nfail" = 0 ]; then [ "${FULL:-0}" = 1 ] && echo "PASS: all assertions hold (FULL)" || echo "PASS: all default assertions hold (pin3 re-solve / drat-trim: FULL=1)"; exit 0; fi +echo "FAIL"; exit 1