From 57c614dcf31e04f6dfa31290423408bbef93b763 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Thu, 15 Oct 2026 05:44:51 +0530 Subject: [PATCH 1/2] research: Desargues/Pappus T=3 decoder atoms, char-2 (CR2) classification New package research/three-total-classical-configs (research note, no kappa claim). It answers OPEN ENDS item 4 of the #2111 handoff for Desargues 10_3 and Pappus 9_3 in structured coordinates, conditional on #2162 Lemma CR2. - Frame-universal char-2 certificates for all 221 Desargues frames (GF(16)) and all 151 Pappus frames (GF(4)), plus every frame of 12 special Pappus extra-triple signatures. By Lemma U, every decoder configuration built from these frames satisfies (A). - Desargues admits no extra triples, so every exact Q-realisation is covered. GF(2/4/8) are exhaustively excluded. An independent count finds no exact Desargues 10_3 in PG(2,4) or PG(2,8). - One mixed coordinate system of a special Pappus realisation has no certificate. There, 88 of 2000 sampled instances are non-CR2. The 18 with f <= 26 have exact min(cost - v) = 1; 70 are skipped. This is a bounded failed search, not a proof of (A). Vendored from #2162 (head 113a7182) with pins and Apache-2.0 notice: lib/cr2.py, c/enumall.c (= #2111) and data. Base 0fdd7d82. Verify: python3 -I -B research/three-total-classical-configs/verify.py Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). Co-Authored-By: Claude Opus 5.5 --- .../three-total-classical-configs/LICENSE | 201 ++++++++++++ .../MANIFEST.sha256 | 18 ++ .../three-total-classical-configs/NOTICE.md | 23 ++ .../three-total-classical-configs/README.md | 185 +++++++++++ .../SOURCES.json | 18 ++ .../three-total-classical-configs/TASK.json | 88 ++++++ .../three-total-classical-configs/VERIFY.json | 19 ++ .../three-total-classical-configs/c/enumall.c | 28 ++ .../data/cex_min_1.json | 1 + .../data/cr2_realisations.json | 1 + .../data/instances.json | 1 + .../data/special.json | 1 + .../data/special_instances.json | 1 + .../data/tied_min.json | 1 + .../data/tm_noncr2.json | 1 + .../data/universal.json | 1 + .../lib/classical.py | 199 ++++++++++++ .../three-total-classical-configs/lib/cr2.py | 85 +++++ .../lib/universal.py | 118 +++++++ .../scripts/special_instances.py | 45 +++ .../scripts/special_sweep.py | 81 +++++ .../scripts/sweep.py | 120 +++++++ .../scripts/universal_sweep.py | 47 +++ .../three-total-classical-configs/verify.py | 293 ++++++++++++++++++ 24 files changed, 1576 insertions(+) create mode 100644 research/three-total-classical-configs/LICENSE create mode 100644 research/three-total-classical-configs/MANIFEST.sha256 create mode 100644 research/three-total-classical-configs/NOTICE.md create mode 100644 research/three-total-classical-configs/README.md create mode 100644 research/three-total-classical-configs/SOURCES.json create mode 100644 research/three-total-classical-configs/TASK.json create mode 100644 research/three-total-classical-configs/VERIFY.json create mode 100644 research/three-total-classical-configs/c/enumall.c create mode 100644 research/three-total-classical-configs/data/cex_min_1.json create mode 100644 research/three-total-classical-configs/data/cr2_realisations.json create mode 100644 research/three-total-classical-configs/data/instances.json create mode 100644 research/three-total-classical-configs/data/special.json create mode 100644 research/three-total-classical-configs/data/special_instances.json create mode 100644 research/three-total-classical-configs/data/tied_min.json create mode 100644 research/three-total-classical-configs/data/tm_noncr2.json create mode 100644 research/three-total-classical-configs/data/universal.json create mode 100644 research/three-total-classical-configs/lib/classical.py create mode 100644 research/three-total-classical-configs/lib/cr2.py create mode 100644 research/three-total-classical-configs/lib/universal.py create mode 100644 research/three-total-classical-configs/scripts/special_instances.py create mode 100644 research/three-total-classical-configs/scripts/special_sweep.py create mode 100644 research/three-total-classical-configs/scripts/sweep.py create mode 100644 research/three-total-classical-configs/scripts/universal_sweep.py create mode 100644 research/three-total-classical-configs/verify.py diff --git a/research/three-total-classical-configs/LICENSE b/research/three-total-classical-configs/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/three-total-classical-configs/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/three-total-classical-configs/MANIFEST.sha256 b/research/three-total-classical-configs/MANIFEST.sha256 new file mode 100644 index 0000000000..4dbb57619a --- /dev/null +++ b/research/three-total-classical-configs/MANIFEST.sha256 @@ -0,0 +1,18 @@ +ff3c1bbd072c4d1f47158f903aa3ff4fcd8db5bbc4709c3d15b21a1815eef3bd lib/cr2.py +55d864202535c22952e1a9080ad834f1908d18ff857c8dc26211e25a847d1fc8 c/enumall.c +670ed90924b601ade22f0d4adaff46d1667e5449326a0f7ba7b88dd8f5906f93 data/tied_min.json +b5aa8ca01a87a898ae27160d5274af7ff08127cf0b27cf372f73a5725cd216a5 data/tm_noncr2.json +2ce114152529d375215f1f64a45072c9b78d1719d156e76bc692eff1fa955666 data/cr2_realisations.json +86064701dde94b4f35427bc3e19275eaf1e40e9e90d4fea28e7857f3564d4dd7 data/cex_min_1.json +1680542d1763a5dd99df26cb7b9b82ec213164b0ee846e4a65acb86cb446d9d7 lib/classical.py +711780269d90511e1ed3343344e4e57fadf9ffeabaf7f5a5027ae29c3d8d4929 lib/universal.py +0b637ec2a8c756ef732ac7b6e7119d52cc1f80e6b6d46f00c573c3ed1579e056 scripts/sweep.py +1af3dce8ed475f13c3c3ca90e937131ba36a98423935770aed979a8b41c01407 scripts/universal_sweep.py +a350284181fd833e725ff5ec3fbc1dc4ffc2872b2faa8a2e575a6f3456fe64e7 scripts/special_sweep.py +0f3938a250e718b2c206bd1aef4aacffad7c68b8b727eb5e5d7ad06806a10d90 scripts/special_instances.py +e3bd487332f0c34a967422eca486fda0c71b687bfb3d3e1bb2f32301587a4d63 data/universal.json +4fd5a9949d561010ba6a3004e031b1b724c6ca6e292d37f107907be998b7a792 data/instances.json +8aa943bf814214b0587db4531fb88f37af2bbc4f5819eb2072454ec8cc7b510f data/special.json +6cf47badb1bec2e3effe232ae99c8614d35d884ead18986e37970f60565eb066 data/special_instances.json +c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4 LICENSE +467ecef13686b9f946edb0f8529b0f5be1a7fbe6887a86a8f25a3631c8a630a8 NOTICE.md diff --git a/research/three-total-classical-configs/NOTICE.md b/research/three-total-classical-configs/NOTICE.md new file mode 100644 index 0000000000..577c9a46d5 --- /dev/null +++ b/research/three-total-classical-configs/NOTICE.md @@ -0,0 +1,23 @@ +# Notice + +New work in this package: thakrarsagar, with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). +Apache-2.0 (`LICENSE`, identical to the repository root licence). + +## Vendored files (unchanged copies, Apache-2.0, author DreamingOfClouds) + +| path | source | sha256 | +|---|---|---| +| `lib/cr2.py` | PR #2162 head `113a718265c62aec301c5695f4bfb9c421bef7ab`, `research/char2-jets/lib/cr2.py` | `ff3c1bbd072c4d1f47158f903aa3ff4fcd8db5bbc4709c3d15b21a1815eef3bd` | +| `c/enumall.c` | PR #2162 head (identical to PR #2111 head `98da76c2839ba38538b510420dec54546ccabf0b`, `research/three-total-decoders/c/enumall.c`) | `55d864202535c22952e1a9080ad834f1908d18ff857c8dc26211e25a847d1fc8` | +| `data/tied_min.json` | #2111 / #2162 `data/tied_min.json` | `670ed90924b601ade22f0d4adaff46d1667e5449326a0f7ba7b88dd8f5906f93` | +| `data/cex_min_1.json` | #2111 / #2162 `data/cex_min_1.json` | `86064701dde94b4f35427bc3e19275eaf1e40e9e90d4fea28e7857f3564d4dd7` | +| `data/tm_noncr2.json` | #2162 `data/tm_noncr2.json` | `b5aa8ca01a87a898ae27160d5274af7ff08127cf0b27cf372f73a5725cd216a5` | +| `data/cr2_realisations.json` | #2162 `data/cr2_realisations.json` | `2ce114152529d375215f1f64a45072c9b78d1719d156e76bc692eff1fa955666` | + +`verify.py` checks these hashes. The #2162 package itself credits #446/#595 (model), #717, #1590 (Lemma B) and #2111. + +## Written for this package + +`lib/classical.py` (realisations, frames, model re-implementation), `lib/universal.py` (frame-universal char-2 search), +`scripts/*.py`, `verify.py`, `data/universal.json`, `data/instances.json`, `data/special.json`, +`data/special_instances.json`, `README.md`, `MANIFEST.sha256` and the package metadata. diff --git a/research/three-total-classical-configs/README.md b/research/three-total-classical-configs/README.md new file mode 100644 index 0000000000..8a613404a3 --- /dev/null +++ b/research/three-total-classical-configs/README.md @@ -0,0 +1,185 @@ +# Desargues 10_3 and Pappus 9_3 as three-total (T = 3) decoder atoms: char-2 (CR2) classification + +**Status: research note / scoped result. No κ claim, no new bound on T(n).** This package answers OPEN ENDS item 4 of +the #2111 handoff ("untested: classical rich configurations (Pappus, Desargues, Reye, D4 line arrangements) as possible tight +atoms or counterexamples") for **Desargues and Pappus only**, in structured coordinates. It is conditional on +**Lemma CR2 of the open PR #2162**, which is inherited and not re-proved here. + +Base commit `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. Predecessor pins: PR #2111 head +`98da76c2839ba38538b510420dec54546ccabf0b`, PR #2162 head `113a718265c62aec301c5695f4bfb9c421bef7ab` (vendored files and +hashes in [NOTICE.md](NOTICE.md)). The selected record (`certificates/selected-result.json`, κ = 0.001672660197076918, +#1094) is untouched and unaffected. + +## Question + +Model (#2111 §1, from #446/#595): a T = 3 decoder configuration is a list of v pairs (p(t), q(t)) ∈ Z³ × Z³ with +p(t)·q(t) ≠ 0. R_j = {t : p_j(t) ≠ 0}, A_j = {s : q_j(s) ≠ 0}. An admissible B over F₂ has unit diagonal and B_ts = 1 (t ≠ s) +only where p(t)·q(s) = 0. cost(B) = Σ_j rank_F₂ B[R_j, A_j]. Statement **(A)**: cost(B) ≥ v for every admissible B. (A) is open at +T = 3 (#2111 §10). #2162 proves **Lemma CR2**: if there are P̃(t), Q̃(s) over a field of characteristic 2 with +supp P̃(t) ⊆ supp p(t), supp Q̃(s) ⊆ supp q(s), P̃(t)·Q̃(s) = 0 for every in-block incidence, and P̃(t)·Q̃(t) ≠ 0, then (A) holds +for that configuration, for every B. + +Hypothesis tested (task card): coordinates in which configuration points or lines form the coordinate triangle are rich in +zeros. The support restriction might block a char-2 realisation, as the anti-Fano configuration `tied_min` does. Such +instances would be where (A) is genuinely open, and they could give new tight atoms or a counterexample. + +## Result + +1. **Every structured Desargues/Pappus decoder configuration satisfies (A) (conditional on CR2).** The objects are: + - Desargues 10_3 and Pappus 9_3 over Q. Each is an exact realisation, checked to have exactly the 30 / 27 incidences. + - Every structured frame. A frame is three non-collinear configuration points sent to e₁, e₂, e₃, or three non-concurrent + configuration lines sent to the coordinate lines. There are 110 + 110 Desargues frames and 75 + 75 Pappus frames, plus + the identity coordinates. + + For each frame, `data/universal.json` stores a **frame-universal** char-2 realisation: X(point) and Y(line) over GF(16) + for Desargues and over GF(4) for Pappus. The supports of X and Y lie inside the frame supports, and X·Y = 0 holds exactly + when the point lies on the line. Lemma U below turns one such certificate into a CR2 realisation for **every** decoder + configuration whose pairs are non-incident (configuration point, configuration line) pairs in that frame. This holds for + any v and allows repeated points or lines. A sample of 740 configurations (v = 6..10, seed 22) is cross-checked: + the vendored #2162 `cr2.py` DFS (GF(2)/GF(4)/GF(8)) or the a = 0 2-adic test certifies each instance independently. +2. **Which realisations are covered.** + - **Desargues: every exact realisation over Q.** By Lemma Z, the frame zero pattern depends only on the incidences and + on any extra collinear point triples or concurrent line triples. Desargues 10_3 cannot have extra triples, because any + three points include two on a common configuration line (and dually; check 6). + - **Pappus: realisations with each extra-triple signature found by the parameter grid.** The grid found the generic + signature and 12 special ones. Each has a single A_iB_iC_i collinearity, a single concurrency ({l,m,pap}, + {A0B1,A1B2,A2B0} or {A0B2,A1B0,A2B1}), or one of each. For every structured frame of every one of these signatures, + `data/special.json` holds a GF(4) universal certificate. +3. **Field size (side fact).** + - Desargues frame-universal realisations are exhaustively excluded over GF(2), GF(4) and GF(8) in every frame. + - An independent constructive count confirms this. It fixes O, a₀, a₁ = e₁, e₂, e₃ and enumerates a₂ and μ_i. It finds + **no exact Desargues 10_3 in PG(2,4) or PG(2,8)**, but finds 1344 in PG(2,16) with a₂ fixed. + - In the frame (O, a₀, a₁), relaxing exactly one of the 10 "opposite" non-incidences (for example the centre O and the + axis) makes GF(8) feasible, and relaxing any other single non-incidence does not. This was an exploratory run and is + not part of the verifier. + - On the sampled instances the per-instance DFS never needed more than GF(4) (740 Desargues/Pappus samples: 710 GF(2), + 10 GF(4), 20 by the 2-adic test). So GF(16) is a cost of universality only. We did not search the literature for this + embedding fact. +4. **Where CR2 does fail (the hypothesis, confirmed once).** One coordinate system has no frame-universal certificate: + - The configuration is the special Pappus realisation `a=(0,1,-1), b=(0,-15,15)`. In it A₀B₀C₀ are collinear and l, m and + pap are concurrent. + - Its coordinates are the stored ones. The coordinate line x = 0 is the extra line A₀B₀C₀, e₁ is the concurrency point, + and e₃ = A₀. This frame is mixed: it uses non-configuration elements. + - No universal realisation exists there over GF(2..16) (exhaustive). The same realisation in full-support coordinates + does have one over GF(4) (exploratory check with one integer change of coordinates; not in the verifier). So the obstruction comes from the support restriction. + - We sampled 2000 decoder configurations in this frame (seed 22, v = 6..10). Of these, 1912 are CR2 and + **88 are not CR2** over GF(2), GF(4) or GF(8). + - 18 non-CR2 instances have f ≤ 26. For these, the exact minimum over all 2^f admissible B (vendored `enumall.c`; + witnesses rechecked in pure Python, f ≤ 18 also exhausted in pure Python) gives **min(cost − v) = 1**. + Distribution of (v, f, min): (7,16,11), (7,17,9), (7,18,10), (7,19,10), (8,20,11), (8,21,11), (8,22,11), (8,24,9), (8,24,11), (8,25,12), (8,26,10), (8,26,11), (9,19,13), (9,24,11), (9,24,12) ×2, (9,26,12), (9,26,14); the single cost − v = 1 instance is (v, f, min) = (8, 24, 9). The non-CR2 instances by v: 4 at v = 7, 9 at v = 8, 20 at v = 9, 55 at v = 10, none at v = 6. The skipped f range is 27..45. + - 70 instances have f > 26 and were skipped (counted, not claimed). + + So, within this bounded search, no counterexample and no tight non-CR2 atom was found. This is a failed finite search, + not a proof of (A) for this frame. + +Counts printed by the verifier: CR2-certified 2652, non-CR2 exact 18, skipped 70; min(cost − v) over the +non-CR2 exact set = 1. + +### Lemma U (frame-universal certificate ⇒ CR2 for every pair list) + +Let P[i] and L[k] be the frame coordinates of the configuration points and lines. Let X[i] and Y[k] be over GF(2^r) with +supp X[i] ⊆ supp P[i], supp Y[k] ⊆ supp L[k], and X[i]·Y[k] = 0 ⇔ P[i]·L[k] = 0. Take any decoder configuration +(p(t), q(t)) = (λ_t P[i_t], μ_t L[k_t]) with λ_t, μ_t ≠ 0 and P[i_t]·L[k_t] ≠ 0, and put P̃(t) = X[i_t], Q̃(t) = Y[k_t]. +- Supports: they shrink as required. +- In-block incidences: if p(t)·q(s) = 0, then P[i_t]·L[k_s] = 0, so X·Y = 0. +- Diagonal: P[i_t]·L[k_t] ≠ 0, so X[i_t]·Y[k_t] ≠ 0. + +This gives the hypotheses of Lemma CR2 (#2162), so cost(B) ≥ v for every admissible B. ∎ In full-support coordinates the +support condition is vacuous, so any certificate applies. + +### Lemma Z (frame zero patterns are combinatorial) + +Take a point frame (u₁, u₂, u₃) and the map p ↦ adj(U)p, where U is the matrix with columns u₁, u₂, u₃. +- Coordinate j of a point p vanishes iff p lies on the line u_k u_l. +- Coordinate j of a line ℓ (ℓ ↦ Uᵀℓ) vanishes iff u_j ∈ ℓ. + +Line frames are dual. Consider two realisations with the same incidences and the same extra collinear point triples and +concurrent line triples. They have the same zero pattern and the same zero set of p·ℓ in every frame. So a certificate +checked on the stored realisation applies to the whole class. (Short proof here; the verifier checks the finite inputs.) + +## Reproduce + +From the repository root (standard library, Python ≥ 3.10; about 1–2 min on a loaded 4-CPU machine): + +```sh +python3 -I -B research/three-total-classical-configs/verify.py +``` + +Expected: every line `PASS`, then +`counts {'CR2_certified': 2652, 'non_CR2_exact': 18, 'skipped': 70, ...}; min(cost - v) over the non-CR2 set: 1` +and `PASS_THREE_TOTAL_CLASSICAL_CONFIGS`. To replay the recorded enumall minima natively as well, run +`gcc -O2 -o /tmp/enumall research/three-total-classical-configs/c/enumall.c` and add `--enumall /tmp/enumall`. + +The verifier does the following: +- **Check 0:** hash pins. +- **Check 1:** exact configurations. +- **Check 2:** search-free check of all 372 frame certificates, with independent GF(2^k) arithmetic written in `verify.py`. +- **Check 3:** exclusions. It replays the DFS on a frame subset and runs the independent constructive Desargues count with + a positive control. +- **Check 4:** the sampled instances. +- **Check 5:** controls. + - `tied_min` (f = 72) must come out non-CR2 over GF(2/4/8). + - The #2162 six-line atom must be non-CR2 with pure-Python exhaustive minimum 6 = v. + - The stored #2162 GF(4) realisation of `cex_min_1` must pass the CR2 checker. + - **Negative controls** must be rejected: a corrupted certificate entry, a certificate checked against another frame, a + GF(4) certificate read over GF(8), a corrupted realisation, a zeroed realisation point, and a constant assignment for + `tied_min`. +- **Check 6:** special realisations and the Desargues no-extra-triple lemma. +- **Check 7:** the non-CR2 instances. It re-runs the exhaustive DFS and rechecks every witness. + +The task card asked for `tied_min` to come out "non-CR2 with exact minimum 12". Its f = 72 cannot be enumerated, so the +minimum 12 is inherited from #2111/#2162 (Theorem T′). The verifier checks non-CR2 and uses the six-line atom as the +enumerable tight control. + +Regeneration (not needed for verification; deterministic; run under `nice`): +- `scripts/universal_sweep.py` takes about 35 s. +- `scripts/sweep.py 600 BIN 2` is the instance sample. +- `scripts/special_sweep.py` takes about 10 s. +- `scripts/special_instances.py 2000 BIN 900` has a 900 s budget. Recorded run: all 2000 requested samples completed in 168 s, inside the budget. + +BIN is `c/enumall.c` compiled with `gcc -O2`. + +## Scope, inherited assumptions, unresolved obligations + +- **Inherited:** Lemma CR2 and the a = 0 2-adic corollary (#2162, open PR; its README reports a Lean check of the core + lemma, not re-reviewed here). The model and `enumall.c` come from #2111 (open PR). +- **Covered:** pairs are configuration points with configuration lines. Coordinates are structured frames (or full-support + coordinates). Realisations are as in item 2. Intersection points of non-configuration lines, mixed frames (except the one + above), Pappus realisations with signatures outside the grid, Reye 12_4 and D4 arrangements are **not** covered. +- **Finite certificate vs proof:** item 1 is a per-frame proof (Lemmas U and Z plus CR2) with stored, exactly checked + certificates. The field-size exclusions are exhaustive finite computations. Item 4 is a **bounded failed search** for + cost < v. It is not an impossibility theorem. The f > 26 non-CR2 instances are unresolved. +- Coverage of the Pappus special signatures depends on a parameter grid (a₂, b₁, b₂ ∈ [−15, 15]). The verifier checks the + necessary condition (extra triples ⊆ the three A_iB_iC_i and three line triples). Whether two extra point triples can + coexist over Q was not settled. + +## Open next questions + +1. **Do the f > 26 non-CR2 instances of the special Pappus frame also satisfy cost ≥ v + 1?** This matters because they are + the only open (A) instances from classical configurations found here. First step: run the #2162 Corollary J jet test, or + SAT via #2111 `satlib`, on the skipped records in `data/special_instances.json`. Blocker: 2^f enumeration is infeasible, + and jets can fail (jf0..2 of #2162). +2. **Mixed frames in general.** The single CR2 failure uses a coordinate triangle built from a non-configuration line and + point. Enumerate frames from the intersection points of the configuration's lines (and the joins of its points), then + rerun `universal_sweep`. This matters because zero-rich supports from such frames are where CR2 can fail. Blocker: the + frame count grows quickly; deduplicate by symmetry (S₅ for Desargues, order-108 group for Pappus). +3. **Reye 12_4 and the D4 arrangement** (the rest of OPEN ENDS item 4). The same frame-universal test applies. First step: + build exact realisations with `check_config`, then run `universal_sweep.py`. No blocker beyond implementation time. +4. **Why GF(16) for Desargues?** Is "no exact Desargues 10_3 in PG(2,8)" known, and does the forced degeneracy (centre on + axis) explain it? First step: a literature check, then a proof from the μ-parametrisation in `verify.py`. This matters + only for the size of certificates, not for (A). + +## Relation to the bottleneck + +Side result on the complex-supplier decoder sub-line. (A) at T = 3 limits what rank-3 root-unit decoders can save (#2111, +#2125). This package removes structured Desargues/Pappus realisations as counterexample candidates. It also locates one +zero-rich coordinate system where CR2 fails, and finds no counterexample there within a bounded search. κ is unchanged. + +## Credit + +DreamingOfClouds: #2111 (three-total model, `enumall.c`, `tied_min`, the Hesse X2 experiment, the OPEN ENDS handoff), +#2162 (Lemma CR2, `cr2.py`, CR2 realisations, the non-CR2 atoms) and #2125. #1590 (Lemma B). #446/#595 (cost model). +Adjacent audits: petalas #2193 (anti-Fano) and RossRichardson #2176 (jf0). Concurrent: a sibling session of the same +account works on the exact cost of `cex_min_1` (#2111 item 5), a different object, which this package does not use. + +Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). Apache-2.0. diff --git a/research/three-total-classical-configs/SOURCES.json b/research/three-total-classical-configs/SOURCES.json new file mode 100644 index 0000000000..392737aa2a --- /dev/null +++ b/research/three-total-classical-configs/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + } + ] +} diff --git a/research/three-total-classical-configs/TASK.json b/research/three-total-classical-configs/TASK.json new file mode 100644 index 0000000000..169c76e761 --- /dev/null +++ b/research/three-total-classical-configs/TASK.json @@ -0,0 +1,88 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Desargues 10_3 and Pappus 9_3 over Q in structured coordinates (three configuration points or lines as the coordinate triangle) as T=3 three-total decoder configurations: classify them by characteristic-2 realisability (Lemma CR2 of open PR #2162) and compute the exact minimum cost over all admissible B on the non-CR2 remainder (OPEN ENDS item 4 of the #2111 handoff, narrowed to Desargues and Pappus).", + "scope_change_reason": "The generic rank-shape card is crowded (#2151, #2124, #2130, #2145). The live, unclaimed handoff https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18932893 (item 4) names classical rich configurations as an untested class for the T=3 decoder floor (A) cost >= v, which limits what rank-3 root-unit decoders can save. A pre-experiment overlap check showed that the generic coordinate regime is already decided by #2162 Lemma CR2, so the task was narrowed to structured (support-restricted) coordinates.", + "bottleneck_link": "Side result on the complex-supplier decoder sub-line: (A) at T=3 bounds the savings of rank-3 root-unit decoders (#2111, #2125). Removing Desargues/Pappus structured realisations as counterexample candidates, and locating where CR2 fails, narrows the open part of (A). No kappa change.", + "budget_minutes": 90, + "stop_rule": "Searching stopped by 2026-10-15T00:34:36Z. Instances with f > 26 are skipped and counted. CR2 certificates are per-frame/per-instance proofs resting on #2162 Lemma CR2. \"No cost < v among non-CR2 instances\" is a bounded failed search, not a proof of (A). At most one evidence-driven pivot (none used; the frame-universal certificate refines the planned per-instance CR2 test).", + "outcome": "completed", + "evidence": "python3 -I -B research/three-total-classical-configs/verify.py prints PASS_THREE_TOTAL_CLASSICAL_CONFIGS. Frame-universal char-2 certificates exist for all 221 Desargues frames (GF(16); GF(2/4/8) excluded) and all 151 Pappus frames (GF(4)), and for all frames of 12 special Pappus signatures. Hence every structured decoder configuration built from them satisfies (A), conditional on CR2. One mixed coordinate system of a special Pappus realisation has no certificate. There, 88 of 2000 sampled instances are non-CR2; the 18 with f <= 26 have exact min(cost - v) = 1 and 70 are skipped. Independent constructive count: no exact Desargues 10_3 in PG(2,4) or PG(2,8).", + "author": "thakrarsagar", + "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) via Claude Code: design, code, computation and write-up, directed and submitted by thakrarsagar.", + "open_questions": [ + { + "question": "Do the 70 skipped (f > 26) non-CR2 instances of the special Pappus frame also satisfy cost >= v + 1?", + "why_it_matters": "They are the only open (A) instances from classical configurations found here.", + "first_step": "Run the #2162 Corollary J jet test, or SAT via the #2111 satlib, on the skipped records of data/special_instances.json.", + "blocked_by": "2^f enumeration is infeasible (f = 27..45), and jets can fail (jf0..2 of #2162)." + }, + { + "question": "Do mixed coordinate frames (triangles from intersection points of configuration lines, or joins of points) produce more non-CR2 instances, and any with cost < v or tight non-CR2 atoms?", + "why_it_matters": "The single CR2 failure found uses a coordinate triangle with a non-configuration line and point; zero-rich supports there are where (A) is genuinely open.", + "first_step": "Enumerate these frames up to the configuration symmetry group and rerun scripts/universal_sweep.py with the frame list extended.", + "blocked_by": "Frame count grows quickly; symmetry reduction (S5 for Desargues, order-108 group for Pappus) is not implemented." + }, + { + "question": "Do Reye 12_4 and the D4 line arrangement (the rest of OPEN ENDS item 4) admit frame-universal char-2 certificates in structured frames?", + "why_it_matters": "This would close the remaining classical-configuration part of the handoff item.", + "first_step": "Build exact integer realisations, check them with classical.check_config-style tests, then run the universal search.", + "blocked_by": "Implementation time only." + }, + { + "question": "Why does Desargues 10_3 need GF(16): is non-embeddability in PG(2,8) known, and is it explained by the forced degeneracy of one opposite point-line pair?", + "why_it_matters": "It affects only certificate size, not (A), but would give a human proof of the exclusion.", + "first_step": "Literature check, then a proof from the mu-parametrisation used in verify.py.", + "blocked_by": "Nothing known." + } + ] +} diff --git a/research/three-total-classical-configs/VERIFY.json b/research/three-total-classical-configs/VERIFY.json new file mode 100644 index 0000000000..6876ff3917 --- /dev/null +++ b/research/three-total-classical-configs/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Hash pins of the vendored #2162/#2111 files; exact Desargues/Pappus realisations; search-free check of 372 frame-universal char-2 certificates plus 1793 special-realisation certificates; replayed exhaustive exclusions and an independent constructive Desargues count with a positive control; 740 + 2000 sampled decoder configurations (CR2 rechecks; non-CR2 DFS re-run; witness costs; pure-Python exhaustion for f <= 18); controls tied_min, the six-line atom and cex_min_1; six negative controls that must be rejected." + } + ] +} diff --git a/research/three-total-classical-configs/c/enumall.c b/research/three-total-classical-configs/c/enumall.c new file mode 100644 index 0000000000..f05b16c846 --- /dev/null +++ b/research/three-total-classical-configs/c/enumall.c @@ -0,0 +1,28 @@ +// exhaustive: input v f; f lines "t s"; for j: nR R.., nA A..; optional slack k: output all B with cost<=min+k (we output cost too) +#include +#include +#include +int v,f,ft[64],fs[64],nR[3],nA[3],R[3][32],A[3][32]; +uint32_t row[32]; +static inline int rk(int j){uint32_t rows[32];int n=0; + for(int a=0;a>s&1)x|=1u<0 && (31-__builtin_clz(rows[k]))>(31-__builtin_clz(rows[k-1]));k--){uint32_t tmp=rows[k];rows[k]=rows[k-1];rows[k-1]=tmp;} + }} + return r;} +int main(int argc,char**argv){int slack=argc>1?atoi(argv[1]):0; + if(scanf("%d %d",&v,&f)!=2)return 1;for(int i=0;i> i & 1: + B[t][s] = 1 + return B + + +def odd_diagonal(P, Q): + """a = 0 case of #2162's 2-adic corollary: all primitive integer diagonal products odd => reduction mod 2 is a CR2 + realisation over GF(2).""" + return all(dot(prim(P[t]), prim(Q[t])) % 2 for t in range(len(P))) diff --git a/research/three-total-classical-configs/lib/cr2.py b/research/three-total-classical-configs/lib/cr2.py new file mode 100644 index 0000000000..bbe816583c --- /dev/null +++ b/research/three-total-classical-configs/lib/cr2.py @@ -0,0 +1,85 @@ +"""Char-2 realisability (CR2) of the incidence pattern used by an admissible B. +If points P~(t), lines Q~(s) over a field K of char 2 exist with supp P~(t) <= pi(t), supp Q~(s) <= sigma(s), +P~(t).Q~(s) = 0 for every off-diagonal B_ts = 1, P~(t).Q~(t) != 0, then +sum_j D(p~_j) B D(q~_j) = diag(P~(t).Q~(t)) has rank v over K, so cost(B) >= v (Hadamard argument of Lemma B, in char 2). +Exhaustive DFS over GF(2^k).""" +import itertools, sys +IRR = {1: 0b11, 2: 0b111, 3: 0b1011, 4: 0b10011, 5: 0b100101, 6: 0b1000011, 8: 0b100011011} +class GF: + def __init__(s, k): + s.k = k; s.q = 1 << k; m = IRR[k] + s.mul = [[0] * s.q for _ in range(s.q)] + for a in range(s.q): + for b in range(s.q): + r = 0; x = a; y = b + while y: + if y & 1: r ^= x + y >>= 1; x <<= 1 + if x & s.q: x ^= m + s.mul[a][b] = r + s.inv = [0] * s.q + for a in range(1, s.q): + for b in range(1, s.q): + if s.mul[a][b] == 1: s.inv[a] = b + def dot(s, a, b): + return s.mul[a[0]][b[0]] ^ s.mul[a[1]][b[1]] ^ s.mul[a[2]][b[2]] + +def proj_points(F, supp): + """normalised projective points with support inside supp (first nonzero = 1).""" + out = [] + for v in itertools.product(range(F.q), repeat=3): + if not any(v): continue + if any(v[j] and j not in supp for j in range(3)): continue + f = next(x for x in v if x) + if f != 1: continue + out.append(v) + return out + +def realise(pi, sig, E, k=2, limit=10**6, want_all=False): + """pi[t], sig[s]: allowed supports; E: set of (t,s) incidences required. Returns a realisation or None (exhaustive over GF(2^k)).""" + F = GF(k); v = len(pi) + cand = {('p', t): proj_points(F, pi[t]) for t in range(v)} + cand.update({('l', s): proj_points(F, sig[s]) for s in range(v)}) + nb = {x: [] for x in cand} + for (t, s) in E: + nb[('p', t)].append(('l', s)); nb[('l', s)].append(('p', t)) + other = {('p', t): ('l', t) for t in range(v)}; other.update({('l', t): ('p', t) for t in range(v)}) + asg = {}; nodes = [0] + def ok(x, val): + for y in nb[x]: + if y in asg and F.dot(val, asg[y]) != 0: return False + y = other[x] + if y in asg and F.dot(val, asg[y]) == 0: return False + return True + def pick(): + best = None; bc = None + for x in cand: + if x in asg: continue + c = [val for val in cand[x] if ok(x, val)] + if bc is None or len(c) < len(bc): + best, bc = x, c + if len(c) <= 1: break + return best, bc + sols = [] + def dfs(): + nodes[0] += 1 + if nodes[0] > limit: raise TimeoutError + if len(asg) == len(cand): + sols.append(dict(asg)); return not want_all + x, c = pick() + for val in c: + asg[x] = val + if dfs(): return True + del asg[x] + return False + try: + dfs() + except TimeoutError: + return 'timeout' + return sols if want_all else (sols[0] if sols else None) + +def cfg_data(P, Q): + v = len(P) + pi = [{j for j in range(3) if P[t][j]} for t in range(v)] + sig = [{j for j in range(3) if Q[t][j]} for t in range(v)] + return pi, sig diff --git a/research/three-total-classical-configs/lib/universal.py b/research/three-total-classical-configs/lib/universal.py new file mode 100644 index 0000000000..7d794d5be4 --- /dev/null +++ b/research/three-total-classical-configs/lib/universal.py @@ -0,0 +1,118 @@ +"""Frame-universal char-2 realisation (written for this package). + +Given a configuration over Q in frame coordinates (points P[i], lines L[k], primitive integer vectors), search GF(2^k) +for X[i], Y[k] (projective, first nonzero coordinate 1) with + supp X[i] <= supp P[i], supp Y[k] <= supp L[k], + X[i].Y[k] = 0 whenever P[i].L[k] = 0, X[i].Y[k] != 0 whenever P[i].L[k] != 0. +Such an (X, Y) gives, for EVERY decoder configuration whose pairs are (P[i], L[k]) with P[i].L[k] != 0 (any v, repetitions +allowed), the assignment P~(t) = X[point(t)], Q~(t) = Y[line(t)], which satisfies the hypotheses of Lemma CR2 of #2162 +(supports, every in-block incidence, nonzero diagonal); hence cost(B) >= v for every admissible B (conditional on CR2). +Exhaustive MRV depth-first search with forward checking; returns a dict, None (exhausted: no realisation), or 'timeout'. +""" +import itertools + +IRR = {1: 0b11, 2: 0b111, 3: 0b1011, 4: 0b10011, 5: 0b100101} + + +def gf_tables(k): + q = 1 << k; m = IRR[k] + mul = [[0] * q for _ in range(q)] + for a in range(q): + for b in range(q): + r = 0; x = a; y = b + while y: + if y & 1: + r ^= x + y >>= 1; x <<= 1 + if x & q: + x ^= m + mul[a][b] = r + return mul + + +def gdot(mul, a, b): + return mul[a[0]][b[0]] ^ mul[a[1]][b[1]] ^ mul[a[2]][b[2]] + + +def domain(q, supp): + out = [] + for v in itertools.product(range(q), repeat=3): + if not any(v) or any(v[j] and j not in supp for j in range(3)): + continue + if next(x for x in v if x) != 1: + continue + out.append(v) + return out + + +def universal_realise(P, L, k, limit=10 ** 6, relax=()): + """relax: (point, line) index pairs left unconstrained (used only for the obstruction analysis).""" + q = 1 << k; mul = gf_tables(k) + n_p, n_l = len(P), len(L) + var = [('p', i) for i in range(n_p)] + [('l', j) for j in range(n_l)] + supp = {('p', i): {j for j in range(3) if P[i][j]} for i in range(n_p)} + supp.update({('l', j): {c for c in range(3) if L[j][c]} for j in range(n_l)}) + dom = {x: domain(q, supp[x]) for x in var} + zero = {} + for i in range(n_p): + for j in range(n_l): + z = sum(a * b for a, b in zip(P[i], L[j])) == 0 + if (i, j) in relax: + z = None + zero[(('p', i), ('l', j))] = z; zero[(('l', j), ('p', i))] = z + nbrs = {x: [y for y in var if y[0] != x[0]] for x in var} + asg = {}; nodes = [0] + + def dfs(doms): + nodes[0] += 1 + if nodes[0] > limit: + raise TimeoutError + free = [x for x in var if x not in asg] + if not free: + return True + best = min(free, key=lambda x: len(doms[x])) + for val in doms[best]: + new = dict(doms); ok = True + for y in nbrs[best]: + if y in asg: + continue + z = zero[(best, y)] + if z is None: + continue + c = [w for w in doms[y] if (gdot(mul, val, w) == 0) == z] + if not c: + ok = False; break + new[y] = c + if not ok: + continue + asg[best] = val + if dfs(new): + return True + del asg[best] + return False + try: + ok = dfs(dom) + except TimeoutError: + return 'timeout' + if not ok: + return None + return dict(X=[list(asg[('p', i)]) for i in range(n_p)], Y=[list(asg[('l', j)]) for j in range(n_l)], nodes=nodes[0]) + + +def check_universal(P, L, k, X, Y): + """Exact, search-free verification of a stored frame-universal realisation.""" + q = 1 << k; mul = gf_tables(k) + for V, W in ((X, P), (Y, L)): + if len(V) != len(W): + return False + for a, b in zip(V, W): + if len(a) != 3 or not any(a) or any(not (0 <= x < q) for x in a): + return False + if any(a[j] and not b[j] for j in range(3)): + return False + for i in range(len(P)): + for j in range(len(L)): + z = sum(a * b for a, b in zip(P[i], L[j])) == 0 + if z != (gdot(mul, X[i], Y[j]) == 0): + return False + return True diff --git a/research/three-total-classical-configs/scripts/special_instances.py b/research/three-total-classical-configs/scripts/special_instances.py new file mode 100644 index 0000000000..77f1189118 --- /dev/null +++ b/research/three-total-classical-configs/scripts/special_instances.py @@ -0,0 +1,45 @@ +"""Per-instance CR2 classification on the one coordinate system without a frame-universal certificate (data/special.json: +Pappus realisation with A0B0C0 collinear and l, m, pap concurrent, identity coordinates). Samples decoder configurations +(v = 6..10, RNG seed 22, incidence-biased as in scripts/sweep.py), classifies them with the a = 0 2-adic test and the +vendored cr2.py DFS over GF(2), GF(4), GF(8); non-CR2 instances with f <= 26 get the exact minimum over all 2^f admissible +B from the vendored enumall (writes data/special_instances.json). + +usage: python3 -I -B scripts/special_instances.py N_SAMPLES ENUMALL_BINARY SECONDS_BUDGET +""" +import json, os, random, sys, time +PKG = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) +sys.path.insert(0, os.path.join(PKG, 'lib')); sys.path.insert(0, os.path.join(PKG, 'scripts')) +from sweep import sample_pairs, classify + + +def main(): + N = int(sys.argv[1]); binary = sys.argv[2]; budget = float(sys.argv[3]); t0 = time.time() + S = json.load(open(os.path.join(PKG, 'data', 'special.json'))) + tgt = [r for r in S['configs']['pappus']['realisations'] if any(f['k'] is None for f in r['frames'])] + assert len(tgt) == 1 and [f['frame'] for f in tgt[0]['frames'] if f['k'] is None] == [['I']] + P2 = [tuple(p) for p in tgt[0]['points']]; L2 = [tuple(l) for l in tgt[0]['lines']] + rng = random.Random(22); seen = set(); out = dict(seed=22, params=tgt[0]['params'], n_requested=N, instances=[]) + for rep in range(N): + if time.time() - t0 > budget: + break + v = 6 + (rep % 5); expo = 1 + rng.randrange(4) + pairs = sample_pairs(P2, L2, v, rng, expo) + key = frozenset(pairs) + if key in seen: + continue + seen.add(key) + P = [list(P2[i]) for (i, k) in pairs]; Q = [list(L2[k]) for (i, k) in pairs] + rec = dict(pairs=[list(x) for x in pairs], expo=expo); rec.update(classify(P, Q, binary)) + out['instances'].append(rec) + out['elapsed_s'] = round(time.time() - t0, 1); out['attempts'] = rep + 1 + json.dump(out, open(os.path.join(PKG, 'data', 'special_instances.json'), 'w'), separators=(',', ':')) + from collections import Counter + print('instances', len(out['instances']), 'elapsed', out['elapsed_s']) + print(Counter((r['status'], r.get('via', r.get('exact'))) for r in out['instances'])) + nc = [r for r in out['instances'] if r['status'] == 'nonCR2' and 'min' in r] + print('non-CR2 exact:', len(nc), 'min(cost - v):', min((r['min'] - r['v'] for r in nc), default=None)) + print(sorted(Counter((r['v'], r['f'], r['min']) for r in nc).items())) + + +if __name__ == '__main__': + main() diff --git a/research/three-total-classical-configs/scripts/special_sweep.py b/research/three-total-classical-configs/scripts/special_sweep.py new file mode 100644 index 0000000000..f6e8df94de --- /dev/null +++ b/research/three-total-classical-configs/scripts/special_sweep.py @@ -0,0 +1,81 @@ +"""Special (zero-richer) realisations: Desargues / Pappus realisations over Z with exactly the configuration incidences but +EXTRA collinear point triples or concurrent line triples (so frame coordinates have extra zeros). Small-integer parameter +grid (fixed order, no randomness); one realisation per distinct extra-triple signature, at most MAXSIG per configuration; +frame-universal char-2 search over GF(2^k), k = 1..4, in every frame (writes data/special.json). + +usage: python3 -I -B scripts/special_sweep.py +""" +import itertools, json, os, sys, time +PKG = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) +sys.path.insert(0, os.path.join(PKG, 'lib')) +from classical import pappus, desargues, check_config, frames, transform, det3 +from universal import universal_realise, check_universal + +MAXSIG = 20; LIMIT = 200000; R = range(-3, 4) + + +def extras(C, n): + pts, lines = C['points'], C['lines']; inc = {tuple(x) for x in C['incidences']}; pn, ln = C['pnames'], C['lnames'] + ec = [t for t in itertools.combinations(range(n), 3) if det3(*[pts[i] for i in t]) == 0 + and not any(all((pn[i], ln[l]) in inc for i in t) for l in range(n))] + el = [t for t in itertools.combinations(range(n), 3) if det3(*[lines[i] for i in t]) == 0 + and not any(all((pn[p], ln[l]) in inc for l in t) for p in range(n))] + return tuple(ec), tuple(el) + + +def candidates(name): + if name == 'desargues': + for x, y in itertools.product(R, R): + for lam in itertools.product([l for l in R if l], repeat=3): + yield dict(a=((1, 0, 1), (0, 1, 1), (x, y, 1)), lam=lam) + else: + for a2, b1, b2 in itertools.product(range(-15, 16), range(-15, 16), range(-15, 16)): + if a2 in (0, 1): + continue + yield dict(a=(0, 1, a2), b=(0, b1, b2)) + + +def main(): + t0 = time.time(); out = dict(limit=LIMIT, maxsig=MAXSIG, configs={}) + for name, n, mk in [('desargues', 10, desargues), ('pappus', 9, pappus)]: + sigs = {}; scanned = 0 + for par in candidates(name): + scanned += 1 + try: + C = mk(**par) + except AssertionError: + continue + if not check_config(C, n, 3): + continue + ex = extras(C, n) + if (ex[0] or ex[1]) and ex not in sigs and len(sigs) < MAXSIG: + sigs[ex] = (par, C) + recs = [] + for ex, (par, C) in sigs.items(): + fr_res = []; worst = 0 + for fr in [('I',)] + frames(C): + P2, L2 = (C['points'], C['lines']) if fr == ('I',) else transform(C, fr) + got = None + for k in (1, 2, 3, 4): + r = universal_realise(P2, L2, k, limit=LIMIT) + if isinstance(r, dict): + assert check_universal(P2, L2, k, r['X'], r['Y']) + got = dict(frame=list(fr), k=k, X=r['X'], Y=r['Y']); break + if r == 'timeout': + got = dict(frame=list(fr), k=None, timeout=k); break + if got is None: + got = dict(frame=list(fr), k=None, excluded_upto=4) + fr_res.append(got); worst = max(worst, got['k'] or 99) + recs.append(dict(params={k: list(v) if isinstance(v, tuple) else v for k, v in par.items()}, + points=[list(p) for p in C['points']], lines=[list(l) for l in C['lines']], + extra_point_triples=[list(t) for t in ex[0]], extra_line_triples=[list(t) for t in ex[1]], + frames=fr_res)) + print(name, 'extra', ex, 'frames', len(fr_res), 'k-dist', + sorted({(x['k'] if x['k'] else 'none') for x in fr_res}, key=str), '%.1fs' % (time.time() - t0), flush=True) + out['configs'][name] = dict(scanned=scanned, signatures=len(sigs), realisations=recs) + out['elapsed_s'] = round(time.time() - t0, 1) + json.dump(out, open(os.path.join(PKG, 'data', 'special.json'), 'w'), separators=(',', ':')) + + +if __name__ == '__main__': + main() diff --git a/research/three-total-classical-configs/scripts/sweep.py b/research/three-total-classical-configs/scripts/sweep.py new file mode 100644 index 0000000000..4bdd062751 --- /dev/null +++ b/research/three-total-classical-configs/scripts/sweep.py @@ -0,0 +1,120 @@ +"""Bounded sweep (writes data/instances.json): structured-coordinate Pappus / Desargues decoder configurations, +CR2 classification (a = 0 2-adic test, then exhaustive support-compatible DFS over GF(2), GF(4), GF(8) with the vendored +#2162 lib/cr2.py), and the exact minimum over all 2^f admissible B (vendored #2111 enumall.c) for non-CR2 instances only. + +usage: python3 -I -B scripts/sweep.py SECONDS_BUDGET ENUMALL_BINARY [PER_FRAME] +(recorded run: budget 600, PER_FRAME 2; instance coordinates are recomputed from frame + pairs, not stored) +RNG seed 22. Frames are visited in a fixed order; the stopping rule is the time budget (recorded in the output). +""" +import json, os, random, subprocess, sys, time +PKG = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) +sys.path.insert(0, os.path.join(PKG, 'lib')) +from classical import (pappus, desargues, check_config, frames, transform, setup, dot, odd_diagonal, cost_of, tomat) +from cr2 import realise, cfg_data + +SEED = 22 +FMAX = 26 +DFS_LIMIT = 200000 + + +def overlap(a, b): + return any(a[j] and b[j] for j in range(3)) + + +def sample_pairs(P2, L2, v, rng, expo): + n_p, n_l = len(P2), len(L2) + cand = [(i, k) for i in range(n_p) for k in range(n_l) if dot(P2[i], L2[k]) != 0] + chosen = [] + while len(chosen) < v: + opts, wts = [], [] + for (i, k) in cand: + if (i, k) in chosen: + continue + sc = sum(1 for (i2, k2) in chosen if dot(P2[i], L2[k2]) == 0 and overlap(P2[i], L2[k2])) + sc += sum(1 for (i2, k2) in chosen if dot(P2[i2], L2[k]) == 0 and overlap(P2[i2], L2[k])) + opts.append((i, k)); wts.append((1 + sc) ** expo) + chosen.append(rng.choices(opts, weights=wts)[0]) + return chosen + + +def enumall(binary, v, R, A, free): + inp = "%d %d\n" % (v, len(free)) + "".join("%d %d\n" % e for e in free) + \ + "".join("%d %s\n%d %s\n" % (len(R[j]), " ".join(map(str, R[j])), len(A[j]), " ".join(map(str, A[j]))) for j in range(3)) + out = subprocess.run([binary, '0'], input=inp, capture_output=True, text=True, check=True, timeout=600).stdout.split() + best, nm = int(out[0]), int(out[1]) + return best, nm, int(out[3]) # first minimiser's mask g + + +def classify(P, Q, binary): + v = len(P) + R, A, free = setup(P, Q) + rec = dict(v=v, f=len(free)) + if odd_diagonal(P, Q): + rec['status'] = 'CR2'; rec['via'] = '2adic-a0'; return rec + pi, sig = cfg_data(P, Q) + timeouts = [] + for k in (1, 2, 3): + r = realise(pi, sig, set(free), k=k, limit=DFS_LIMIT) + if isinstance(r, dict): + rec['status'] = 'CR2'; rec['via'] = 'dfs'; rec['k'] = k + rec['Pt'] = [list(r[('p', t)]) for t in range(v)]; rec['Qt'] = [list(r[('l', t)]) for t in range(v)] + return rec + if r == 'timeout': + timeouts.append(k) + if timeouts: + rec['status'] = 'undecided'; rec['dfs_timeout_k'] = timeouts; return rec + rec['status'] = 'nonCR2' + if len(free) > FMAX: + rec['exact'] = 'skipped-f'; return rec + best, nm, g = enumall(binary, v, R, A, free) + c = cost_of(P, Q, tomat(g, free, v)) + assert c == best, (c, best) + rec['exact'] = 'enumall'; rec['min'] = best; rec['nmin'] = nm; rec['witness_g'] = g + return rec + + +def main(): + budget = float(sys.argv[1]); binary = sys.argv[2]; per_frame = int(sys.argv[3]) if len(sys.argv) > 3 else 6 + t0 = time.time(); rng = random.Random(SEED) + confs = [(desargues(), 10), (pappus(), 9)] + for C, n in confs: + assert check_config(C, n, 3), C['name'] + out = dict(seed=SEED, fmax=FMAX, dfs_limit=DFS_LIMIT, per_frame=per_frame, budget_s=budget, configs={}, instances=[]) + for C, n in confs: + out['configs'][C['name']] = dict(points=[list(p) for p in C['points']], pnames=C['pnames'], + lines=[list(l) for l in C['lines']], lnames=C['lnames'], incidences=C['incidences']) + seen = set(); stopped = False; frames_done = {} + # interleave: Desargues frames first (primary), then Pappus, round-robin by v + for C, n in confs: + frs = frames(C); frames_done[C['name']] = [0, len(frs)] + for fr in frs: + if time.time() - t0 > budget: + stopped = True; break + P2, L2 = transform(C, fr) + for rep in range(per_frame): + v = 6 + (rep % 5) + expo = 1 + rng.randrange(3) + pairs = sample_pairs(P2, L2, v, rng, expo) + key = (C['name'], fr, frozenset(pairs)) + if key in seen: + continue + seen.add(key) + P = [list(P2[i]) for (i, k) in pairs]; Q = [list(L2[k]) for (i, k) in pairs] + rec = dict(config=C['name'], frame=list(fr), pairs=[list(x) for x in pairs], expo=expo) + rec.update(classify(P, Q, binary)) + out['instances'].append(rec) + frames_done[C['name']][0] += 1 + if stopped: + break + out['frames_done'] = frames_done; out['stopped_by_budget'] = stopped; out['elapsed_s'] = round(time.time() - t0, 1) + json.dump(out, open(os.path.join(PKG, 'data', 'instances.json'), 'w'), separators=(',', ':')) + from collections import Counter + print('frames', frames_done, 'stopped', stopped, 'elapsed', out['elapsed_s']) + print(Counter((r['config'], r['status'], r.get('via', r.get('exact'))) for r in out['instances'])) + nc = [r for r in out['instances'] if r['status'] == 'nonCR2' and 'min' in r] + if nc: + print('min(cost - v) over non-CR2 exact:', min(r['min'] - r['v'] for r in nc)) + + +if __name__ == '__main__': + main() diff --git a/research/three-total-classical-configs/scripts/universal_sweep.py b/research/three-total-classical-configs/scripts/universal_sweep.py new file mode 100644 index 0000000000..4bb88a4ae4 --- /dev/null +++ b/research/three-total-classical-configs/scripts/universal_sweep.py @@ -0,0 +1,47 @@ +"""Frame-universal CR2 certificates (writes data/universal.json). + +For each configuration (Desargues 10_3, Pappus 9_3) and each structured frame (three non-collinear configuration points sent +to e_1, e_2, e_3, or three non-concurrent configuration lines sent to the coordinate lines), plus the identity frame of the +base realisation, search GF(2^k), k = 1..4 in order, for a frame-universal char-2 realisation (lib/universal.py). +For the identity frame, and for one frame per configuration, also record which k are exhaustively excluded. + +usage: python3 -I -B scripts/universal_sweep.py +""" +import json, os, sys, time +PKG = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) +sys.path.insert(0, os.path.join(PKG, 'lib')) +from classical import pappus, desargues, check_config, frames, transform +from universal import universal_realise, check_universal + +LIMIT = 200000 + + +def main(): + out = dict(limit=LIMIT, configs={}) + t0 = time.time() + for C, n in [(desargues(), 10), (pappus(), 9)]: + assert check_config(C, n, 3) + recs = [] + for fr in [('I',)] + frames(C): + if fr == ('I',): + P2, L2 = C['points'], C['lines'] + else: + P2, L2 = transform(C, fr) + rec = dict(frame=list(fr), P=[list(p) for p in P2], L=[list(l) for l in L2], excluded=[], timeout=[]) + for k in (1, 2, 3, 4): + r = universal_realise(P2, L2, k, limit=LIMIT) + if isinstance(r, dict): + assert check_universal(P2, L2, k, r['X'], r['Y']) + rec.update(k=k, X=r['X'], Y=r['Y']) + break + (rec['excluded'] if r is None else rec['timeout']).append(k) + recs.append(rec) + print(C['name'], fr, 'k=%s' % rec.get('k'), 'excluded', rec['excluded'], 'timeout', rec['timeout'], + '%.1fs' % (time.time() - t0), flush=True) + out['configs'][C['name']] = recs + out['elapsed_s'] = round(time.time() - t0, 1) + json.dump(out, open(os.path.join(PKG, 'data', 'universal.json'), 'w'), separators=(',', ':')) + + +if __name__ == '__main__': + main() diff --git a/research/three-total-classical-configs/verify.py b/research/three-total-classical-configs/verify.py new file mode 100644 index 0000000000..7c52212c13 --- /dev/null +++ b/research/three-total-classical-configs/verify.py @@ -0,0 +1,293 @@ +"""Replay for research/three-total-classical-configs (standard library only; about 60 s, about 3 min with --enumall). + +usage: python3 -I -B research/three-total-classical-configs/verify.py [--enumall PATH_TO_COMPILED_c/enumall.c] +Prints one PASS/FAIL line per check and a final PASS_THREE_TOTAL_CLASSICAL_CONFIGS line; exit status 1 on any failure. +All acceptance checks are exact (integers and GF(2^k) bitmask arithmetic). The search-free certificate checker and the +constructive Desargues count below are written here and do not import lib/universal.py. +""" +import hashlib, itertools, json, os, sys, time + +PKG = os.path.dirname(os.path.abspath(__file__)) +sys.path.insert(0, os.path.join(PKG, 'lib')) +from classical import (pappus, desargues, check_config, frames, transform, setup, dot, det3, odd_diagonal, + cost_of, tomat) +from cr2 import realise, cfg_data # vendored from #2162 (DFS used for per-instance cross-checks) +from universal import universal_realise # used only to replay the exhaustive exclusions + +BAD = [0]; T0 = time.time() +ENUMALL = sys.argv[sys.argv.index('--enumall') + 1] if '--enumall' in sys.argv else None # optional native replay + + +def report(name, ok, msg=''): + print('%s %s %s' % ('PASS' if ok else 'FAIL', name, msg), flush=True) + if not ok: + BAD[0] += 1 + + +# ---------- independent GF(2^k) arithmetic ---------- +POLY = {1: 0b11, 2: 0b111, 3: 0b1011, 4: 0b10011} + + +def gmul(a, b, k): + r = 0 + while b: + if b & 1: + r ^= a + b >>= 1; a <<= 1 + if a >> k & 1: + a ^= POLY[k] + return r + + +def gdot(a, b, k): + return gmul(a[0], b[0], k) ^ gmul(a[1], b[1], k) ^ gmul(a[2], b[2], k) + + +def gcross(a, b, k): + return (gmul(a[1], b[2], k) ^ gmul(a[2], b[1], k), gmul(a[2], b[0], k) ^ gmul(a[0], b[2], k), + gmul(a[0], b[1], k) ^ gmul(a[1], b[0], k)) + + +def supp_ok(V, W, k): + return len(V) == 3 and any(V) and all(0 <= x < (1 << k) for x in V) and all(W[j] or not V[j] for j in range(3)) + + +def universal_ok(P, L, k, X, Y): + """Frame-universal certificate: supports shrink, and X[i].Y[j] == 0 over GF(2^k) iff P[i].L[j] == 0 over Z.""" + if len(X) != len(P) or len(Y) != len(L): + return False + if not all(supp_ok(a, b, k) for a, b in zip(X, P)) or not all(supp_ok(a, b, k) for a, b in zip(Y, L)): + return False + return all((dot(P[i], L[j]) == 0) == (gdot(X[i], Y[j], k) == 0) for i in range(len(P)) for j in range(len(L))) + + +def cr2_hyp_ok(P, Q, k, Pt, Qt): + """Hypotheses of #2162 Lemma CR2 for one decoder configuration: supports, every in-block incidence, nonzero diagonal.""" + v = len(P); R, A, free = setup(P, Q) + if len(Pt) != v or len(Qt) != v: + return False + if not all(supp_ok(Pt[t], P[t], k) and supp_ok(Qt[t], Q[t], k) for t in range(v)): + return False + return all(gdot(Pt[t], Qt[s], k) == 0 for (t, s) in free) and all(gdot(Pt[t], Qt[t], k) != 0 for t in range(v)) + + +def desargues_exact_count(k, a2_choices=None): + """Constructive, exhaustive: Desargues 10_3 realisations over GF(2^k) with O, a0, a1 = e1, e2, e3 (WLOG by PGL(3): + O, a0, a1 are non-collinear in any exact realisation). Every point of line O a_i other than O, a_i is a_i + mu_i O with + mu_i != 0; c_ij = a_ia_j x b_ib_j and axis = c01 x c02 are forced. Counts the choices whose point-line incidence + relation equals the combinatorial 10_3 incidences exactly.""" + q = 1 << k + C = desargues(); pn, ln = C['pnames'], C['lnames'] + want = {(pn.index(p), ln.index(l)) for (p, l) in C['incidences']} + O, a0, a1 = (1, 0, 0), (0, 1, 0), (0, 0, 1) + allpts = [v for v in itertools.product(range(q), repeat=3) if any(v) and next(x for x in v if x) == 1] + prs = [(0, 1), (0, 2), (1, 2)] + cnt = 0 + for a2 in (a2_choices or allpts): + A = [a0, a1, tuple(a2)] + for mu in itertools.product(range(1, q), repeat=3): + B = [(A[i][0] ^ mu[i], A[i][1], A[i][2]) for i in range(3)] + c = [gcross(gcross(A[i], A[j], k), gcross(B[i], B[j], k), k) for (i, j) in prs] + pts = [O] + A + B + c + lines = [gcross(A[i], B[i], k) for i in range(3)] + [gcross(A[i], A[j], k) for (i, j) in prs] + \ + [gcross(B[i], B[j], k) for (i, j) in prs] + [gcross(c[0], c[1], k)] + if not all(any(x) for x in pts + lines): + continue + got = {(i, j) for i in range(10) for j in range(10) if gdot(pts[i], lines[j], k) == 0} + cnt += got == want + return cnt + + +def main(): + # 0. manifest + bad = [] + for line in open(os.path.join(PKG, 'MANIFEST.sha256')): + h, p = line.split() + if hashlib.sha256(open(os.path.join(PKG, p), 'rb').read()).hexdigest() != h: + bad.append(p) + PINS = {'lib/cr2.py': 'ff3c1bbd072c4d1f47158f903aa3ff4fcd8db5bbc4709c3d15b21a1815eef3bd', # #2162 MANIFEST.sha256 + 'c/enumall.c': '55d864202535c22952e1a9080ad834f1908d18ff857c8dc26211e25a847d1fc8', # = #2111 c/enumall.c + 'data/tied_min.json': '670ed90924b601ade22f0d4adaff46d1667e5449326a0f7ba7b88dd8f5906f93', + 'data/cex_min_1.json': '86064701dde94b4f35427bc3e19275eaf1e40e9e90d4fea28e7857f3564d4dd7', + 'data/tm_noncr2.json': 'b5aa8ca01a87a898ae27160d5274af7ff08127cf0b27cf372f73a5725cd216a5', + 'data/cr2_realisations.json': '2ce114152529d375215f1f64a45072c9b78d1719d156e76bc692eff1fa955666'} + bad += [p for p, h in PINS.items() if hashlib.sha256(open(os.path.join(PKG, p), 'rb').read()).hexdigest() != h] + report('0 MANIFEST.sha256, and vendored lib/cr2.py, c/enumall.c and copied data match the #2162 head 113a7182 pins', not bad, str(bad)) + + # 1. configurations + confs = [(desargues(), 10), (pappus(), 9)] + for C, n in confs: + pts, lines = C['points'], C['lines']; inc = {tuple(x) for x in C['incidences']} + pn, ln = C['pnames'], C['lnames'] + on = lambda tri: any(all((pn[i], ln[l]) in inc for i in tri) for l in range(n)) + at = lambda tri: any(all((pn[p], ln[l]) in inc for l in tri) for p in range(n)) + ec = [t for t in itertools.combinations(range(n), 3) if det3(*[pts[i] for i in t]) == 0 and not on(t)] + el = [t for t in itertools.combinations(range(n), 3) if det3(*[lines[i] for i in t]) == 0 and not at(t)] + report('1 %s %d_3 over Z: exactly the %d configuration incidences, no extra collinear point / concurrent line triples' + % (C['name'], n, 3 * n), check_config(C, n, 3) and not ec and not el) + + # 2. frame-universal certificates (search-free check) + U = json.load(open(os.path.join(PKG, 'data', 'universal.json'))) + kwant = {'desargues': 4, 'pappus': 2}; nframes = {} + for C, n in confs: + recs = U['configs'][C['name']]; frs = [('I',)] + frames(C) + ok = [tuple(r['frame']) for r in recs] == frs; ks = set() + for r, fr in zip(recs, frs): + P2, L2 = (C['points'], C['lines']) if fr == ('I',) else transform(C, fr) + ok &= [list(p) for p in P2] == r['P'] and [list(l) for l in L2] == r['L'] + ok &= 'k' in r and universal_ok(P2, L2, r['k'], r['X'], r['Y']); ks.add(r.get('k')) + nframes[C['name']] = len(recs) + report('2 %s: all %d frames (identity + %d point/line coordinate triangles) carry a frame-universal char-2 ' + 'realisation over GF(%d)' % (C['name'], len(recs), len(recs) - 1, 1 << kwant[C['name']]), + ok and ks == {kwant[C['name']]}) + + # 3. exclusions (smaller fields): recorded for every frame, DFS replay on a fixed subset, independent constructive count + for C, n in confs: + recs = U['configs'][C['name']]; sub = recs[::15]; ok = True + for r in sub: + for k in r['excluded']: + ok &= universal_realise(r['P'], r['L'], k, limit=200000) is None + allex = all(r['excluded'] == list(range(1, kwant[C['name']])) and not r['timeout'] for r in recs) + report('3 %s: frame-universal realisation exhaustively excluded over GF(2^k), k < %d, in every frame (recorded); ' + 'DFS replay on %d frames' % (C['name'], kwant[C['name']], len(sub)), ok and allex) + c4, c8 = desargues_exact_count(2), desargues_exact_count(3) + report('3 Desargues 10_3, independent constructive count: no exact realisation in PG(2,4) or PG(2,8)', c4 == 0 and c8 == 0, + 'counts %d, %d' % (c4, c8)) + r = next(x for x in U['configs']['desargues'] if x['frame'] == ['P', 0, 1, 2]) + c16 = desargues_exact_count(4, a2_choices=[r['X'][3]]) + report('3 positive control: the constructive count finds exact PG(2,16) realisations (a2 fixed to the stored one)', c16 > 0, + 'count %d' % c16) + + # 4. sampled instances: universal certificate applied per instance + stored per-instance cr2.py results + I = json.load(open(os.path.join(PKG, 'data', 'instances.json'))) + cache = {}; n_cert = n_dfs = n_2adic = skipped = 0; nonCR2 = []; okall = True; fs = [] + byname = {C['name']: C for C, n in confs} + ucert = {c: {tuple(r['frame']): r for r in U['configs'][c]} for c in U['configs']} + for rec in I['instances']: + C = byname[rec['config']]; fr = tuple(rec['frame']) + if (C['name'], fr) not in cache: + cache[(C['name'], fr)] = transform(C, fr) + P2, L2 = cache[(C['name'], fr)] + P = [P2[i] for i, k in rec['pairs']]; Q = [L2[k] for i, k in rec['pairs']] + f = len(setup(P, Q)[2]); fs.append(f) + okall &= all(dot(p, q) != 0 for p, q in zip(P, Q)) and 6 <= len(P) <= 10 and f == rec['f'] and len(P) == rec['v'] + u = ucert[C['name']][fr] + Pt = [u['X'][i] for i, k in rec['pairs']]; Qt = [u['Y'][k] for i, k in rec['pairs']] + uok = cr2_hyp_ok(P, Q, u['k'], Pt, Qt); okall &= uok; n_cert += uok + if rec['status'] == 'CR2' and rec['via'] == 'dfs': + okall &= cr2_hyp_ok(P, Q, rec['k'], rec['Pt'], rec['Qt']); n_dfs += 1 + elif rec['status'] == 'CR2' and rec['via'] == '2adic-a0': + okall &= odd_diagonal(P, Q); n_2adic += 1 + else: + nonCR2.append(rec); skipped += rec.get('exact') == 'skipped-f' + report('4 %d sampled decoder configurations (v = 6..10, f = %d..%d, seed %d): Lemma CR2 hypotheses hold via the ' + 'frame-universal certificate; independent per-instance cross-check: %d by the vendored cr2.py DFS, %d by the a = 0 ' + '2-adic test' % (len(I['instances']), min(fs), max(fs), I['seed'], n_dfs, n_2adic), + okall and n_cert == len(I['instances']) and not nonCR2) + + # 5. controls + T = json.load(open(os.path.join(PKG, 'data', 'tied_min.json'))); Pm = [l[0] for l in T]; Qm = [l[1] for l in T] + R, A, free = setup(Pm, Qm); pi, sig = cfg_data(Pm, Qm) + res = [realise(pi, sig, set(free), k=k) for k in (1, 2, 3)] + report('5 control tied_min (#2111): NOT CR2 over GF(2), GF(4), GF(8) (exhaustive DFS), f = %d' % len(free), + all(x is None for x in res) and len(free) == 72) + S = (0, 1, 2, 3, 8, 10); P6 = [Pm[i] for i in S]; Q6 = [Qm[i] for i in S]; R, A, free = setup(P6, Q6); pi, sig = cfg_data(P6, Q6) + res = [realise(pi, sig, set(free), k=k) for k in (1, 2, 3)] + best = min(cost_of(P6, Q6, tomat(g, free, 6)) for g in range(1 << len(free))) + report('5 control: six-line atom %s of tied_min (#2162): NOT CR2, and pure-Python exhaustive min over 2^%d admissible B ' + '= 6 = v (tight)' % (list(S), len(free)), all(x is None for x in res) and best == 6) + D = json.load(open(os.path.join(PKG, 'data', 'cr2_realisations.json')))['cex_min_1'] + X = json.load(open(os.path.join(PKG, 'data', 'cex_min_1.json'))); Pc = [l[0] for l in X]; Qc = [l[1] for l in X] + report('5 control: stored #2162 CR2 realisation of cex_min_1 (GF(%d)) passes the CR2 hypothesis checker' % (1 << D['k']), + cr2_hyp_ok(Pc, Qc, D['k'], D['P'], D['Q'])) + neg = [] # negative controls: each must be REJECTED + r = U['configs']['desargues'][1]; Xb = [list(x) for x in r['X']]; Xb[3][1] ^= 1 + neg.append(('corrupted certificate entry', universal_ok(r['P'], r['L'], r['k'], Xb, r['Y']))) + r2 = U['configs']['desargues'][2] + neg.append(('certificate checked against another frame', universal_ok(r2['P'], r2['L'], r['k'], r['X'], r['Y']))) + r3 = U['configs']['pappus'][5] + neg.append(('Pappus GF(4) certificate read over GF(8)', universal_ok(r3['P'], r3['L'], 3, r3['X'], r3['Y']))) + Cb = desargues(); Cb['points'] = list(Cb['points']); p9 = Cb['points'][9]; Cb['points'][9] = (p9[0] + 1, p9[1], p9[2]) + neg.append(('corrupted Desargues realisation (one coordinate +1)', check_config(Cb, 10, 3))) + Db = [list(x) for x in D['P']]; Db[0] = [0, 0, 0] + neg.append(('cex_min_1 realisation with a zeroed point', cr2_hyp_ok(Pc, Qc, D['k'], Db, D['Q']))) + neg.append(('tied_min with a constant GF(2) assignment', cr2_hyp_ok(Pm, Qm, 1, [[1, 1, 1]] * 12, [[1, 1, 0]] * 12))) + report('5 negative controls rejected: ' + '; '.join(nm for nm, val in neg), not any(val for nm, val in neg), + str([nm for nm, val in neg if val])) + + # 6. special (zero-richer) realisations: combinatorial lemma for Desargues, certificates for the Pappus signatures + for C, n in confs: + inc = {tuple(x) for x in C['incidences']}; pn, ln = C['pnames'], C['lnames'] + colin = lambda a, b: any((pn[a], ln[l]) in inc and (pn[b], ln[l]) in inc for l in range(n)) + conc = lambda a, b: any((pn[p], ln[a]) in inc and (pn[p], ln[b]) in inc for p in range(n)) + free_pt = [t for t in itertools.combinations(range(n), 3) if not any(colin(a, b) for a, b in itertools.combinations(t, 2))] + free_ln = [t for t in itertools.combinations(range(n), 3) if not any(conc(a, b) for a, b in itertools.combinations(t, 2))] + if C['name'] == 'desargues': + report('6 Desargues lemma: every point triple contains two points on a common configuration line (and dually), so no ' + 'exact realisation has an extra collinear / concurrent triple', not free_pt and not free_ln) + else: + report('6 Pappus: the only possible extra collinear point triples are A_iB_iC_i and the only extra concurrent line ' + 'triples are {l,m,pap}, {A0B1,A1B2,A2B0}, {A0B2,A1B0,A2B1}: %s / %s' % (free_pt, free_ln), + free_pt == [(0, 3, 6), (1, 4, 7), (2, 5, 8)] and free_ln == [(0, 1, 2), (3, 6, 7), (4, 5, 8)]) + SP = json.load(open(os.path.join(PKG, 'data', 'special.json'))); ok = True; nfr = 0; uncert = [] + ok &= SP['configs']['desargues']['signatures'] == 0 + for r in SP['configs']['pappus']['realisations']: + C = pappus(**{k: tuple(v) for k, v in r['params'].items()}) + ok &= check_config(C, 9, 3) and [list(p) for p in C['points']] == r['points'] and [list(l) for l in C['lines']] == r['lines'] + frs = [('I',)] + frames(C); ok &= [tuple(f['frame']) for f in r['frames']] == frs + for f, fr in zip(r['frames'], frs): + P2, L2 = (C['points'], C['lines']) if fr == ('I',) else transform(C, fr) + if f['k'] is None: + uncert.append((r['params'], fr)); ok &= f.get('excluded_upto') == 4 + ok &= all(universal_realise(P2, L2, k, limit=10 ** 6) is None for k in (1, 2, 3, 4)) + else: + ok &= universal_ok(P2, L2, f['k'], f['X'], f['Y']); nfr += 1 + sigs = {(tuple(map(tuple, r['extra_point_triples'])), tuple(map(tuple, r['extra_line_triples']))) + for r in SP['configs']['pappus']['realisations']} + report('6 Pappus special realisations: %d extra-triple signatures (grid %d points), %d frame certificates verified; ' + 'exactly one coordinate system without one, exhaustively excluded over GF(2..16): %s' + % (len(sigs), SP['configs']['pappus']['scanned'], nfr, uncert), ok and len(sigs) == 12 and len(uncert) == 1 + and uncert[0][1] == ('I',)) + + # 7. per-instance classification on that coordinate system + SI = json.load(open(os.path.join(PKG, 'data', 'special_instances.json'))) + tgt = [r for r in SP['configs']['pappus']['realisations'] if any(f['k'] is None for f in r['frames'])][0] + P2, L2 = tgt['points'], tgt['lines']; ok = True; sc = dict(cr2=0, exact=0, skipped=0, py_exhaustive=0) + special_mins = [] + for rec in SI['instances']: + P = [P2[i] for i, k in rec['pairs']]; Q = [L2[k] for i, k in rec['pairs']] + R_, A_, free = setup(P, Q); v = len(P) + ok &= all(dot(p, q) != 0 for p, q in zip(P, Q)) and len(free) == rec['f'] and v == rec['v'] + if rec['status'] == 'CR2': + ok &= cr2_hyp_ok(P, Q, rec['k'], rec['Pt'], rec['Qt']) if rec['via'] == 'dfs' else odd_diagonal(P, Q); sc['cr2'] += 1 + continue + pi, sig = cfg_data(P, Q) + ok &= rec['status'] == 'nonCR2' and all(realise(pi, sig, set(free), k=k) is None for k in (1, 2, 3)) + if rec.get('exact') == 'skipped-f': + ok &= len(free) > 26; sc['skipped'] += 1; continue + ok &= cost_of(P, Q, tomat(rec['witness_g'], free, v)) == rec['min'] and rec['witness_g'] < 1 << len(free) + if len(free) <= 18: + ok &= min(cost_of(P, Q, tomat(g, free, v)) for g in range(1 << len(free))) == rec['min']; sc['py_exhaustive'] += 1 + if ENUMALL: + import subprocess + inp = '%d %d\n' % (v, len(free)) + ''.join('%d %d\n' % e for e in free) + ''.join( + '%d %s\n%d %s\n' % (len(R_[j]), ' '.join(map(str, R_[j])), len(A_[j]), ' '.join(map(str, A_[j]))) for j in range(3)) + ok &= int(subprocess.run([ENUMALL, '0'], input=inp, capture_output=True, text=True, check=True).stdout.split()[0]) == rec['min'] + sc['exact'] += 1; special_mins.append(rec['min'] - v) + report('7 special Pappus frame: %d sampled instances (seed %d): %d CR2-certified (rechecked), %d non-CR2 (cr2.py DFS re-run, ' + 'exhaustive) of which %d exact minima (witness costs rechecked; %d also by pure-Python exhaustion%s), %d skipped f > 26' + % (len(SI['instances']), SI['seed'], sc['cr2'], sc['exact'] + sc['skipped'], sc['exact'], sc['py_exhaustive'], + ', all replayed with enumall' if ENUMALL else '', sc['skipped']), ok) + + summary = dict(CR2_certified=n_cert + sc['cr2'], non_CR2_exact=sc['exact'], skipped=sc['skipped'], + universal_frames=nframes) + mins = special_mins + print(' counts %s; min(cost - v) over the non-CR2 set: %s (%.1fs)' + % (summary, min(mins) if mins else 'n/a', + time.time() - T0)) + print('PASS_THREE_TOTAL_CLASSICAL_CONFIGS' if not BAD[0] else 'FAIL_THREE_TOTAL_CLASSICAL_CONFIGS (%d failures)' % BAD[0]) + sys.exit(1 if BAD[0] else 0) + + +if __name__ == '__main__': + main() From 67294e7dd5bc7caa0d253b74e1d39c376ca99663 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Thu, 15 Oct 2026 08:35:02 +0530 Subject: [PATCH 2/2] research: three-total-classical-configs review fixes (scope, lower-bound labelling, summary assertion) - Qualify "non-CR2" as "no CR2 realisation over GF(2/4/8)" (per instance) and "no frame-universal certificate over GF(2^k), k <= 4" (per frame). - Scope the single certificate-search failure to 1 of 2,166 coordinate systems examined (13 identity frames, one mixed type); scope Pappus coverage to the generic + 12 grid-found signatures. - verify.py: new check 8 asserts the summary counts and min(cost - v) = 1; check 7 states that default mode re-derives lower bounds only for f <= 18; incidence-only negative control (swapped Pappus line vectors); guard against a missing uncertified frame instead of IndexError. - README/TASK/VERIFY: handoff + claim links, novelty delta vs #2111 X2/#2162, concurrent credit to #2206, tested interpreter, "separately coded" wording, likely-classical note on the PG(2,8) Desargues fact. Co-Authored-By: Claude Opus 5.5 --- .../three-total-classical-configs/README.md | 88 +++++++++++++------ .../three-total-classical-configs/TASK.json | 12 +-- .../three-total-classical-configs/VERIFY.json | 2 +- .../three-total-classical-configs/verify.py | 32 +++++-- 4 files changed, 93 insertions(+), 41 deletions(-) diff --git a/research/three-total-classical-configs/README.md b/research/three-total-classical-configs/README.md index 8a613404a3..b164246b7d 100644 --- a/research/three-total-classical-configs/README.md +++ b/research/three-total-classical-configs/README.md @@ -10,6 +10,19 @@ Base commit `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. Predecessor pins: PR #21 hashes in [NOTICE.md](NOTICE.md)). The selected record (`certificates/selected-result.json`, κ = 0.001672660197076918, #1094) is untouched and unaffected. +Terminology: "no CR2 realisation" below always means **none over GF(2), GF(4) or GF(8)** for a single instance, or **no +frame-universal certificate over GF(2^k), k ≤ 4** for a frame. Lemma CR2 allows any char-2 field, so these are bounded +failed searches, not proofs of non-realisability. + +Links: the handoff this answers is +https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18932893 and the sprint claim is +https://github.com/CrocSwap/integer-mult-bounds/discussions/1163#discussioncomment-18936306. + +**What is new relative to the predecessors.** In full-support (generic) coordinates the result already follows from +#2162 Lemma CR2 plus char-2 embeddability of the incidence pattern (compare #2111's X2 Hesse experiment). This package's +contribution is the structured, support-restricted frames, the special (zero-richer) Pappus realisations, and the one +coordinate system found where the certificate search fails. + ## Question Model (#2111 §1, from #446/#595): a T = 3 decoder configuration is a list of v pairs (p(t), q(t)) ∈ Z³ × Z³ with @@ -25,7 +38,8 @@ instances would be where (A) is genuinely open, and they could give new tight at ## Result -1. **Every structured Desargues/Pappus decoder configuration satisfies (A) (conditional on CR2).** The objects are: +1. **Every structured Desargues/Pappus decoder configuration satisfies (A), conditional on CR2** (Desargues: every exact + realisation over Q; Pappus: the generic signature and the 12 grid-found special signatures, see item 2). The objects are: - Desargues 10_3 and Pappus 9_3 over Q. Each is an exact realisation, checked to have exactly the 30 / 27 incidences. - Every structured frame. A frame is three non-collinear configuration points sent to e₁, e₂, e₃, or three non-concurrent configuration lines sent to the coordinate lines. There are 110 + 110 Desargues frames and 75 + 75 Pappus frames, plus @@ -47,32 +61,43 @@ instances would be where (A) is genuinely open, and they could give new tight at `data/special.json` holds a GF(4) universal certificate. 3. **Field size (side fact).** - Desargues frame-universal realisations are exhaustively excluded over GF(2), GF(4) and GF(8) in every frame. - - An independent constructive count confirms this. It fixes O, a₀, a₁ = e₁, e₂, e₃ and enumerates a₂ and μ_i. It finds + - A separately coded constructive count (a second method in the same verifier; a local-only pre-submission review, whose scripts are not in this package, reproduced the + counts 0/0/1344 with its own code and normalisation) confirms this. Since a GF(4)/GF(8) frame certificate would itself + be an exact 10_3 in PG(2,4)/PG(2,8), this covers every frame, not only the DFS-replayed subset. It fixes O, a₀, a₁ = e₁, e₂, e₃ and enumerates a₂ and μ_i. It finds **no exact Desargues 10_3 in PG(2,4) or PG(2,8)**, but finds 1344 in PG(2,16) with a₂ fixed. - In the frame (O, a₀, a₁), relaxing exactly one of the 10 "opposite" non-incidences (for example the centre O and the axis) makes GF(8) feasible, and relaxing any other single non-incidence does not. This was an exploratory run and is not part of the verifier. - On the sampled instances the per-instance DFS never needed more than GF(4) (740 Desargues/Pappus samples: 710 GF(2), 10 GF(4), 20 by the 2-adic test). So GF(16) is a cost of universality only. We did not search the literature for this - embedding fact. -4. **Where CR2 does fail (the hypothesis, confirmed once).** One coordinate system has no frame-universal certificate: + embedding fact; it is likely classical (every planar Desargues configuration is a plane section of the complete + 5-point in PG(3,q)), so it is not claimed as new. +4. **Where the CR2 certificate search fails (the hypothesis, confirmed once).** Of the 2,166 coordinate systems examined + (every structured frame of the generic and the 12 special realisations, plus 13 identity frames that are all of one + mixed type: e₁ = l∩m, e₃ = A₀, x = 0 the join A₀B₀), exactly one has no frame-universal certificate over GF(2..16). + No other mixed frame type was tested. - The configuration is the special Pappus realisation `a=(0,1,-1), b=(0,-15,15)`. In it A₀B₀C₀ are collinear and l, m and pap are concurrent. - Its coordinates are the stored ones. The coordinate line x = 0 is the extra line A₀B₀C₀, e₁ is the concurrency point, and e₃ = A₀. This frame is mixed: it uses non-configuration elements. - No universal realisation exists there over GF(2..16) (exhaustive). The same realisation in full-support coordinates does have one over GF(4) (exploratory check with one integer change of coordinates; not in the verifier). So the obstruction comes from the support restriction. - - We sampled 2000 decoder configurations in this frame (seed 22, v = 6..10). Of these, 1912 are CR2 and - **88 are not CR2** over GF(2), GF(4) or GF(8). + - We sampled 2000 decoder configurations in this frame (seed 22, v = 6..10). Of these, 1912 are CR2-certified and + **88 have no CR2 realisation over GF(2), GF(4) or GF(8)** (written "non-CR2" below, with that meaning only). - 18 non-CR2 instances have f ≤ 26. For these, the exact minimum over all 2^f admissible B (vendored `enumall.c`; - witnesses rechecked in pure Python, f ≤ 18 also exhausted in pure Python) gives **min(cost − v) = 1**. + witnesses rechecked in pure Python, f ≤ 18 also exhausted in pure Python) gives **min(cost − v) = 1**. The default + verifier re-derives the lower bounds only for the 3 instances with f ≤ 18; for the other 15 (f = 19..26) it checks the + witness (an upper bound) and the lower bound is recorded enumall output, replayed by `--enumall` (which re-runs the same + vendored C code, not an independent implementation). A local-only pre-submission review (scripts not included) re-enumerated all 18 + minima with its own C enumerator and found no B with cost < v. Distribution of (v, f, min): (7,16,11), (7,17,9), (7,18,10), (7,19,10), (8,20,11), (8,21,11), (8,22,11), (8,24,9), (8,24,11), (8,25,12), (8,26,10), (8,26,11), (9,19,13), (9,24,11), (9,24,12) ×2, (9,26,12), (9,26,14); the single cost − v = 1 instance is (v, f, min) = (8, 24, 9). The non-CR2 instances by v: 4 at v = 7, 9 at v = 8, 20 at v = 9, 55 at v = 10, none at v = 6. The skipped f range is 27..45. - 70 instances have f > 26 and were skipped (counted, not claimed). So, within this bounded search, no counterexample and no tight non-CR2 atom was found. This is a failed finite search, not a proof of (A) for this frame. -Counts printed by the verifier: CR2-certified 2652, non-CR2 exact 18, skipped 70; min(cost − v) over the +Counts printed (and asserted, check 8) by the verifier: CR2-certified 2652, no CR2 realisation over GF(2/4/8) with exact +minimum 18, skipped 70; min(cost − v) over the non-CR2 exact set = 1. ### Lemma U (frame-universal certificate ⇒ CR2 for every pair list) @@ -99,33 +124,41 @@ checked on the stored realisation applies to the whole class. (Short proof here; ## Reproduce -From the repository root (standard library, Python ≥ 3.10; about 1–2 min on a loaded 4-CPU machine): +From the repository root (standard library only; tested on CPython 3.14.4 only, syntax is 3.10-compatible; about 1–2 min +on a loaded 4-CPU machine): ```sh python3 -I -B research/three-total-classical-configs/verify.py ``` Expected: every line `PASS`, then -`counts {'CR2_certified': 2652, 'non_CR2_exact': 18, 'skipped': 70, ...}; min(cost - v) over the non-CR2 set: 1` -and `PASS_THREE_TOTAL_CLASSICAL_CONFIGS`. To replay the recorded enumall minima natively as well, run -`gcc -O2 -o /tmp/enumall research/three-total-classical-configs/c/enumall.c` and add `--enumall /tmp/enumall`. +`counts {'CR2_certified': 2652, 'noCR2_GF2to8_exact': 18, 'skipped': 70, ...}; min(cost - v) over the set with no CR2 +realisation over GF(2/4/8) and f <= 26: 1` and `PASS_THREE_TOTAL_CLASSICAL_CONFIGS`. **Default mode certifies exact +minima (lower bounds) only for f ≤ 18 (3 instances); for f = 19..26 it checks witness upper bounds and asserts the +recorded minima.** To replay all 18 minima (including the headline (8, 24, 9) instance), run +`gcc -O2 -o /tmp/enumall research/three-total-classical-configs/c/enumall.c` and add `--enumall /tmp/enumall` +(about 3 min). The verifier does the following: - **Check 0:** hash pins. - **Check 1:** exact configurations. -- **Check 2:** search-free check of all 372 frame certificates, with independent GF(2^k) arithmetic written in `verify.py`. -- **Check 3:** exclusions. It replays the DFS on a frame subset and runs the independent constructive Desargues count with - a positive control. +- **Check 2:** search-free check of all 372 frame certificates, with separately coded GF(2^k) arithmetic in `verify.py`. +- **Check 3:** exclusions. It replays the DFS on a frame subset and runs the separately coded constructive Desargues count with + a positive control (the count also implies the Desargues exclusion in every frame). - **Check 4:** the sampled instances. - **Check 5:** controls. - `tied_min` (f = 72) must come out non-CR2 over GF(2/4/8). - The #2162 six-line atom must be non-CR2 with pure-Python exhaustive minimum 6 = v. - The stored #2162 GF(4) realisation of `cex_min_1` must pass the CR2 checker. - **Negative controls** must be rejected: a corrupted certificate entry, a certificate checked against another frame, a - GF(4) certificate read over GF(8), a corrupted realisation, a zeroed realisation point, and a constant assignment for - `tied_min`. + GF(4) certificate read over GF(8), a corrupted realisation, a zeroed realisation point, a Pappus certificate with two + line vectors swapped (incidence-only corruption), and a constant assignment for `tied_min`. The zeroed-point and + constant-assignment controls are rejected for trivial reasons (zero vector; zero diagonal), so they do not exercise + the incidence logic; the swapped-lines and corrupted-entry controls do. - **Check 6:** special realisations and the Desargues no-extra-triple lemma. -- **Check 7:** the non-CR2 instances. It re-runs the exhaustive DFS and rechecks every witness. +- **Check 7:** the instances with no CR2 realisation over GF(2/4/8). It re-runs the exhaustive DFS and rechecks every + witness; lower bounds as described above. +- **Check 8:** asserts the summary counts and min(cost − v) = 1. The task card asked for `tied_min` to come out "non-CR2 with exact minimum 12". Its f = 72 cannot be enumerated, so the minimum 12 is inherited from #2111/#2162 (Theorem T′). The verifier checks non-CR2 and uses the six-line atom as the @@ -144,8 +177,8 @@ BIN is `c/enumall.c` compiled with `gcc -O2`. - **Inherited:** Lemma CR2 and the a = 0 2-adic corollary (#2162, open PR; its README reports a Lean check of the core lemma, not re-reviewed here). The model and `enumall.c` come from #2111 (open PR). - **Covered:** pairs are configuration points with configuration lines. Coordinates are structured frames (or full-support - coordinates). Realisations are as in item 2. Intersection points of non-configuration lines, mixed frames (except the one - above), Pappus realisations with signatures outside the grid, Reye 12_4 and D4 arrangements are **not** covered. + coordinates). Realisations are as in item 2. Intersection points of non-configuration lines, mixed frames (only the identity + frames of the one mixed type above were examined), Pappus realisations with signatures outside the grid, Reye 12_4 and D4 arrangements are **not** covered. - **Finite certificate vs proof:** item 1 is a per-frame proof (Lemmas U and Z plus CR2) with stored, exactly checked certificates. The field-size exclusions are exhaustive finite computations. Item 4 is a **bounded failed search** for cost < v. It is not an impossibility theorem. The f > 26 non-CR2 instances are unresolved. @@ -155,31 +188,34 @@ BIN is `c/enumall.c` compiled with `gcc -O2`. ## Open next questions -1. **Do the f > 26 non-CR2 instances of the special Pappus frame also satisfy cost ≥ v + 1?** This matters because they are +1. **Do the f > 26 instances without a CR2 realisation over GF(2/4/8) of the special Pappus frame also satisfy cost ≥ v + 1?** This matters because they are the only open (A) instances from classical configurations found here. First step: run the #2162 Corollary J jet test, or SAT via #2111 `satlib`, on the skipped records in `data/special_instances.json`. Blocker: 2^f enumeration is infeasible, and jets can fail (jf0..2 of #2162). -2. **Mixed frames in general.** The single CR2 failure uses a coordinate triangle built from a non-configuration line and +2. **Mixed frames in general.** The single certificate-search failure uses a coordinate triangle built from a non-configuration line and point. Enumerate frames from the intersection points of the configuration's lines (and the joins of its points), then rerun `universal_sweep`. This matters because zero-rich supports from such frames are where CR2 can fail. Blocker: the frame count grows quickly; deduplicate by symmetry (S₅ for Desargues, order-108 group for Pappus). 3. **Reye 12_4 and the D4 arrangement** (the rest of OPEN ENDS item 4). The same frame-universal test applies. First step: build exact realisations with `check_config`, then run `universal_sweep.py`. No blocker beyond implementation time. 4. **Why GF(16) for Desargues?** Is "no exact Desargues 10_3 in PG(2,8)" known, and does the forced degeneracy (centre on - axis) explain it? First step: a literature check, then a proof from the μ-parametrisation in `verify.py`. This matters + axis) explain it? A sketch suggested by a pre-submission review (not verified here): a planar Desargues configuration is a + section of the complete 5-point in PG(3,q); in characteristic 2 the 15 forbidden points form a PG(3,2) subgeometry, and + a plane a·x = 0 avoids them iff a₁..a₄ are F₂-independent in GF(2^h), i.e. iff h ≥ 4. First step: a literature check, then a proof from the μ-parametrisation in `verify.py`. This matters only for the size of certificates, not for (A). ## Relation to the bottleneck Side result on the complex-supplier decoder sub-line. (A) at T = 3 limits what rank-3 root-unit decoders can save (#2111, #2125). This package removes structured Desargues/Pappus realisations as counterexample candidates. It also locates one -zero-rich coordinate system where CR2 fails, and finds no counterexample there within a bounded search. κ is unchanged. +zero-rich coordinate system where the CR2 certificate search fails (up to GF(16)), and finds no counterexample there within a bounded search. κ is unchanged. ## Credit DreamingOfClouds: #2111 (three-total model, `enumall.c`, `tied_min`, the Hesse X2 experiment, the OPEN ENDS handoff), #2162 (Lemma CR2, `cr2.py`, CR2 realisations, the non-CR2 atoms) and #2125. #1590 (Lemma B). #446/#595 (cost model). -Adjacent audits: petalas #2193 (anti-Fano) and RossRichardson #2176 (jf0). Concurrent: a sibling session of the same -account works on the exact cost of `cex_min_1` (#2111 item 5), a different object, which this package does not use. +Adjacent audits: petalas #2193 (anti-Fano) and RossRichardson #2176 (jf0). Concurrent: petalas #2206 certifies the exact +pairing cost 21 of the 19-line configuration `cex_min_1`, a different question; this package uses `cex_min_1` only as a +stored-CR2 control and does not use #2206. Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). Apache-2.0. diff --git a/research/three-total-classical-configs/TASK.json b/research/three-total-classical-configs/TASK.json index 169c76e761..0d44f8b7ea 100644 --- a/research/three-total-classical-configs/TASK.json +++ b/research/three-total-classical-configs/TASK.json @@ -50,25 +50,25 @@ ] }, "scope_status": "changed", - "actual_scope": "Desargues 10_3 and Pappus 9_3 over Q in structured coordinates (three configuration points or lines as the coordinate triangle) as T=3 three-total decoder configurations: classify them by characteristic-2 realisability (Lemma CR2 of open PR #2162) and compute the exact minimum cost over all admissible B on the non-CR2 remainder (OPEN ENDS item 4 of the #2111 handoff, narrowed to Desargues and Pappus).", + "actual_scope": "Desargues 10_3 and Pappus 9_3 over Q in structured coordinates (three configuration points or lines as the coordinate triangle) as T=3 three-total decoder configurations: classify them by characteristic-2 realisability (Lemma CR2 of open PR #2162) and compute the exact minimum cost over all admissible B on the remainder with no CR2 realisation over GF(2/4/8) (OPEN ENDS item 4 of the #2111 handoff, narrowed to Desargues and Pappus).", "scope_change_reason": "The generic rank-shape card is crowded (#2151, #2124, #2130, #2145). The live, unclaimed handoff https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18932893 (item 4) names classical rich configurations as an untested class for the T=3 decoder floor (A) cost >= v, which limits what rank-3 root-unit decoders can save. A pre-experiment overlap check showed that the generic coordinate regime is already decided by #2162 Lemma CR2, so the task was narrowed to structured (support-restricted) coordinates.", - "bottleneck_link": "Side result on the complex-supplier decoder sub-line: (A) at T=3 bounds the savings of rank-3 root-unit decoders (#2111, #2125). Removing Desargues/Pappus structured realisations as counterexample candidates, and locating where CR2 fails, narrows the open part of (A). No kappa change.", + "bottleneck_link": "Side result on the complex-supplier decoder sub-line: (A) at T=3 bounds the savings of rank-3 root-unit decoders (#2111, #2125). Removing Desargues/Pappus structured realisations as counterexample candidates, and locating the one coordinate system where the CR2 certificate search fails (up to GF(16)), narrows the open part of (A). No kappa change.", "budget_minutes": 90, "stop_rule": "Searching stopped by 2026-10-15T00:34:36Z. Instances with f > 26 are skipped and counted. CR2 certificates are per-frame/per-instance proofs resting on #2162 Lemma CR2. \"No cost < v among non-CR2 instances\" is a bounded failed search, not a proof of (A). At most one evidence-driven pivot (none used; the frame-universal certificate refines the planned per-instance CR2 test).", "outcome": "completed", - "evidence": "python3 -I -B research/three-total-classical-configs/verify.py prints PASS_THREE_TOTAL_CLASSICAL_CONFIGS. Frame-universal char-2 certificates exist for all 221 Desargues frames (GF(16); GF(2/4/8) excluded) and all 151 Pappus frames (GF(4)), and for all frames of 12 special Pappus signatures. Hence every structured decoder configuration built from them satisfies (A), conditional on CR2. One mixed coordinate system of a special Pappus realisation has no certificate. There, 88 of 2000 sampled instances are non-CR2; the 18 with f <= 26 have exact min(cost - v) = 1 and 70 are skipped. Independent constructive count: no exact Desargues 10_3 in PG(2,4) or PG(2,8).", + "evidence": "python3 -I -B research/three-total-classical-configs/verify.py prints PASS_THREE_TOTAL_CLASSICAL_CONFIGS. Frame-universal char-2 certificates exist for all 221 Desargues frames (GF(16); GF(2/4/8) excluded) and all 151 Pappus frames (GF(4)), and for all frames of 12 special Pappus signatures. Hence every structured decoder configuration built from them satisfies (A), conditional on CR2. Of 2,166 coordinate systems examined (all structured frames plus 13 identity frames of one mixed type), exactly one, a mixed frame of a special Pappus realisation, has no certificate over GF(2..16). There, 88 of 2000 sampled instances have no CR2 realisation over GF(2/4/8); the 18 with f <= 26 have exact min(cost - v) = 1 (lower bounds re-derived in pure Python for the 3 with f <= 18, the rest recorded enumall output replayed with --enumall) and 70 are skipped. Separately coded constructive count: no exact Desargues 10_3 in PG(2,4) or PG(2,8).", "author": "thakrarsagar", "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) via Claude Code: design, code, computation and write-up, directed and submitted by thakrarsagar.", "open_questions": [ { - "question": "Do the 70 skipped (f > 26) non-CR2 instances of the special Pappus frame also satisfy cost >= v + 1?", + "question": "Do the 70 skipped (f > 26) instances without a CR2 realisation over GF(2/4/8) of the special Pappus frame also satisfy cost >= v + 1?", "why_it_matters": "They are the only open (A) instances from classical configurations found here.", "first_step": "Run the #2162 Corollary J jet test, or SAT via the #2111 satlib, on the skipped records of data/special_instances.json.", "blocked_by": "2^f enumeration is infeasible (f = 27..45), and jets can fail (jf0..2 of #2162)." }, { - "question": "Do mixed coordinate frames (triangles from intersection points of configuration lines, or joins of points) produce more non-CR2 instances, and any with cost < v or tight non-CR2 atoms?", - "why_it_matters": "The single CR2 failure found uses a coordinate triangle with a non-configuration line and point; zero-rich supports there are where (A) is genuinely open.", + "question": "Do mixed coordinate frames (triangles from intersection points of configuration lines, or joins of points) produce more instances without a CR2 realisation, and any with cost < v or tight non-CR2 atoms?", + "why_it_matters": "The single certificate-search failure found (no certificate over GF(2..16)) uses a coordinate triangle with a non-configuration line and point; zero-rich supports there are where (A) is genuinely open.", "first_step": "Enumerate these frames up to the configuration symmetry group and rerun scripts/universal_sweep.py with the frame list extended.", "blocked_by": "Frame count grows quickly; symmetry reduction (S5 for Desargues, order-108 group for Pappus) is not implemented." }, diff --git a/research/three-total-classical-configs/VERIFY.json b/research/three-total-classical-configs/VERIFY.json index 6876ff3917..06cd7b41aa 100644 --- a/research/three-total-classical-configs/VERIFY.json +++ b/research/three-total-classical-configs/VERIFY.json @@ -13,7 +13,7 @@ "{package}/verify.py" ], "timeout_seconds": 300, - "checks": "Hash pins of the vendored #2162/#2111 files; exact Desargues/Pappus realisations; search-free check of 372 frame-universal char-2 certificates plus 1793 special-realisation certificates; replayed exhaustive exclusions and an independent constructive Desargues count with a positive control; 740 + 2000 sampled decoder configurations (CR2 rechecks; non-CR2 DFS re-run; witness costs; pure-Python exhaustion for f <= 18); controls tied_min, the six-line atom and cex_min_1; six negative controls that must be rejected." + "checks": "Hash pins of the vendored #2162/#2111 files; exact Desargues/Pappus realisations; search-free check of 372 frame-universal char-2 certificates plus 1793 special-realisation certificates; replayed exhaustive exclusions and an independent constructive Desargues count with a positive control; 740 + 2000 sampled decoder configurations (CR2 rechecks; no-CR2-over-GF(2/4/8) DFS re-run; witness costs (upper bounds); lower bounds by pure-Python exhaustion for f <= 18 only, the f = 19..26 minima are recorded enumall output unless --enumall BIN is passed); controls tied_min, the six-line atom and cex_min_1; seven negative controls that must be rejected; check 8 asserts the summary counts and min(cost - v) = 1." } ] } diff --git a/research/three-total-classical-configs/verify.py b/research/three-total-classical-configs/verify.py index 7c52212c13..47d9c78bb4 100644 --- a/research/three-total-classical-configs/verify.py +++ b/research/three-total-classical-configs/verify.py @@ -149,9 +149,12 @@ def main(): ok &= universal_realise(r['P'], r['L'], k, limit=200000) is None allex = all(r['excluded'] == list(range(1, kwant[C['name']])) and not r['timeout'] for r in recs) report('3 %s: frame-universal realisation exhaustively excluded over GF(2^k), k < %d, in every frame (recorded); ' - 'DFS replay on %d frames' % (C['name'], kwant[C['name']], len(sub)), ok and allex) + 'DFS replay on %d frames%s' % (C['name'], kwant[C['name']], len(sub), + '; for every frame this also follows from the count below, since a GF(4)/GF(8) frame certificate would be ' + 'an exact 10_3 in PG(2,4)/PG(2,8) and GF(2) is a subfield of both' if C['name'] == 'desargues' else ''), + ok and allex) c4, c8 = desargues_exact_count(2), desargues_exact_count(3) - report('3 Desargues 10_3, independent constructive count: no exact realisation in PG(2,4) or PG(2,8)', c4 == 0 and c8 == 0, + report('3 Desargues 10_3, separately coded constructive count: no exact realisation in PG(2,4) or PG(2,8)', c4 == 0 and c8 == 0, 'counts %d, %d' % (c4, c8)) r = next(x for x in U['configs']['desargues'] if x['frame'] == ['P', 0, 1, 2]) c16 = desargues_exact_count(4, a2_choices=[r['X'][3]]) @@ -211,6 +214,9 @@ def main(): neg.append(('corrupted Desargues realisation (one coordinate +1)', check_config(Cb, 10, 3))) Db = [list(x) for x in D['P']]; Db[0] = [0, 0, 0] neg.append(('cex_min_1 realisation with a zeroed point', cr2_hyp_ok(Pc, Qc, D['k'], Db, D['Q']))) + r4 = U['configs']['pappus'][7]; Yb = [list(y) for y in r4['Y']]; Yb[0], Yb[3] = Yb[3], Yb[0] + neg.append(('Pappus frame certificate with two line vectors swapped (incidence-only corruption)', + universal_ok(r4['P'], r4['L'], r4['k'], r4['X'], Yb))) neg.append(('tied_min with a constant GF(2) assignment', cr2_hyp_ok(Pm, Qm, 1, [[1, 1, 1]] * 12, [[1, 1, 0]] * 12))) report('5 negative controls rejected: ' + '; '.join(nm for nm, val in neg), not any(val for nm, val in neg), str([nm for nm, val in neg if val])) @@ -251,7 +257,11 @@ def main(): # 7. per-instance classification on that coordinate system SI = json.load(open(os.path.join(PKG, 'data', 'special_instances.json'))) - tgt = [r for r in SP['configs']['pappus']['realisations'] if any(f['k'] is None for f in r['frames'])][0] + tgts = [r for r in SP['configs']['pappus']['realisations'] if any(f['k'] is None for f in r['frames'])] + if not tgts: + report('7 special Pappus frame: no uncertified coordinate system recorded in data/special.json', False) + print('FAIL_THREE_TOTAL_CLASSICAL_CONFIGS (%d failures)' % BAD[0]); sys.exit(1) + tgt = tgts[0] P2, L2 = tgt['points'], tgt['lines']; ok = True; sc = dict(cr2=0, exact=0, skipped=0, py_exhaustive=0) special_mins = [] for rec in SI['instances']: @@ -274,15 +284,21 @@ def main(): '%d %s\n%d %s\n' % (len(R_[j]), ' '.join(map(str, R_[j])), len(A_[j]), ' '.join(map(str, A_[j]))) for j in range(3)) ok &= int(subprocess.run([ENUMALL, '0'], input=inp, capture_output=True, text=True, check=True).stdout.split()[0]) == rec['min'] sc['exact'] += 1; special_mins.append(rec['min'] - v) - report('7 special Pappus frame: %d sampled instances (seed %d): %d CR2-certified (rechecked), %d non-CR2 (cr2.py DFS re-run, ' - 'exhaustive) of which %d exact minima (witness costs rechecked; %d also by pure-Python exhaustion%s), %d skipped f > 26' + report('7 special Pappus frame: %d sampled instances (seed %d): %d CR2-certified (rechecked), %d with no CR2 realisation ' + 'over GF(2/4/8) (cr2.py DFS re-run, exhaustive) of which %d have recorded exact minima: witness costs (upper bounds) ' + 'rechecked for all; lower bounds re-derived by pure-Python exhaustion for %d (f <= 18)%s; %d skipped f > 26' % (len(SI['instances']), SI['seed'], sc['cr2'], sc['exact'] + sc['skipped'], sc['exact'], sc['py_exhaustive'], - ', all replayed with enumall' if ENUMALL else '', sc['skipped']), ok) + ', and for all by replaying the vendored enumall' if ENUMALL else + '; the other lower bounds are recorded enumall output (pass --enumall BIN to replay them)', sc['skipped']), ok) - summary = dict(CR2_certified=n_cert + sc['cr2'], non_CR2_exact=sc['exact'], skipped=sc['skipped'], + summary = dict(CR2_certified=n_cert + sc['cr2'], noCR2_GF2to8_exact=sc['exact'], skipped=sc['skipped'], universal_frames=nframes) mins = special_mins - print(' counts %s; min(cost - v) over the non-CR2 set: %s (%.1fs)' + expected = dict(CR2_certified=2652, noCR2_GF2to8_exact=18, skipped=70, universal_frames={'desargues': 221, 'pappus': 151}) + report('8 summary equals the recorded result (counts %s, min(cost - v) = 1, no cost < v)%s' % ( + expected, '' if ENUMALL else '; lower bounds for f = 19..26 are recorded enumall output in default mode'), + summary == expected and bool(mins) and min(mins) == 1) + print(' counts %s; min(cost - v) over the set with no CR2 realisation over GF(2/4/8) and f <= 26: %s (%.1fs)' % (summary, min(mins) if mins else 'n/a', time.time() - T0)) print('PASS_THREE_TOTAL_CLASSICAL_CONFIGS' if not BAD[0] else 'FAIL_THREE_TOTAL_CLASSICAL_CONFIGS (%d failures)' % BAD[0])