diff --git a/research/gaussian-all-clique-dual/CERTIFICATE.json b/research/gaussian-all-clique-dual/CERTIFICATE.json new file mode 100644 index 0000000000..d18b262461 --- /dev/null +++ b/research/gaussian-all-clique-dual/CERTIFICATE.json @@ -0,0 +1,971 @@ +{ + "format": "gaussian-all-clique-dual-v1", + "root_count": 240, + "line_count": 60, + "orthogonal_ordered_pair_count": 900, + "dual_pair_count": 180, + "dual_pairs": [ + [ + 0, + 45 + ], + [ + 0, + 54 + ], + [ + 0, + 59 + ], + [ + 1, + 12 + ], + [ + 1, + 55 + ], + [ + 1, + 58 + ], + [ + 2, + 11 + ], + [ + 2, + 56 + ], + [ + 2, + 57 + ], + [ + 3, + 10 + ], + [ + 3, + 48 + ], + [ + 3, + 51 + ], + [ + 4, + 9 + ], + [ + 4, + 49 + ], + [ + 4, + 50 + ], + [ + 5, + 8 + ], + [ + 5, + 46 + ], + [ + 5, + 53 + ], + [ + 6, + 7 + ], + [ + 6, + 47 + ], + [ + 6, + 52 + ], + [ + 7, + 6 + ], + [ + 7, + 47 + ], + [ + 7, + 52 + ], + [ + 8, + 5 + ], + [ + 8, + 46 + ], + [ + 8, + 53 + ], + [ + 9, + 4 + ], + [ + 9, + 49 + ], + [ + 9, + 50 + ], + [ + 10, + 3 + ], + [ + 10, + 48 + ], + [ + 10, + 51 + ], + [ + 11, + 2 + ], + [ + 11, + 56 + ], + [ + 11, + 57 + ], + [ + 12, + 1 + ], + [ + 12, + 55 + ], + [ + 12, + 58 + ], + [ + 13, + 20 + ], + [ + 13, + 38 + ], + [ + 13, + 43 + ], + [ + 14, + 19 + ], + [ + 14, + 37 + ], + [ + 14, + 44 + ], + [ + 15, + 18 + ], + [ + 15, + 40 + ], + [ + 15, + 41 + ], + [ + 16, + 17 + ], + [ + 16, + 39 + ], + [ + 16, + 42 + ], + [ + 17, + 16 + ], + [ + 17, + 39 + ], + [ + 17, + 42 + ], + [ + 18, + 15 + ], + [ + 18, + 40 + ], + [ + 18, + 41 + ], + [ + 19, + 14 + ], + [ + 19, + 37 + ], + [ + 19, + 44 + ], + [ + 20, + 13 + ], + [ + 20, + 38 + ], + [ + 20, + 43 + ], + [ + 21, + 28 + ], + [ + 21, + 30 + ], + [ + 21, + 35 + ], + [ + 22, + 27 + ], + [ + 22, + 29 + ], + [ + 22, + 36 + ], + [ + 23, + 26 + ], + [ + 23, + 32 + ], + [ + 23, + 33 + ], + [ + 24, + 25 + ], + [ + 24, + 31 + ], + [ + 24, + 34 + ], + [ + 25, + 24 + ], + [ + 25, + 31 + ], + [ + 25, + 34 + ], + [ + 26, + 23 + ], + [ + 26, + 32 + ], + [ + 26, + 33 + ], + [ + 27, + 22 + ], + [ + 27, + 29 + ], + [ + 27, + 36 + ], + [ + 28, + 21 + ], + [ + 28, + 30 + ], + [ + 28, + 35 + ], + [ + 29, + 22 + ], + [ + 29, + 27 + ], + [ + 29, + 36 + ], + [ + 30, + 21 + ], + [ + 30, + 28 + ], + [ + 30, + 35 + ], + [ + 31, + 24 + ], + [ + 31, + 25 + ], + [ + 31, + 34 + ], + [ + 32, + 23 + ], + [ + 32, + 26 + ], + [ + 32, + 33 + ], + [ + 33, + 23 + ], + [ + 33, + 26 + ], + [ + 33, + 32 + ], + [ + 34, + 24 + ], + [ + 34, + 25 + ], + [ + 34, + 31 + ], + [ + 35, + 21 + ], + [ + 35, + 28 + ], + [ + 35, + 30 + ], + [ + 36, + 22 + ], + [ + 36, + 27 + ], + [ + 36, + 29 + ], + [ + 37, + 14 + ], + [ + 37, + 19 + ], + [ + 37, + 44 + ], + [ + 38, + 13 + ], + [ + 38, + 20 + ], + [ + 38, + 43 + ], + [ + 39, + 16 + ], + [ + 39, + 17 + ], + [ + 39, + 42 + ], + [ + 40, + 15 + ], + [ + 40, + 18 + ], + [ + 40, + 41 + ], + [ + 41, + 15 + ], + [ + 41, + 18 + ], + [ + 41, + 40 + ], + [ + 42, + 16 + ], + [ + 42, + 17 + ], + [ + 42, + 39 + ], + [ + 43, + 13 + ], + [ + 43, + 20 + ], + [ + 43, + 38 + ], + [ + 44, + 14 + ], + [ + 44, + 19 + ], + [ + 44, + 37 + ], + [ + 45, + 0 + ], + [ + 45, + 54 + ], + [ + 45, + 59 + ], + [ + 46, + 5 + ], + [ + 46, + 8 + ], + [ + 46, + 53 + ], + [ + 47, + 6 + ], + [ + 47, + 7 + ], + [ + 47, + 52 + ], + [ + 48, + 3 + ], + [ + 48, + 10 + ], + [ + 48, + 51 + ], + [ + 49, + 4 + ], + [ + 49, + 9 + ], + [ + 49, + 50 + ], + [ + 50, + 4 + ], + [ + 50, + 9 + ], + [ + 50, + 49 + ], + [ + 51, + 3 + ], + [ + 51, + 10 + ], + [ + 51, + 48 + ], + [ + 52, + 6 + ], + [ + 52, + 7 + ], + [ + 52, + 47 + ], + [ + 53, + 5 + ], + [ + 53, + 8 + ], + [ + 53, + 46 + ], + [ + 54, + 0 + ], + [ + 54, + 45 + ], + [ + 54, + 59 + ], + [ + 55, + 1 + ], + [ + 55, + 12 + ], + [ + 55, + 58 + ], + [ + 56, + 2 + ], + [ + 56, + 11 + ], + [ + 56, + 57 + ], + [ + 57, + 2 + ], + [ + 57, + 11 + ], + [ + 57, + 56 + ], + [ + 58, + 1 + ], + [ + 58, + 12 + ], + [ + 58, + 55 + ], + [ + 59, + 0 + ], + [ + 59, + 45 + ], + [ + 59, + 54 + ] + ], + "dual_pairing_rank_census": { + "2": 180 + }, + "dual_multiplier": "1/9", + "ceiling": "40", + "frames": [ + [ + 0, + 45, + 54, + 59 + ], + [ + 1, + 12, + 55, + 58 + ], + [ + 2, + 11, + 56, + 57 + ], + [ + 3, + 10, + 48, + 51 + ], + [ + 4, + 9, + 49, + 50 + ], + [ + 5, + 8, + 46, + 53 + ], + [ + 6, + 7, + 47, + 52 + ], + [ + 13, + 20, + 38, + 43 + ], + [ + 14, + 19, + 37, + 44 + ], + [ + 15, + 18, + 40, + 41 + ], + [ + 16, + 17, + 39, + 42 + ], + [ + 21, + 28, + 30, + 35 + ], + [ + 22, + 27, + 29, + 36 + ], + [ + 23, + 26, + 32, + 33 + ], + [ + 24, + 25, + 31, + 34 + ] + ], + "clique_counts": { + "1": 60, + "2": 1320, + "3": 14000, + "4": 79200, + "5": 252288, + "6": 474240, + "7": 554880, + "8": 419040, + "9": 203200, + "10": 59904, + "11": 9600, + "12": 640 + }, + "clique_total": 2068372, + "minimum_dual_hits": { + "1": 18, + "2": 30, + "3": 42, + "4": 52, + "5": 60, + "6": 78, + "7": 84, + "8": 84, + "9": 92, + "10": 102, + "11": 108, + "12": 108 + }, + "minimum_witnesses": { + "1": [ + 0 + ], + "2": [ + 0, + 1 + ], + "3": [ + 0, + 1, + 2 + ], + "4": [ + 0, + 1, + 3, + 13 + ], + "5": [ + 0, + 1, + 3, + 5, + 13 + ], + "6": [ + 0, + 1, + 3, + 7, + 13, + 15 + ], + "7": [ + 0, + 7, + 9, + 11, + 13, + 15, + 21 + ], + "8": [ + 1, + 3, + 4, + 11, + 17, + 18, + 21, + 22 + ], + "9": [ + 0, + 1, + 3, + 4, + 11, + 17, + 18, + 21, + 22 + ], + "10": [ + 0, + 1, + 3, + 4, + 11, + 13, + 17, + 18, + 21, + 22 + ], + "11": [ + 0, + 1, + 3, + 4, + 5, + 11, + 13, + 17, + 18, + 21, + 22 + ], + "12": [ + 0, + 1, + 3, + 7, + 9, + 11, + 13, + 14, + 15, + 21, + 23, + 24 + ] + }, + "all_cliques_sha256": "e07f4d5b163728561aa881fd76ba32092d93a2914c2718019964f8dd013e8efd", + "all_cliques_encoding": "nonempty masks sorted numerically, uint64 little endian", + "original_dual_failure": { + "clique": [ + 0 + ], + "hits": 42, + "required": 45 + }, + "negative_controls": 6, + "inherited_primal_value": "640*12/192=40; PR738/PR770, not rebuilt here", + "new_kappa": false +} diff --git a/research/gaussian-all-clique-dual/CLAIM.md b/research/gaussian-all-clique-dual/CLAIM.md new file mode 100644 index 0000000000..5af2bceec8 --- /dev/null +++ b/research/gaussian-all-clique-dual/CLAIM.md @@ -0,0 +1,78 @@ +# Local sprint claim + +Contributor: William Lawyer, with substantial OpenAI Codex assistance. +Start: 2026-10-13 07:54:33 UTC. Expected finish: by 09:54:33 UTC. +Track: structural decoder research. Assignment seed: **40**, one operating-system +draw using Python `secrets.randbelow(100)`. +Base: `f567884aeb8851b6e794af1184119a3bfbe1e631`. + +Three narrow candidates were considered: + +1. Test a mixed partial-hyperplane rectangle decoder on the Gaussian E8 unit. + PR767 leaves partial supports open, but a positive supplier would require + a new complete cost and realization argument. +2. Test PR770's explicit hyperplane-pair dual on **all** nonorthogonal cliques, + including non-maximal cliques. Its inspected proof expressly excludes them. +3. Extend the Gaussian scalar floor to fixed-support nonlinear messages. + PR785 supplies this mechanism on Hurwitz geometry; that transfer offers + less separation from existing work than the all-clique certificate gap. + +Selected candidate: **2**. Seed 40 selects the second candidate by `seed % 3`; +its useful diversification is the previously excluded certificate domain. +Object: the 60 Gaussian E8 lines and PR770's 900 ordered orthogonal-normal +hyperplane pairs. Hypothesis: each nonempty nonorthogonal clique Q meets both +hyperplanes in at least `45 |Q|` ordered pairs. Test by complete integer +clique enumeration, with a separately constructed geometry and traversal. +Deliverable: a solver-free exact dual certificate closing this method's gap, +or an explicit failed-dual witness; no new kappa claim. + +The live inventory retrieved at 07:58:21 UTC contains 654 open PRs through +#857 and no open issues or pinned coordination issue. Scope overlaps were +checked in PR738, PR767, PR770, PR785, PR798 and PR801; their exact inspected +heads will be retained with the result. The ledger marks PR620 partially +reviewed; pending PR claims are not accepted supplier results. +No external reservation issue is opened. This local claim is the reservation. + +Research will stop by 09:24:33 UTC, leaving the final 30 minutes for verification +and handoff. One evidence-driven pivot is allowed if the proposed dual fails. + +## Result update + +Result posted at 2026-10-13 08:41:32 UTC: +[PR868: Gaussian E8 all-clique certificate ceiling is 40](https://github.com/CrocSwap/integer-mult-bounds/pull/868). +Research note / scoped negative result, **no new kappa**. The first result +commit is `7cdd3ac12254290c55bac602d5e293dea4d981ae`. + +The original 900-pair extension fails concretely on singleton `{0}`: +42 hits rather than 45. One evidence-driven pivot retains the 180 ordered +orthogonal-normal hyperplane pairs with six-line intersection. Each has +Gaussian pairing charge two. Every nonempty clique has at least nine hits +per vertex, bounding every nonnegative weighted-clique certificate by 40. +This closes PR770's expressly excluded non-maximal-clique domain; the +predecessor's feasible value 40 and scalar decoder interval [40,60] are +unchanged. A cost-40 decoder and a stronger multiplication bound are not +constructed. + +Domain and stopping rule: every nonempty clique in the fixed 60-line Gaussian +E8 nonorthogonality graph, extending until no vertex can be added; no sample +or size cutoff. Completed coverage: **2,068,372 cliques**, sizes 1–12, with +all counts and minima in `CERTIFICATE.json`. Seed 40 selected the task; the +coverage itself is deterministic and exhaustive. The increasing-order +traversal and an independent Gaussian-coordinate, Bron–Kerbosch/submask +implementation agree on the complete domain digest +`e07f4d5b163728561aa881fd76ba32092d93a2914c2718019964f8dd013e8efd`. + +The code and mathematical inputs pass ordinary replays and an isolated, +optimized cold export from staged Git blobs. All 10 package tests pass, +including source/certificate corruption controls and exhaustive small-graph +checks. `VALIDATION.md` records the measured checks and exclusions. A separate +scoped AI worker reviewed the proof; no independent human review is claimed. + +The refreshed overlap inventory at 08:33 UTC contains 661 open PRs through +#866, no coordination issue, no duplicate of this scope, and unchanged heads +for all eight inspected source PRs. Exact pins and predecessor credits are +retained. No external claim requires an update; this is the single local +claim result update. Research stopped after the complete certificate and +independent replay, within the 120-minute budget, leaving ample verification +and handoff time. Only the new package changes; no selected frontier or +`upstream/` files are edited. diff --git a/research/gaussian-all-clique-dual/LICENSE b/research/gaussian-all-clique-dual/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/gaussian-all-clique-dual/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/gaussian-all-clique-dual/NOTICE.md b/research/gaussian-all-clique-dual/NOTICE.md new file mode 100644 index 0000000000..754fef65cd --- /dev/null +++ b/research/gaussian-all-clique-dual/NOTICE.md @@ -0,0 +1,48 @@ +# Attribution and licenses + +Prepared for **William Lawyer (@WilliamLawyer)** with substantial **OpenAI +Codex assistance** in research selection, mathematics, proof review, +implementation, verification and writing. Separate Codex workers reviewed +the dual deduction and built an independent replay within the claimed +scope. These are independent implementations and AI reviews; no independent +human review is claimed. + +Credit **Sagar Thakrar (@thakrarsagar), PR738** for the Gaussian scalar copy +floor of 40, closure to geometric flats, the uniform 640-clique certificate, +and its exact whole-support pairing-rank replay. His unchanged proof is +retained at `vendor/pr738-PROOF.md`. + +Credit **@chinmayarvind23, PR770** for independent replay of +that floor and the ceiling 40 for all inclusion-maximal-clique weights. The +explicit limitation to maximal cliques is the starting point of this note. +Its unchanged proof and notice are retained under `vendor/pr770-*`. +The 180-pair dual and complete non-maximal-clique coverage are this note's +additional evidence. No predecessor executable code is imported. + +Credit **Joel Pulikkan (@GamingPuzzled), PR620** for the extension-ring E8 +geometry, decoder question, earlier searches and symmetric cost-60 upper +bound; its retained report is `vendor/pr620-extension-REPORT.md`. +Credit **Douglas R. Colkitt (@Mister-Meeseeks), PR703** for the earlier +weighted-clique method on Hurwitz geometry, and **DreamingOfClouds, +PR446/PR595** for the conditional source/reader pairing-rank and format +accounting used by that line of work. + +**Charles Bethin's PR767**, **Alexander Templeton's PR785**, **Jonathan Lam's +PR798**, **Rohan Guliani's PR801**, and **PR814's Eisenstein nonlinear-message +extension** were checked as overlapping or adjacent research. Their geometry, +decoder subclasses or nonlinear-message domains differ. No claims from +their PR titles are treated as the selected supplier result. + +The selected PR799 construction and its Jeremy Kothe / Chafik Boukhalfa / +DreamingOfClouds / eumemic and ancestral realization lineage retain the +credit in the base review and notices. This contribution changes none of +their source artifacts or selected result. + +[SOURCES.json](SOURCES.json) binds exact inspected heads and retained file +bytes. The Apache-2.0 license applies to new files and the retained source +documents; their original notices and attributions are preserved. +Relative references inside unchanged vendored documents refer to their +original source packages at the pinned commits, rather than this package. +Standard +E8 coordinates, basic Hermitian rank identities and graph algorithms are +not claimed as novel. No global literature-priority claim is made. diff --git a/research/gaussian-all-clique-dual/PROOF.md b/research/gaussian-all-clique-dual/PROOF.md new file mode 100644 index 0000000000..d6f04d9873 --- /dev/null +++ b/research/gaussian-all-clique-dual/PROOF.md @@ -0,0 +1,174 @@ +# A dual ceiling of 40 for all Gaussian E8 clique certificates + +Prepared by William Lawyer with substantial OpenAI Codex assistance. +Research note / scoped negative result. No new kappa or physical supplier. + +## Result and its predecessor boundary + +In the fixed 60-line Gaussian E8 geometry, **every nonnegative weighted-clique +certificate for the scalar binary decoder pairing-rank charge has value at +most 40 Gaussian rank units**. The weights may use every nonempty clique, +including singletons, non-maximal cliques, and mixtures of clique sizes. + +Sagar Thakrar's PR738 already supplies the valid value-40 certificate, closure +to flats and the abstract decoder interval [40,60]. @chinmayarvind23's PR770 +independently reproduces that result and proves the ceiling 40 for all +inclusion-maximal cliques. Its Section 5 explicitly excludes non-maximal +cliques. This note closes that certificate-domain gap. It neither finds a +cost-40 decoder nor improves the already established scalar lower bound. +The matching value-40 primal certificate is inherited from those pinned +sources; their unchanged full flat-pair replay is not repeated here. + +## Geometry and the certificate class + +Take the 240 doubled E8 roots in Q^8: the 112 vectors with two entries in +{−2,2} and all other entries zero, and the 128 vectors in {−1,1}^8 with an +even number of negative entries. Define J on each coordinate pair by +`(x,y) -> (-y,x)`. The roots are closed under J and J squared is −I. +Their orbits under {I,J,−I,−J} give 60 Gaussian lines in K^4, K=Q(i). +The check also establishes projective distinctness: for different chosen +roots r,s, `(r·s)^2+(r·Js)^2 < 64`, while every root has squared norm 8. + +Let G be the graph joining distinct **nonorthogonal** Gaussian lines. For a +support S, write X_S for its K-span and + +`c(R,A) = rank_K of the Hermitian pairing X_R by X_A`. + +A fitting binary decoder has `B_tt=1` and `B_ts=0` for distinct nonorthogonal +lines t,s; entries at distinct orthogonal lines are free. Thus for any +nonempty clique Q of G, `B[Q,Q]=I_|Q|`. +If `B = sum_j 1_Rj 1_Aj^T` over F2, its restriction to Q has +rank at most `sum_j [Q meets R_j and Q meets A_j]`. This is the predecessor's +principal-identity rank inequality; it permits asymmetric supports and any +finite number of scalar totals. + +A weighted-clique certificate is a nonnegative weight w_Q for each clique, +subject to the local domination inequalities + +`sum_Q w_Q [Q meets R and Q meets A] <= c(R,A)` + +for all source/reader supports (equivalently all their geometric closures). +Closure adds every configuration line in the same K-span: it preserves +pairing rank while only increasing clique-hit indicators. Hence constraints +on all closed supports imply the constraints on every smaller support; +closed supports are themselves permitted supports, proving the equivalence. +Its certified decoder lower bound is `sum_Q |Q| w_Q`. Repeated clique entries +can be combined. An empty clique contributes zero and can be omitted. +Negative weights and other submatrix or algebraic inequalities are outside +this certificate class. The theorem below bounds these certificates, not +arbitrary proofs of a decoder lower bound. + +## Exact dual supports and their charges + +For each configuration line t, let H_t be the set of configuration lines +orthogonal to t. All 60 H_t have 15 members and span the entire K-hyperplane +`t-perp` (Gaussian dimension three). There are 900 ordered pairs (t,u) of +distinct orthogonal configuration lines. + +Retain only the following ordered pairs: + +`D = {(t,u): t perpendicular u and |H_t intersection H_u| = 6}`. + +Exact geometry gives **180** such pairs. Their undirected graph partitions +the 60 normals into fifteen disjoint four-vertex complete graphs. This is a +diagnostic structural check; the primary incidence calculation directly +counts the ordered pairs and does not need the partition. + +For every pair in D, the local charge is exactly **2 Gaussian / 4 rational +rank units**. Indeed `X_Hu^perp=span_K(u)`, and orthogonality puts u in X_Ht. +The pairing kernel on X_Ht therefore has dimension one, so its rank is +`3-1=2`. The six-line intersection selects the useful pairs; it is not the +reason for that charge. Both implementations independently check all +hyperplane dimensions and all 180 pairing ranks by exact elimination. + +For a clique Q, define + +`h_D(Q) = # {(t,u) in D: Q meets H_t and Q meets H_u}`. + +The exhaustive finite lemma is: + +**For every nonempty clique Q of G, `h_D(Q) >= 9 |Q|`.** + +Its complete domain and exact minima are: + +| Size | Number of cliques | Minimum h_D | +|---:|---:|---:| +| 1 | 60 | 18 | +| 2 | 1,320 | 30 | +| 3 | 14,000 | 42 | +| 4 | 79,200 | 52 | +| 5 | 252,288 | 60 | +| 6 | 474,240 | 78 | +| 7 | 554,880 | 84 | +| 8 | 419,040 | 84 | +| 9 | 203,200 | 92 | +| 10 | 59,904 | 102 | +| 11 | 9,600 | 108 | +| 12 | 640 | 108 | + +There are **2,068,372** nonempty cliques and no larger clique. Every inequality +holds in integer arithmetic. CERTIFICATE.json includes one attaining witness +per size, all 180 dual pairs, the frame partition, and the SHA256 of every +clique mask sorted numerically and encoded as eight little-endian bytes. + +The primary traversal extends each clique in increasing vertex order. Every +clique has exactly one such sorted path; intersecting the available vertices +with each chosen vertex's neighbors retains exactly its possible extensions. +It visits every nonempty clique once, without a size cutoff or sample. + +The independent traversal enumerates inclusion-maximal cliques with +Bron–Kerbosch, then all their submasks and deduplicates them. Every clique in +a finite graph extends to a maximal clique, so this covers exactly the same +domain by a different algorithm. It reconstructs geometry separately and +agrees on the complete domain digest and all size minima. These are exact +finite certificates, not a proof-assistant formalization. + +## The all-clique ceiling + +Apply each local certificate constraint to `(R,A)=(H_t,H_u)` for the 180 +ordered pairs in D and sum. Their total charge is 360, giving + +`sum_Q w_Q h_D(Q) <= 360`. + +Nonnegative weights and the finite lemma give + +`9 sum_Q |Q| w_Q <= sum_Q w_Q h_D(Q) <= 360`. + +Therefore the certificate value is at most **40**. This is the explicit +dual, assigning weight **1/9** to each of the 180 local constraints. It +covers arbitrary nonuniform weights on all cliques, not just weights within +an orbit. No solver status or symmetry assumption about the weights is used. +Combined with the predecessor's feasible uniform value-40 certificate, it +settles the optimum of this entire specified certificate method at 40. + +## Failed hypothesis and controls + +The unmodified PR770 dual cannot simply be extended: with all 900 ordered +orthogonal pairs, a singleton Q={0} has 42 hits, below `45 |Q|`. This is a +concrete counterexample to the proposed extension, not a defect in PR770's +correctly scoped maximal-clique theorem. The retained result uses the +repaired dual above and checks its complete domain. + +The primary replay rejects the original singleton inequality, the stronger +coefficient 10 (a size-12 clique has only 108 hits), an orthogonal pair called +a clique, an empty clique in the nonempty domain, the complementary 720-pair +dual with the proposed coefficient 36, and a deleted orthogonality edge. +The independent replay and package tests add their own controls. + +## Scope and accounting + +This closes a proof mechanism for copied-information lower bounds. It is +not a search for a cheaper decoder, an impossibility theorem for all decoder +mechanisms, or a bound on new geometries. The actual scalar decoder optimum +remains between 40 and 60 Gaussian charge units. Vector or nonlinear totals, +sub-line supports, changed fitting patterns, interacting delivery programs, +and stronger inequalities remain outside this result. + +No helper, source-access operation, frame transition, restoration, recursive +child or assembly is implemented or priced as a new supplier. Translating +the abstract pairing-rank charge into physical costs inherits PR446 and the +predecessor's realization premises. The selected PR799 construction retains +its all-size/compiler, common-label/mutable-source, whole-call hosting, +precision/tape and analytic obligations. This note does not change them or +the selected conditional kappa, and it does not prove the multiplication +theorem. diff --git a/research/gaussian-all-clique-dual/README.md b/research/gaussian-all-clique-dual/README.md new file mode 100644 index 0000000000..5fd4d3c7f5 --- /dev/null +++ b/research/gaussian-all-clique-dual/README.md @@ -0,0 +1,59 @@ +# Gaussian E8 all-clique certificate ceiling: 40 + +**Research note / scoped negative result; no new kappa.** + +Nonnegative weighting of **any** nonorthogonal cliques in the fixed 60-line +Gaussian E8 configuration cannot certify copy charge above **40 Gaussian +rank units**. PR770 establishes this ceiling for inclusion-maximal cliques; +this contribution covers the non-maximal cliques it expressly leaves open. +PR738 and PR770 already supply the matching feasible certificate and the +scalar decoder interval [40,60]. A cost-40 decoder remains unconstructed. + +The new dual uses 180 exact hyperplane pairs of charge two. Complete +enumeration of **2,068,372 nonempty cliques** establishes the required +integer incidence inequality. An independent geometry implementation and +maximal-clique/submask traversal check the same complete domain. +[PROOF.md](PROOF.md) states the certificate class and the deduction. + +From the repository root, Python 3.10+ and its standard library suffice: + +```sh +python -B research/gaussian-all-clique-dual/verify.py +``` + +Expected: + +```text +PASS_GAUSSIAN_ALL_CLIQUE_DUAL cliques=2068372 ordered_pairs=180 ceiling=40 controls=6 no_new_kappa +``` + +Independent replay: + +```sh +python -B research/gaussian-all-clique-dual/independent.py +``` + +Both replays are offline, read-only by default, accept optimized Python, and +compare their rebuilt mathematical fields against [CERTIFICATE.json](CERTIFICATE.json). +The primary `--output /absolute/new/file.json` option exports a fresh receipt +and refuses an existing output. No third-party library or predecessor +executable is imported. [VALIDATION.md](VALIDATION.md) records measured checks. + +Exact base: `f567884aeb8851b6e794af1184119a3bfbe1e631`. +The selected conditional saving at this base is +`1661634653669567/10^18 = 0.001661634653669567`, PR799 X4. +[SOURCES.json](SOURCES.json) pins source heads, retained bytes and Git blobs; +[CLAIM.md](CLAIM.md) records seed 40, candidate selection, domain and handoff. +Only this new package changes. + +The original 900-pair dual fails at a singleton (42 hits instead of 45). +This is a failed extension hypothesis, not a flaw in the predecessor's +scoped theorem. The repaired dual settles the certificate-method ceiling, +without changing the lower bound, constructing a supplier, or proving the +full multiplication theorem. The unchanged predecessor primal flat-pair +checks are credited and pinned rather than repeated as new evidence. + +Prepared by **William Lawyer** with substantial **OpenAI Codex assistance** +in selection, mathematical development, implementation, independent AI +replay, review and packaging. No independent human review or literature +priority is claimed. Apache-2.0; see [NOTICE.md](NOTICE.md) and [LICENSE](LICENSE). diff --git a/research/gaussian-all-clique-dual/SOURCES.json b/research/gaussian-all-clique-dual/SOURCES.json new file mode 100644 index 0000000000..8db0a5093f --- /dev/null +++ b/research/gaussian-all-clique-dual/SOURCES.json @@ -0,0 +1,113 @@ +{ + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "attribution": "William Lawyer", + "selected_kappa": "1661634653669567/1000000000000000000", + "retained_files": { + "vendor/pr738-PROOF.md": { + "pr": 738, + "commit": "9671c5d72f3119ba26f3774f40aa7130c67bcf77", + "author": "thakrarsagar", + "source_path": "research/gaussian-clique-copy-bound/PROOF.md", + "license": "Apache-2.0", + "sha256": "e33a3950f172bc93400fffd85df55236059f5391d4ed8a82e0f12bcd7f196812", + "git_blob": "748e6324394d53cf910836eb55e28578d8bc684a" + }, + "vendor/pr770-PROOF.md": { + "pr": 770, + "commit": "48d027a664288ea1d4e987de63cb79588b8b936b", + "author": "chinmayarvind23", + "source_path": "research/gaussian-e8-copy-bound/PROOF.md", + "license": "Apache-2.0", + "sha256": "0f4ba837c2337cc06d7d3315e6e6a8598cc3919baf4f8a90c2a03713c2556a2c", + "git_blob": "ecd7b342e15c3435b39155305edab6191685ca71" + }, + "vendor/pr770-NOTICE.md": { + "pr": 770, + "commit": "48d027a664288ea1d4e987de63cb79588b8b936b", + "author": "chinmayarvind23", + "source_path": "research/gaussian-e8-copy-bound/NOTICE.md", + "license": "Apache-2.0", + "sha256": "f10fd675f1b45f9414718e4876ea4f6a28031610e8b4cac48a8f6d9ee271537b", + "git_blob": "1cbb79cde41910e4d220aa0f84d7786bfd5f73ce" + }, + "vendor/selected-result.json": { + "commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "source_path": "certificates/selected-result.json", + "license": "Apache-2.0", + "sha256": "9873519224e2db72d6a8c926f51e3e75129671e467948c6f6b03744f8bcfc699", + "git_blob": "1f107b55a2f045fa66d9c35d658b3b79549f5ba6" + }, + "vendor/pr620-extension-REPORT.md": { + "commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "source_path": "research/e8-decoder-floors-and-cold14-notes/s1-extension-rings/REPORT.md", + "license": "Apache-2.0", + "sha256": "e8de809976a1253087e9058d346dfcc7b098f6481c64f1569aa3072d27345e02", + "git_blob": "1a766e365587b0c1bce414b50ffb7b916ba28da9" + }, + "LICENSE": { + "commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "source_path": "LICENSE", + "license": "Apache-2.0", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64" + } + }, + "inspected_prs": { + "620": { + "head": "e9cf03bbdf7094b5a83f6dbd1d74bfd77a05fb87", + "author": "GamingPuzzled", + "status": "open; prior PR claims are context, not maintainer acceptance", + "title": "Research notes (no \u03ba claim): E8 decoder floors are tight; #615 levers exhausted; +1.1e-7 \u03ba owner-map headroom on #617" + }, + "738": { + "head": "9671c5d72f3119ba26f3774f40aa7130c67bcf77", + "author": "thakrarsagar", + "status": "open; prior PR claims are context, not maintainer acceptance", + "title": "Scoped negative result: Gaussian E8 copy floor 40 excludes three stages" + }, + "767": { + "head": "96b4b74677d1bef99e8346bfb6a4ed0531e58a62", + "author": "cbethin", + "status": "open; prior PR claims are context, not maintainer acceptance", + "title": "Scoped negative result: Gaussian E8 planar and incidence decoder obstructions" + }, + "770": { + "head": "48d027a664288ea1d4e987de63cb79588b8b936b", + "author": "chinmayarvind23", + "status": "open; prior PR claims are context, not maintainer acceptance", + "title": "Research: Gaussian E8 weighted maximal-clique ceiling 40 and independent replay" + }, + "785": { + "head": "83e78085ae9c110a34bff87e71387292d85e47c0", + "author": "azide0x37", + "status": "open; prior PR claims are context, not maintainer acceptance", + "title": "Scoped negative result: Hurwitz copy floor for fixed-support nonlinear messages" + }, + "798": { + "head": "0aea3382e49abd9a59d3cb6676cdb26fd15b04e5", + "author": "jonathanlam", + "status": "open; prior PR claims are context, not maintainer acceptance", + "title": "Research note: Eisenstein E8 copy cost \u226522 and sharp clique-method limit" + }, + "801": { + "head": "f0758653a5a1f72c3b59e58d6fe8d658db20b50b", + "author": "Rohansguliani", + "status": "open; prior PR claims are context, not maintainer acceptance", + "title": "Research: certified format ceilings for Eisenstein/Gaussian/Hurwitz E8 copy floors (no \u03ba claim)" + }, + "814": { + "head": "d91c5152b314391406b0ec792b6765a5cf0af2f1", + "author": "shiftybitshiftr", + "status": "open; prior PR claims are context, not maintainer acceptance", + "title": "Research: Eisenstein nonlinear message copy floor 22b under explicit width pricing" + } + }, + "runtime_dependencies": "Python 3.10+ standard library; no predecessor executable imports", + "selected_construction": { + "review": "docs/research/community-frontier799-review.md", + "actual_construction": "research/gauge44-frames-x/PROOF-NOTE-FRAMES-X4.md", + "source_head": "80e6463157cfc80b85af09e7e2f14748fe2dac60" + }, + "new_result_scope": "all nonnegative weighted clique certificates on fixed 60-line Gaussian E8 geometry", + "inherited_primal": "PR738 and PR770 independently certify uniform 1/192 on 640 size-12 cliques; unchanged full flat-pair coverage not replayed by this package" +} diff --git a/research/gaussian-all-clique-dual/VALIDATION.md b/research/gaussian-all-clique-dual/VALIDATION.md new file mode 100644 index 0000000000..56418a1617 --- /dev/null +++ b/research/gaussian-all-clique-dual/VALIDATION.md @@ -0,0 +1,63 @@ +# Verification receipt and limits + +William Lawyer / OpenAI Codex. All results below were observed on Windows, +CPython **3.10.9**, using only the standard library. No hosted-CI pass is +claimed by this receipt. + +Normal primary and independent replays passed during development. The final +code, certificate, source pins and retained files were then exported from +their **canonical staged Git blobs** into an otherwise empty directory. +Each exported byte matched the working file. No predecessor code or original +repository files were available to the cold package. Its commands ran with +an unrelated working directory: + +| Cold command | Result | Elapsed seconds | +|---|---|---:| +| `python -I -O -B /absolute/export/verify.py --output /absolute/new/receipt.json` | PASS; regenerated certificate equals every published field | 17.702 | +| `python -I -O -B /absolute/export/independent.py --show-report` | PASS; independent geometry, rank and complete domain agree | 7.840 | +| `python -B /absolute/export/test_package.py` | All 10 tests pass | 9.254 | + +These are single-run timings, not a performance improvement claim. +[evidence/cold-verification.json](evidence/cold-verification.json) records +the environment, completion time and SHA256 of the checked replay inputs. +The primary output, complete independent report and test output are retained +beside it. The handoff text and evidence receipt itself are not replay inputs. + +From the repository root, the ordinary checks are: + +```sh +python -B research/gaussian-all-clique-dual/verify.py +python -B research/gaussian-all-clique-dual/independent.py +python -B research/gaussian-all-clique-dual/test_package.py +``` + +The two algorithms agree on the complete domain of **2,068,372 nonempty +cliques**, all size counts and hit minima, all 180 ordered dual pairs and +the digest +`e07f4d5b163728561aa881fd76ba32092d93a2914c2718019964f8dd013e8efd`. +The primary rank checks use rational realification; the independent checks +use direct Gaussian-rational elimination. Both check all 60 hyperplane +dimensions and all 180 local pairing ranks, rather than a sample. + +Both clique enumerators are also checked against brute force on every +labelled graph of orders one through five (**1,099 graphs**). Controls cover +the failed original singleton dual, an overly strong coefficient, malformed +cliques and geometry, a dropped contributing dual pair, changed certificate +claims, an incorrect local pairing charge, corrupted retained source bytes, +an escaping source path and refusal to overwrite an existing receipt. +The package test also relocates and replays the independent checker with +`-I -O -B`. Explicit failure checks remain active under optimization. + +`python -B scripts/verify_selected_result.py` passed at the recorded base, +reporting selected kappa `1661634653669567/1000000000000000000` and checking +the original-source inventory and proof supplement. Staged whitespace checks +passed. Only this new research directory changes; selected construction +files, `upstream/`, generators and global certificates are untouched. + +The unchanged PR738/PR770 primal flat-pair checks are inherited and pinned; +this receipt does not present them as newly rerun. Full `make verify`, the +selected supplier cold replay, Linux CI and proof-assistant compilation were +not run for this isolated addition. This is an exact finite certificate for +the stated clique method, with a written dual deduction. It is not formal +verification of the full multiplication theorem or a construction of a +cost-40 decoder. diff --git a/research/gaussian-all-clique-dual/evidence/cold-verification.json b/research/gaussian-all-clique-dual/evidence/cold-verification.json new file mode 100644 index 0000000000..3cb988fc00 --- /dev/null +++ b/research/gaussian-all-clique-dual/evidence/cold-verification.json @@ -0,0 +1,42 @@ +{ + "completed_utc": "2026-10-13T08:32:54.179661+00:00", + "base": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "python": "3.10.9", + "implementation": "CPython", + "platform": "Windows-10-10.0.26200-SP0", + "source": "canonical staged Git blobs; unrelated working directory", + "verified_source_sha256": { + "CERTIFICATE.json": "44c18f0092c31bff7fe41fd860bff0d61d323e8bd1d772ea1d87a3b8e3db40d6", + "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "SOURCES.json": "b9e67e6e5f567924e1061dc006c88fab5521ed5430b17f43cb8f4cb2600accb1", + "independent.py": "442427fd199dffe7390def08fde789de9d98d82e60f3199948656449856f3399", + "test_package.py": "bf2eedbe97cf2bc69335a18763caa37d681d56274498876625d504fa4f62fc21", + "vendor/pr620-extension-REPORT.md": "e8de809976a1253087e9058d346dfcc7b098f6481c64f1569aa3072d27345e02", + "vendor/pr738-PROOF.md": "e33a3950f172bc93400fffd85df55236059f5391d4ed8a82e0f12bcd7f196812", + "vendor/pr770-NOTICE.md": "f10fd675f1b45f9414718e4876ea4f6a28031610e8b4cac48a8f6d9ee271537b", + "vendor/pr770-PROOF.md": "0f4ba837c2337cc06d7d3315e6e6a8598cc3919baf4f8a90c2a03713c2556a2c", + "vendor/selected-result.json": "9873519224e2db72d6a8c926f51e3e75129671e467948c6f6b03744f8bcfc699", + "verify.py": "0b7ad60f1cc3d5200f448c6cc370c89b024d155cec3d3be05dc4986ac3aaaebd" + }, + "checks": [ + { + "check": "primary-optimized", + "exit_code": 0, + "elapsed_seconds": 17.702 + }, + { + "check": "independent-optimized", + "exit_code": 0, + "elapsed_seconds": 7.84 + }, + { + "check": "package-tests", + "exit_code": 0, + "elapsed_seconds": 9.254 + } + ], + "certificate_mathematical_equality": true, + "independent_all_cliques_sha256": "e07f4d5b163728561aa881fd76ba32092d93a2914c2718019964f8dd013e8efd", + "clique_total": 2068372, + "source_hash_scope": "Only replay code, fixtures, source pins and retained source bytes; final handoff prose is not a mathematical input." +} diff --git a/research/gaussian-all-clique-dual/evidence/independent-replay.json b/research/gaussian-all-clique-dual/evidence/independent-replay.json new file mode 100644 index 0000000000..2c0b8f0f92 --- /dev/null +++ b/research/gaussian-all-clique-dual/evidence/independent-replay.json @@ -0,0 +1,790 @@ +{ + "all_cliques_sha256": "e07f4d5b163728561aa881fd76ba32092d93a2914c2718019964f8dd013e8efd", + "ceiling": "40", + "certificate_mathematical_fields_match": true, + "clique_counts": { + "1": 60, + "10": 59904, + "11": 9600, + "12": 640, + "2": 1320, + "3": 14000, + "4": 79200, + "5": 252288, + "6": 474240, + "7": 554880, + "8": 419040, + "9": 203200 + }, + "controls": { + "all_labelled_graphs_order1_through5": 1099, + "corrupted_certificate_digest_rejected": true, + "deleted_edge_rejected": true, + "dropped_dual_pair_rejected": true, + "dropped_pair_hits": 107, + "gaussian_rank_controls": 2, + "hermitian_sign_controls": 2, + "multiplier1_over10_rejected": true, + "odd_root_sign_rejected": true, + "original900_required_singleton_hits": 45, + "original900_singleton_hits": 42, + "orthogonal_pair_rejected": [ + 0, + 45 + ] + }, + "dual_multiplier": "1/9", + "dual_pair_count": 180, + "dual_pairs": [ + [ + 0, + 45 + ], + [ + 0, + 54 + ], + [ + 0, + 59 + ], + [ + 1, + 12 + ], + [ + 1, + 55 + ], + [ + 1, + 58 + ], + [ + 2, + 11 + ], + [ + 2, + 56 + ], + [ + 2, + 57 + ], + [ + 3, + 10 + ], + [ + 3, + 48 + ], + [ + 3, + 51 + ], + [ + 4, + 9 + ], + [ + 4, + 49 + ], + [ + 4, + 50 + ], + [ + 5, + 8 + ], + [ + 5, + 46 + ], + [ + 5, + 53 + ], + [ + 6, + 7 + ], + [ + 6, + 47 + ], + [ + 6, + 52 + ], + [ + 7, + 6 + ], + [ + 7, + 47 + ], + [ + 7, + 52 + ], + [ + 8, + 5 + ], + [ + 8, + 46 + ], + [ + 8, + 53 + ], + [ + 9, + 4 + ], + [ + 9, + 49 + ], + [ + 9, + 50 + ], + [ + 10, + 3 + ], + [ + 10, + 48 + ], + [ + 10, + 51 + ], + [ + 11, + 2 + ], + [ + 11, + 56 + ], + [ + 11, + 57 + ], + [ + 12, + 1 + ], + [ + 12, + 55 + ], + [ + 12, + 58 + ], + [ + 13, + 20 + ], + [ + 13, + 38 + ], + [ + 13, + 43 + ], + [ + 14, + 19 + ], + [ + 14, + 37 + ], + [ + 14, + 44 + ], + [ + 15, + 18 + ], + [ + 15, + 40 + ], + [ + 15, + 41 + ], + [ + 16, + 17 + ], + [ + 16, + 39 + ], + [ + 16, + 42 + ], + [ + 17, + 16 + ], + [ + 17, + 39 + ], + [ + 17, + 42 + ], + [ + 18, + 15 + ], + [ + 18, + 40 + ], + [ + 18, + 41 + ], + [ + 19, + 14 + ], + [ + 19, + 37 + ], + [ + 19, + 44 + ], + [ + 20, + 13 + ], + [ + 20, + 38 + ], + [ + 20, + 43 + ], + [ + 21, + 28 + ], + [ + 21, + 30 + ], + [ + 21, + 35 + ], + [ + 22, + 27 + ], + [ + 22, + 29 + ], + [ + 22, + 36 + ], + [ + 23, + 26 + ], + [ + 23, + 32 + ], + [ + 23, + 33 + ], + [ + 24, + 25 + ], + [ + 24, + 31 + ], + [ + 24, + 34 + ], + [ + 25, + 24 + ], + [ + 25, + 31 + ], + [ + 25, + 34 + ], + [ + 26, + 23 + ], + [ + 26, + 32 + ], + [ + 26, + 33 + ], + [ + 27, + 22 + ], + [ + 27, + 29 + ], + [ + 27, + 36 + ], + [ + 28, + 21 + ], + [ + 28, + 30 + ], + [ + 28, + 35 + ], + [ + 29, + 22 + ], + [ + 29, + 27 + ], + [ + 29, + 36 + ], + [ + 30, + 21 + ], + [ + 30, + 28 + ], + [ + 30, + 35 + ], + [ + 31, + 24 + ], + [ + 31, + 25 + ], + [ + 31, + 34 + ], + [ + 32, + 23 + ], + [ + 32, + 26 + ], + [ + 32, + 33 + ], + [ + 33, + 23 + ], + [ + 33, + 26 + ], + [ + 33, + 32 + ], + [ + 34, + 24 + ], + [ + 34, + 25 + ], + [ + 34, + 31 + ], + [ + 35, + 21 + ], + [ + 35, + 28 + ], + [ + 35, + 30 + ], + [ + 36, + 22 + ], + [ + 36, + 27 + ], + [ + 36, + 29 + ], + [ + 37, + 14 + ], + [ + 37, + 19 + ], + [ + 37, + 44 + ], + [ + 38, + 13 + ], + [ + 38, + 20 + ], + [ + 38, + 43 + ], + [ + 39, + 16 + ], + [ + 39, + 17 + ], + [ + 39, + 42 + ], + [ + 40, + 15 + ], + [ + 40, + 18 + ], + [ + 40, + 41 + ], + [ + 41, + 15 + ], + [ + 41, + 18 + ], + [ + 41, + 40 + ], + [ + 42, + 16 + ], + [ + 42, + 17 + ], + [ + 42, + 39 + ], + [ + 43, + 13 + ], + [ + 43, + 20 + ], + [ + 43, + 38 + ], + [ + 44, + 14 + ], + [ + 44, + 19 + ], + [ + 44, + 37 + ], + [ + 45, + 0 + ], + [ + 45, + 54 + ], + [ + 45, + 59 + ], + [ + 46, + 5 + ], + [ + 46, + 8 + ], + [ + 46, + 53 + ], + [ + 47, + 6 + ], + [ + 47, + 7 + ], + [ + 47, + 52 + ], + [ + 48, + 3 + ], + [ + 48, + 10 + ], + [ + 48, + 51 + ], + [ + 49, + 4 + ], + [ + 49, + 9 + ], + [ + 49, + 50 + ], + [ + 50, + 4 + ], + [ + 50, + 9 + ], + [ + 50, + 49 + ], + [ + 51, + 3 + ], + [ + 51, + 10 + ], + [ + 51, + 48 + ], + [ + 52, + 6 + ], + [ + 52, + 7 + ], + [ + 52, + 47 + ], + [ + 53, + 5 + ], + [ + 53, + 8 + ], + [ + 53, + 46 + ], + [ + 54, + 0 + ], + [ + 54, + 45 + ], + [ + 54, + 59 + ], + [ + 55, + 1 + ], + [ + 55, + 12 + ], + [ + 55, + 58 + ], + [ + 56, + 2 + ], + [ + 56, + 11 + ], + [ + 56, + 57 + ], + [ + 57, + 2 + ], + [ + 57, + 11 + ], + [ + 57, + 56 + ], + [ + 58, + 1 + ], + [ + 58, + 12 + ], + [ + 58, + 55 + ], + [ + 59, + 0 + ], + [ + 59, + 45 + ], + [ + 59, + 54 + ] + ], + "elapsed_seconds": 7.622, + "exact_rank_checks": { + "ordered_gram_blocks_rank2": 180, + "source_spans_rank3": 60 + }, + "line_count": 60, + "maximal_clique_counts": { + "10": 2304, + "11": 1920, + "12": 640, + "7": 1920, + "8": 1920 + }, + "minimum_dual_hits": { + "1": 18, + "10": 102, + "11": 108, + "12": 108, + "2": 30, + "3": 42, + "4": 52, + "5": 60, + "6": 78, + "7": 84, + "8": 84, + "9": 92 + }, + "nonempty_cliques": 2068372, + "orthogonal_ordered_pair_count": 900, + "verification": "PASS" +} diff --git a/research/gaussian-all-clique-dual/evidence/package-tests.txt b/research/gaussian-all-clique-dual/evidence/package-tests.txt new file mode 100644 index 0000000000..7d6255aa65 --- /dev/null +++ b/research/gaussian-all-clique-dual/evidence/package-tests.txt @@ -0,0 +1,5 @@ +.......... +---------------------------------------------------------------------- +Ran 10 tests in 9.031s + +OK diff --git a/research/gaussian-all-clique-dual/evidence/primary-output.txt b/research/gaussian-all-clique-dual/evidence/primary-output.txt new file mode 100644 index 0000000000..9bb9efcbc5 --- /dev/null +++ b/research/gaussian-all-clique-dual/evidence/primary-output.txt @@ -0,0 +1 @@ +PASS_GAUSSIAN_ALL_CLIQUE_DUAL cliques=2068372 ordered_pairs=180 ceiling=40 controls=6 no_new_kappa diff --git a/research/gaussian-all-clique-dual/independent.py b/research/gaussian-all-clique-dual/independent.py new file mode 100644 index 0000000000..df28e3b36d --- /dev/null +++ b/research/gaussian-all-clique-dual/independent.py @@ -0,0 +1,432 @@ +#!/usr/bin/env python3 +"""Independent finite replay of the Gaussian E8 all-clique dual. + +Only Python's standard library is used. No primary or predecessor executable +code is imported. Geometry is reconstructed from the doubled real E8 roots; +Gaussian ranks are checked by direct Gaussian-rational Fraction elimination. +All nonempty cliques are obtained as deduplicated subsets of Bron--Kerbosch +maximal cliques, rather than by the primary replay's ordered clique recursion. + +Prepared for William Lawyer with substantial OpenAI Codex assistance. Separate +AI implementation is not independent human review or a formal proof assistant. +""" + +from __future__ import annotations + +import argparse +from collections import Counter +from fractions import Fraction +import hashlib +from itertools import combinations, product +import json +from pathlib import Path +import struct +import time + + +Gaussian = tuple[int, int] +Vector = tuple[Gaussian, ...] + + +def require(condition: bool, message: str) -> None: + # Deliberately not an assert: optimized Python must retain failure detection. + if not condition: + raise ValueError(message) + + +def e8_root_valid(root: tuple[int, ...]) -> bool: + """Membership in the *doubled* E8 root system, not just its norm shell.""" + if len(root) != 8: + return False + if all(x in (-1, 1) for x in root): + return sum(x < 0 for x in root) % 2 == 0 + return (sum(x != 0 for x in root) == 2 + and all(x in (-2, 0, 2) for x in root)) + + +def doubled_roots() -> set[tuple[int, ...]]: + roots: set[tuple[int, ...]] = set() + for support in combinations(range(8), 2): + for signs in product((-2, 2), repeat=2): + row = [0] * 8 + for position, value in zip(support, signs): + row[position] = value + roots.add(tuple(row)) + for row in product((-1, 1), repeat=8): + if sum(x == -1 for x in row) % 2 == 0: + roots.add(row) + require(len(roots) == 240, "Doubled E8 root count changed") + require(all(e8_root_valid(row) for row in roots), "Invalid E8 root") + return roots + + +def rotate_i(root: tuple[int, ...]) -> tuple[int, ...]: + return tuple(value for j in range(0, 8, 2) + for value in (-root[j + 1], root[j])) + + +def line_representative(root: tuple[int, ...]) -> tuple[int, ...]: + phase_i = rotate_i(root) + return min(root, phase_i, tuple(-x for x in root), + tuple(-x for x in phase_i)) + + +def hermitian(left: Vector, right: Vector) -> Gaussian: + require(len(left) == len(right), "Mismatched vector lengths") + # conj(a+ib)(c+id) = ac+bd + i(ad-bc). + return (sum(a * c + b * d for (a, b), (c, d) in zip(left, right)), + sum(a * d - b * c for (a, b), (c, d) in zip(left, right))) + + +def indices(mask: int): + while mask: + bit = mask & -mask + yield bit.bit_length() - 1 + mask ^= bit + + +def gaussian_rank(matrix: list[list[Gaussian]]) -> int: + """Exact rank over Q(i), using direct pairs of rational components. + + This does not realify the matrix or use the primary replay's real RREF. + Every elimination quotient is evaluated in the Gaussian rational field. + """ + if not matrix: + return 0 + width = len(matrix[0]) + require(all(len(row) == width for row in matrix), "Ragged Gaussian matrix") + rows = [[(Fraction(real), Fraction(imaginary)) for real, imaginary in row] + for row in matrix] + pivot_row = 0 + for column in range(width): + pivot = next((j for j in range(pivot_row, len(rows)) + if rows[j][column] != (0, 0)), None) + if pivot is None: + continue + rows[pivot_row], rows[pivot] = rows[pivot], rows[pivot_row] + row = rows[pivot_row] + for j in range(pivot_row + 1, len(rows)): + if rows[j][column] != (0, 0): + a, b = rows[j][column] + c, d = row[column] + denominator = c * c + d * d + factor = ((a * c + b * d) / denominator, + (b * c - a * d) / denominator) + rows[j][column] = (Fraction(0), Fraction(0)) + f, g = factor + for k in range(column + 1, width): + c, d = row[k] + a, b = rows[j][k] + rows[j][k] = (a - (f * c - g * d), + b - (f * d + g * c)) + pivot_row += 1 + if pivot_row == len(rows): + break + return pivot_row + + +def build_geometry() -> tuple[list[Vector], list[int], list[int]]: + roots = doubled_roots() + representatives = sorted({line_representative(row) for row in roots}) + require(len(representatives) == 60, "Gaussian line count changed") + for row in representatives: + orbit = {row, rotate_i(row), tuple(-x for x in row), + tuple(-x for x in rotate_i(row))} + require(len(orbit) == 4 and orbit <= roots, + "Gaussian phase orbit does not consist of four E8 roots") + lines = [tuple((row[j], row[j + 1]) for j in range(0, 8, 2)) + for row in representatives] + perpendiculars = [sum(1 << j for j, right in enumerate(lines) + if hermitian(left, right) == (0, 0)) + for left in lines] + universe = (1 << len(lines)) - 1 + nonorthogonal = [universe ^ perpendiculars[i] ^ (1 << i) + for i in range(len(lines))] + verify_geometry(lines, perpendiculars, nonorthogonal) + return lines, perpendiculars, nonorthogonal + + +def verify_geometry(lines: list[Vector], perpendiculars: list[int], + nonorthogonal: list[int]) -> None: + require(len(lines) == len(perpendiculars) == len(nonorthogonal) == 60, + "Geometry arrays must contain 60 lines") + universe = (1 << 60) - 1 + for i, left in enumerate(lines): + require(hermitian(left, left) == (8, 0), "Invalid root norm") + require(perpendiculars[i].bit_count() == 15, + "Hyperplane does not contain 15 line indices") + require(perpendiculars[i] & (1 << i) == 0, "Self orthogonality") + require(nonorthogonal[i] == universe ^ perpendiculars[i] ^ (1 << i), + "Nonorthogonality graph complement is incorrect") + for j, right in enumerate(lines): + if i < j: + real, imaginary = hermitian(left, right) + require(64 - real * real - imaginary * imaginary > 0, + "Two representatives are the same Gaussian line") + expected = hermitian(left, right) == (0, 0) + require(bool(perpendiculars[i] & (1 << j)) == expected, + "Orthogonality edge does not match exact Hermitian form") + require(bool(perpendiculars[j] & (1 << i)) == expected, + "Orthogonality graph is not symmetric") + + +def ordered_dual_pairs(perpendiculars: list[int]) -> list[tuple[int, int]]: + return [(i, j) for i, neighbors in enumerate(perpendiculars) + for j in indices(neighbors) + if (neighbors & perpendiculars[j]).bit_count() == 6] + + +def geometry_ranks(lines: list[Vector], perpendiculars: list[int], + dual_pairs: list[tuple[int, int]]) -> dict[str, int]: + spans = [list(indices(mask)) for mask in perpendiculars] + source_rank = Counter(gaussian_rank([list(lines[i]) for i in support]) + for support in spans) + require(source_rank == {3: 60}, "Hyperplane source span is not dimension3") + pairing_rank = Counter() + for first, second in dual_pairs: + gram = [[hermitian(lines[i], lines[j]) for j in spans[second]] + for i in spans[first]] + pairing_rank[gaussian_rank(gram)] += 1 + require(pairing_rank == {2: 180}, "Selected hyperplane pairing rank changed") + return {"source_spans_rank3": source_rank[3], + "ordered_gram_blocks_rank2": pairing_rank[2]} + + +def maximal_cliques(adjacency: list[int]) -> list[int]: + """Bron--Kerbosch pivot recursion; every returned clique is maximal.""" + found: list[int] = [] + + def visit(chosen: int, possible: int, excluded: int) -> None: + if not possible and not excluded: + found.append(chosen) + return + candidates = possible | excluded + pivot = max(indices(candidates), + key=lambda i: (possible & adjacency[i]).bit_count()) + branch = possible & ~adjacency[pivot] + while branch: + bit = branch & -branch + vertex = bit.bit_length() - 1 + visit(chosen | bit, possible & adjacency[vertex], + excluded & adjacency[vertex]) + possible ^= bit + excluded |= bit + branch ^= bit + + visit(0, (1 << len(adjacency)) - 1, 0) + require(len(found) == len(set(found)), "Duplicate maximal cliques") + for mask in found: + require(is_clique(mask, adjacency), "Malformed maximal clique") + common = (1 << len(adjacency)) - 1 + for i in indices(mask): + common &= adjacency[i] + require(common == 0, "Returned clique is extendible") + return sorted(found) + + +def is_clique(mask: int, adjacency: list[int]) -> bool: + if mask < 0 or mask >> len(adjacency): + return False + for i in indices(mask): + if (mask ^ (1 << i)) & ~adjacency[i]: + return False + return True + + +def all_cliques(maximals: list[int]) -> set[int]: + """A finite graph clique extends to a maximal one: enumerate all subsets.""" + result: set[int] = set() + for mask in maximals: + subset = mask + while subset: + result.add(subset) + subset = (subset - 1) & mask + return result + + +def dual_incidence(perpendiculars: list[int], + pairs: list[tuple[int, int]]) -> tuple[list[int], list[int]]: + first = [0] * len(perpendiculars) + second = [0] * len(perpendiculars) + for index, (u, v) in enumerate(pairs): + for i in indices(perpendiculars[u]): + first[i] |= 1 << index + for i in indices(perpendiculars[v]): + second[i] |= 1 << index + return first, second + + +def hit_count(mask: int, incidence: tuple[list[int], list[int]]) -> int: + left = right = 0 + first, second = incidence + for i in indices(mask): + left |= first[i] + right |= second[i] + return (left & right).bit_count() + + +def expected_failure(action, message: str) -> None: + try: + action() + except ValueError: + return + raise ValueError("Negative control was accepted: " + message) + + +def small_graph_domain_controls() -> int: + """Compare BK/subsets with brute force for all labelled graphs of order1..5.""" + checked = 0 + for order in range(1, 6): + edges = list(combinations(range(order), 2)) + for edge_mask in range(1 << len(edges)): + adjacency = [0] * order + for position, (i, j) in enumerate(edges): + if edge_mask & (1 << position): + adjacency[i] |= 1 << j + adjacency[j] |= 1 << i + brute_force = {mask for mask in range(1, 1 << order) + if is_clique(mask, adjacency)} + reconstructed = all_cliques(maximal_cliques(adjacency)) + require(reconstructed == brute_force, + f"Small graph domain mismatch: n={order}, edges={edge_mask}") + checked += 1 + return checked + + +def controls(lines: list[Vector], perpendiculars: list[int], + adjacency: list[int], pairs: list[tuple[int, int]], + maximum_clique: int) -> dict[str, object]: + require(hermitian(((1, 0), (0, 1)), ((0, 1), (1, 0))) == (0, 0), + "Hermitian conjugation control failed") + require(hermitian(((1, 0),), ((0, 1),)) == (0, 1), + "Hermitian imaginary-sign control failed") + require(gaussian_rank([[(1, 0), (0, 1)], [(0, 1), (-1, 0)]]) == 1, + "Gaussian-dependent rank control failed") + require(gaussian_rank([[(1, 0), (0, 1)], [(0, 1), (1, 0)]]) == 2, + "Gaussian-independent rank control failed") + root = (1,) * 8 + corrupt_root = (-1,) + root[1:] + require(e8_root_valid(root) and not e8_root_valid(corrupt_root), + "Odd root-sign corruption was not rejected") + orthogonal = (0, next(indices(perpendiculars[0]))) + require(not is_clique((1 << orthogonal[0]) | (1 << orthogonal[1]), + adjacency), "Orthogonal pair admitted as clique") + bad_perps = perpendiculars.copy() + bad_perps[0] ^= 1 << orthogonal[1] + expected_failure(lambda: verify_geometry(lines, bad_perps, adjacency), + "deleted orthogonality edge") + original = [(i, j) for i, mask in enumerate(perpendiculars) + for j in indices(mask)] + old_singleton_hits = hit_count(1, dual_incidence(perpendiculars, original)) + require(old_singleton_hits == 42 and old_singleton_hits < 45, + "Original 900-pair singleton counterexample disappeared") + hits = hit_count(maximum_clique, dual_incidence(perpendiculars, pairs)) + require(hits < 10 * maximum_clique.bit_count(), + "Stronger multiplier 1/10 negative control did not fail") + # Removing a contributing pair invalidates a tight size12 dual inequality. + contributing = next(k for k, (u, v) in enumerate(pairs) + if maximum_clique & perpendiculars[u] + and maximum_clique & perpendiculars[v]) + reduced = pairs[:contributing] + pairs[contributing + 1:] + reduced_hits = hit_count(maximum_clique, + dual_incidence(perpendiculars, reduced)) + require(hits == 9 * maximum_clique.bit_count() + and reduced_hits < 9 * maximum_clique.bit_count(), + "Dropped-dual-pair negative control did not fail") + return {"orthogonal_pair_rejected": list(orthogonal), + "deleted_edge_rejected": True, + "odd_root_sign_rejected": True, + "hermitian_sign_controls": 2, + "gaussian_rank_controls": 2, + "all_labelled_graphs_order1_through5": small_graph_domain_controls(), + "original900_singleton_hits": old_singleton_hits, + "original900_required_singleton_hits": 45, + "multiplier1_over10_rejected": True, + "dropped_dual_pair_rejected": True, + "dropped_pair_hits": reduced_hits} + + +MATHEMATICAL_FIELDS = ("line_count", "orthogonal_ordered_pair_count", + "dual_pair_count", "clique_counts", "minimum_dual_hits", + "all_cliques_sha256", "dual_pairs", "dual_multiplier", "ceiling") + + +def compare_certificate(result: dict, certificate: dict) -> None: + for field in MATHEMATICAL_FIELDS: + require(field in certificate, "Missing certificate field: " + field) + require(certificate[field] == result[field], + "Independent certificate mismatch: " + field) + + +def replay() -> dict: + lines, perpendiculars, adjacency = build_geometry() + pairs = ordered_dual_pairs(perpendiculars) + require(len(pairs) == 180, "Selected dual is not 180 ordered pairs") + ranks = geometry_ranks(lines, perpendiculars, pairs) + maximals = maximal_cliques(adjacency) + cliques = all_cliques(maximals) + incidence = dual_incidence(perpendiculars, pairs) + counts: Counter[int] = Counter() + minima: dict[int, int] = {} + digest = hashlib.sha256() + for mask in sorted(cliques): + size = mask.bit_count() + hits = hit_count(mask, incidence) + require(hits >= 9 * size, + f"All-clique dual fails: mask={mask}, size={size}, hits={hits}") + counts[size] += 1 + minima[size] = min(minima.get(size, len(pairs) + 1), hits) + digest.update(struct.pack(" None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--certificate", type=Path, + default=Path(__file__).with_name("CERTIFICATE.json")) + parser.add_argument("--compute-only", action="store_true", + help="emit recomputed evidence without comparing a fixture") + parser.add_argument("--show-report", action="store_true", + help="print the complete independent evidence") + arguments = parser.parse_args() + started = time.perf_counter() + result = replay() + if not arguments.compute_only: + certificate = json.loads(arguments.certificate.read_text(encoding="utf-8")) + compare_certificate(result, certificate) + result["certificate_mathematical_fields_match"] = True + # A replayed claim must reject changed published evidence. + changed = dict(certificate) + changed["all_cliques_sha256"] = "0" * 64 + expected_failure(lambda: compare_certificate(result, changed), + "corrupted clique-set digest") + result["controls"]["corrupted_certificate_digest_rejected"] = True + result["verification"] = "PASS" + result["elapsed_seconds"] = round(time.perf_counter() - started, 3) + if arguments.show_report or arguments.compute_only: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + print("PASS_INDEPENDENT_GAUSSIAN_ALL_CLIQUE_DUAL cliques=" + + str(result["nonempty_cliques"]) + + " ordered_pairs=180 ceiling=40 graphs=1099 no_new_kappa") + + +if __name__ == "__main__": + main() diff --git a/research/gaussian-all-clique-dual/test_package.py b/research/gaussian-all-clique-dual/test_package.py new file mode 100644 index 0000000000..6604cb63d2 --- /dev/null +++ b/research/gaussian-all-clique-dual/test_package.py @@ -0,0 +1,131 @@ +"""Scope, arithmetic, enumeration and portable failure-detection controls.""" +from itertools import combinations +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +import independent +import verify + +HERE = Path(__file__).resolve().parent + + +class MathematicalControls(unittest.TestCase): + def test_primary_clique_domain_all_small_graphs(self): + checked = 0 + for n in range(1, 6): + edges = list(combinations(range(n), 2)) + for encoding in range(1 << len(edges)): + adjacency = [0] * n + for k, (i, j) in enumerate(edges): + if encoding >> k & 1: + adjacency[i] |= 1 << j + adjacency[j] |= 1 << i + expected = set() + for mask in range(1, 1 << n): + members = [i for i in range(n) if mask >> i & 1] + if all(adjacency[i] >> j & 1 for i, j in combinations(members, 2)): + expected.add(mask) + actual = list(verify.all_cliques(adjacency)) + self.assertEqual(len(actual), len(set(actual))) + self.assertEqual(set(actual), expected) + checked += 1 + self.assertEqual(checked, 1099) + + def test_two_rank_implementations(self): + # Complex dependence differs from dependence of real coordinate rows. + matrix = [[(1, 0), (0, 1)], [(0, 1), (-1, 0)]] + self.assertEqual(independent.gaussian_rank(matrix), 1) + realified = [] + for row in matrix: + realified.append([x for a, b in row for x in (a, -b)]) + realified.append([x for a, b in row for x in (b, a)]) + self.assertEqual(len(verify.reduced_basis(realified)), 2) + + def test_wrong_original_and_stronger_duals_rejected(self): + with self.assertRaisesRegex(ValueError, 'does not dominate'): + verify.check_dual_hit(1, 42, 45) + with self.assertRaisesRegex(ValueError, 'does not dominate'): + verify.check_dual_hit(12, 108, 10) + verify.check_dual_hit(12, 108, 9) + + def test_false_frame_partition_rejected(self): + _, lines = verify.roots_and_lines() + _, orthogonal, dual, _ = verify.graph_data(lines) + wrong = list(dual) + wrong[0] ^= 1 << next(verify.bits(wrong[0])) + with self.assertRaises(ValueError): + verify.frames_from_dual(wrong) + wrong = list(orthogonal) + wrong[0] |= 1 + with self.assertRaises(ValueError): + verify.check_orthogonal_graph(wrong) + + def test_nonorthogonal_normals_have_different_charge(self): + _, lines = verify.roots_and_lines() + adjacency, orthogonal, _, _ = verify.graph_data(lines) + j = next(verify.bits(adjacency[0])) + with self.assertRaisesRegex(ValueError, 'wrong rational pairing rank'): + verify.check_geometry(lines, orthogonal, ((0, j),)) + + def test_claim_fields_are_checked_independently(self): + certificate = json.loads((HERE / 'CERTIFICATE.json').read_text()) + result = {key: certificate[key] for key in independent.MATHEMATICAL_FIELDS} + for field, value in [('ceiling', '39'), ('dual_multiplier', '1/10'), + ('all_cliques_sha256', '0' * 64), ('dual_pairs', [])]: + damaged = dict(certificate, **{field: value}) + with self.assertRaisesRegex(ValueError, field): + independent.compare_certificate(result, damaged) + + +class PortableControls(unittest.TestCase): + def setUp(self): + self.temporary = tempfile.TemporaryDirectory() + self.folder = Path(self.temporary.name) + self.package = self.folder / 'relocated' + shutil.copytree(HERE, self.package, ignore=shutil.ignore_patterns('__pycache__')) + + def tearDown(self): + self.temporary.cleanup() + + def run_script(self, script, *arguments): + return subprocess.run([sys.executable, '-I', '-O', '-B', + str(self.package / script), *map(str, arguments)], + cwd=self.folder, capture_output=True, text=True, timeout=120) + + def test_relocated_optimized_independent_replay(self): + result = self.run_script('independent.py') + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn('PASS_INDEPENDENT_GAUSSIAN_ALL_CLIQUE_DUAL', result.stdout) + + def test_changed_retained_source_rejected(self): + source = self.package / 'vendor/pr738-PROOF.md' + source.write_bytes(source.read_bytes() + b'corruption\n') + result = self.run_script('verify.py') + self.assertNotEqual(result.returncode, 0) + self.assertIn('retained source mismatch', result.stderr) + + def test_escaping_source_path_rejected(self): + path = self.package / 'SOURCES.json' + sources = json.loads(path.read_text()) + sources['retained_files']['../outside'] = next(iter(sources['retained_files'].values())) + path.write_text(json.dumps(sources)) + result = self.run_script('verify.py') + self.assertNotEqual(result.returncode, 0) + self.assertIn('invalid retained source path', result.stderr) + + def test_existing_output_preserved(self): + existing = self.folder / 'existing.json' + existing.write_bytes(b'preserve this exact content') + result = self.run_script('verify.py', '--output', existing) + self.assertNotEqual(result.returncode, 0) + self.assertIn('output file already exists', result.stderr) + self.assertEqual(existing.read_bytes(), b'preserve this exact content') + + +if __name__ == '__main__': + unittest.main() diff --git a/research/gaussian-all-clique-dual/vendor/pr620-extension-REPORT.md b/research/gaussian-all-clique-dual/vendor/pr620-extension-REPORT.md new file mode 100644 index 0000000000..1a766e3655 --- /dev/null +++ b/research/gaussian-all-clique-dual/vendor/pr620-extension-REPORT.md @@ -0,0 +1,57 @@ +# S1: E8 over extension rings and other line systems (stopped early because the budget ran out; no kappa claim) + +Scripts are in $SP/s1/ and run with $SP/venv/bin/python -B from inside that directory. The package/ directory was not written. + +## Reduction (argued) +- **Bit side.** The cost is rank_Q of the frame changes. A Q(i)-line costs 2 Q-ranks, so a K-linear unit is a rank-k unit with k = [K:Q] and h = k·w_K. +- **The ceiling under this scaling.** X depends only on (s, w = h/k, x/k) (§A.2, general k). The window does "halve" (8 -> 4), but v falls by the same factor: 120 real lines become 60 Q(i)-lines. +- **What decides the comparison.** It comes down to (w_K, x_K = Σ rank_K / v), with the F2 decoder pattern taken from K-orthogonality. +- **Q(i) is free on the bit side.** No ring rule (Lemma λ) blocks Q(i) there: the payload is F2 and the frames are Q-linear. + +## Numbers (exact) +- **Gaussian E8** (J = i on coordinate pairs; preserves E8; checked) + - 60 lines, w = 4. + - Each line is non-orthogonal to 44 others. + - α (largest pairwise non-orthogonal set) = 12. + - F2 minrank (asymmetric allowed, SAT with clique gauge) = 15: c = 13 and 14 are UNSAT, c = 15 is SAT. 15 = v/w, the frame-partition decoder. + - Hyperplane flats: 60 of size 15, 480 of size 6, 960 of size 4. +- **Eisenstein E8** (fixed-point-free order-3 element from 4 orthogonal A2's; Witting configuration) + - 40 lines, w = 4, non-orthogonal degree 27, α = 7. + - F2 minrank = 10: c = 7, 8, 9 are UNSAT, c = 10 is SAT. 10 = v/w. +- **Hurwitz E8** (left multiplication by i, j) + - 10 lines in H^2, w = 2, each line orthogonal to exactly one other, α = 5, minrank 5 = v/w. +- **Copy cost.** Symmetric decoders, exact CP-SAT with cost = dim span A_j, searched 900 s (not proven optimal): + - Gaussian (c ≤ 20): best found 60, so x_K = 1.0. Proven lower bound only 9 (x_K ≥ 0.15). + - Eisenstein (c ≤ 16): best found 40, so x_K = 1.0. Lower bound 9 (x_K ≥ 0.225). + - Hurwitz: + - Symmetric optimum is 10 (x_K = 1.0, proven OPTIMAL). + - The asymmetric D_j-relaxation gives only 2, and that relaxation is too weak. + - The exact SAT run with the Theorem-C cost (costs 8/9/10) did not finish, so the Hurwitz asymmetric case is **open**. +- **Under the README's own E8 premise** (cst = minrank × full in-cap clique rank, the same premise as E8's 72): Gaussian, Eisenstein and Hurwitz all have x_K = minrank·w/v = **1.0**. Then D/k = (s−1)v − s·v < 0 at every s, so there is **no saving at all**. +- **Threshold to beat bit E8** (X* = 6.0005e-3, float screen fx.py): x_K < ~0.71 at w = 4, < ~0.86 at w = 2, < ~0.64 at w = 6. +- **Structural finding.** The cross-field gain of E8 (minrank 9 < v/w = 15) disappears over Q(i), Q(ω) and H: in every extension view minrank = v/w exactly. +- **G34 / Coxeter–Todd K12.** Built exactly as {x ∈ Z[ω]^6 : x_i ≡ x_j mod θ, Σ x_i ≡ 0 mod 3}: 756 minimal vectors, 126 lines. + - w = 6, non-orthogonal degree 80, α = 15. + - Even at minrank = α, x_K ≥ 90/126 = 0.714 > 0.64, so it loses under the premise. The minrank itself was not run. +- **Complex side** (argued). Rules out F4/Eisenstein F2-labels and Gaussian F2-labels: + - **F4 / Eisenstein labels.** A Hermitian form over F4 has an alternating F2 trace form (Tr h(x,x) = 0), so there are no odd-norm residuals. This breaks the phase calculus (orthonormal kernel basis; Lemma λ consequence). It is the first broken rule. + - **Gaussian labels.** Z[i]/(1+i) = F2, so there is no extension. + - **A Q(i)-valued decoder** (Hermitian Gram, 4 centres) forces F2 window = the Gaussian-pattern minrank = 15 on 60 ports, or ≥ 24 on the 120 real ports (clique of r, ir pairs). Not evaluated further. +- **Side finding (b), checked with the float screen only.** The upstream Alon triple family (v = C(h,3), cst = h² bit / h(h+1) complex) has a higher **ceiling** than E8: + - X* = 7.39e-3 (bit, h = 24) and 7.16e-3 (complex, h = 24), at s = 3. + - Generalised Alon sets (7-subsets, λ = 3) would push the ceiling higher still. + - So X* alone does not rank unit families; helper cost decides (per-target neighbour count z = 3·C(h−3,2) = 630 at h = 24, against 63 for E8). + - This was the pre-E8 family (h = 23/25/28 audits in docs/research). + - Task (c), the helper-floor estimate, was not done. + +## Reproduce +- explore4.py: v, degree, α for the three views. +- minrank_any.py {Gauss|Eisen|Hurwitz|K12} [cmin]: minrank SAT. +- costexact.py {Gauss|Eisen} cmax 1 secs: exact cost CP-SAT (needs flats_*.pkl, built by costlb.py). +- k12.py: G34. +- fx.py: float X screen (certify with skel.X before publishing). + +## Open and next steps +1. A real lower bound Σ_j dim span A_j ≥ 0.71·v (Gaussian) for decoders with more than minrank totals. CP-SAT bounds stay at 9; a structural argument is needed. Same open status as E8's 72. +2. Finish the Hurwitz asymmetric SAT (hurwitz_exact.py, cost ≤ 8/9/10). +3. Certify the triple-family X* with skel.X, and estimate helpers via d1 cover numbers. The triple cover number is 2 by the argued two-hyperplane cover. diff --git a/research/gaussian-all-clique-dual/vendor/pr738-PROOF.md b/research/gaussian-all-clique-dual/vendor/pr738-PROOF.md new file mode 100644 index 0000000000..748e632439 --- /dev/null +++ b/research/gaussian-all-clique-dual/vendor/pr738-PROOF.md @@ -0,0 +1,170 @@ +# Weighted clique certificate for scalar Gaussian decoders + +The exact certificate gives a copy-charge lower bound of **40 Gaussian rank +units**, or **80 rational rank units**, for every decoder in the class below. +It does not assert a new multiplication bound. + +Let V index the 60 Gaussian lines obtained from the E8 roots in Q^8 by the +complex structure J with J e_(2a) = e_(2a+1) and +J e_(2a+1) = -e_(2a), for a=0,...,3. For a line set S, let X_S be the +rational span of its representatives and their J-images. Write + + c(R,A) = rank_Q(V_R V_A^T) / 2, + +where V_S has rows spanning X_S. This is the Gaussian pairing rank, in +Gaussian rather than rational rank units. It is not the dimension of the +source span, and it is not the binary rank of a decoder submatrix. + +Consider any finite scalar-total binary factorization + + B = sum_j 1_(R_j) 1_(A_j)^T over F2, + +with B_tt=1 and B_ts=0 when distinct Gaussian lines t,s are nonorthogonal. +Reader/source supports may differ; orthogonal off-diagonal entries are free. +The abstract copy charge is C=sum_j c(R_j,A_j). + +## Certificate theorem + +Let K be any finite collection of pairwise nonorthogonal cliques. Assign +nonnegative rational weights lambda_Q to its cliques. Suppose that, for +every ordered pair of flats F,G of the Gaussian line matroid, + + sum_(Q in K) lambda_Q [Q meets F and Q meets G] <= c(F,G). (1) + +Then every fitting scalar-total factorization satisfies + + C >= sum_(Q in K) lambda_Q |Q|. (2) + +Proof: the fitting constraints force B[Q,Q]=I_|Q|. A rectangle restricted +to Q has binary rank one exactly when both supports meet Q, and has rank +zero otherwise. Binary rank subadditivity therefore gives + + |Q| <= sum_j [Q meets R_j and Q meets A_j]. + +Multiply by lambda_Q, sum over Q, and apply (1) to each term. The reduction +from arbitrary supports to flats in that last step is justified below. +There is no assumption on the binary rank of B, the number of totals, or +symmetry of the factorization. Zero-charge terms are allowed. + +## Why all flat pairs suffice + +Define cl(S)={t in V: X_{t} is contained in X_S}. This closure contains S +and spans exactly X_S. Consequently + + c(cl(R),cl(A)) = c(R,A). + +Each clique-hit indicator is nondecreasing when either support grows, so +its value on (R,A) is at most its value on (cl(R),cl(A)). Thus (1), checked +on all flat pairs, covers every one of the 2^60 by 2^60 support pairs. +This is a completeness argument, not an inference from sampled supports. + +All flats can be generated starting with the empty flat and adjoining one +line outside a previously generated flat, followed by exact closure. +Completeness follows by induction on rank: choose a line basis of any +nonempty flat, remove its last line, and use the lower-rank closure as its +parent. The rank is at most four, so this process terminates after rank +four. The verifier checks exact closure, Gaussian invariance, and that the +basis equals the canonical span of the stated lines. An independent Fraction +elimination checks fixed rank cases and the sharp witness's Gram matrix. + +For zero pairing rank the left side of (1) is automatically zero. If a +clique met both supports, a chosen reader/source pair would either be the +same nonzero line or two distinct nonorthogonal lines. Either choice has a +nonzero Gram block, contradicting zero pairing rank. + +## Uniform weights and their exact limitation + +For equal-size cliques of size q, let n=|K| and + + h(F,G) = number of cliques meeting both F and G; + rho = max_(c(F,G)>0) h(F,G)/c(F,G). + +The largest valid uniform weight is exactly 1/rho, and the resulting floor +is n*q/rho. An exhaustive exact maximum over flat pairs therefore certifies +both the bound and optimality within this uniform-weight method. A pair +attaining rho is a useful witness against every larger uniform weight. + +Here n=640, q=12, and rho=192. The committed certificate records all 2,272 +flats, including the empty flat, and all 2,579,856 unordered pairs of nonempty +flats. Symmetry of both the Gram rank and joint-hit count covers both orders. +Empty supports have zero charge and zero hits. + +For a pair with h>0 and flat ranks r,s, the proof above gives c>=1. +Sylvester's rank inequality on the real Gram product gives c>=r+s-4. +The verifier therefore accepts h<=192 max(1,r+s-4) directly. It computes +the exact rational Gram rank for every remaining pair. This partitions the +entire domain into 2,725 zero-hit pairs, 1,827,741 rank-bound pairs and +749,390 exact-rank pairs. No candidate is skipped on a numerical tolerance. + +With the lexicographic line numbering in `geometry.py`, the pair + + F = {0,1,2,11,12,45} + G = {0,3,4,5,6,7,8,9,10,54,55,56,57,58,59} + +has ranks 2 and 3, pairing rank 1, and joint-hit count 192. Thus 1/192 is +valid and is the largest uniform weight on these 640 cliques. Applying the +certificate theorem gives C>=640*12/192=40. The witness is also a concrete +reason that replacing pairing rank by a support's dimension would be invalid. +This sharpness concerns the certificate method; it does not exhibit a +cost-40 decoder. + +There is also a limitation independent of the computed maximum. Take both +supports to be the full ground set. Its cost is four and it meets every +nonempty clique, so every feasible system of nonnegative clique weights +must satisfy sum_Q lambda_Q <= 4. If the maximum nonorthogonal clique size +is 12, no such weighted-clique certificate can prove a floor larger than +48, even with nonuniform weights or with smaller cliques included. This is +a limitation of this certificate method, not an upper bound on the true +minimum copy charge. + +For comparison, every fitting B has an abstract decomposition of cost 60: +take one rectangle per row, with R={t} and A equal to that row's nonzero +support. Its Gram pairing has rank one because B_tt=1, while every other +possible nonzero entry in that row lies on a line orthogonal to t. This +upper bound does not establish a physical supplier or attainability without +additional expenses. + +## Conditional three-stage consequence + +Under the separate Dfc accounting of #595 and the Gaussian scaling argued +in #620, v=60 and each line has rational rank k=2. For T replicas and s +stages, the optimistic deficit therefore satisfies + + D/T = (s-1) v k - s cst <= 120(s-1) - 80s = 40s-120. + +At s=3 this is nonpositive. Under the same pressure identity with +nonnegative paid children and fallback cost, a positive supplier saving +requires positive deficit. Thus this three-stage Gaussian format cannot +give a positive saving, even before charging helper preparation, source +access, frame changes, restoration, or recursive children. Those required +costs cannot repair a nonpositive optimistic deficit. + +The bound allows positive deficit at s>=5. It does not decide the best +decoder cost, construct a complete supplier, or price the other supplier +and outer assembly. No kappa improvement follows. Changing stage accounting +or allowing sub-line/vector-valued operations is outside this consequence. + +## Provenance and scope + +The Gaussian object above is exactly the object in Joel Pulikkan / +GamingPuzzled's #620 `gauss_geom.py`: its J is also exactly the block-diagonal +`Li` in `algebra_lines.py: left_quat()`. Each rational Gaussian root line +contains its four roots r,Jr,-r,-Jr; changing representatives only permutes +the line indices and multiplies rows by invertible Gaussian scalars. + +The weighted-clique argument extends the method of Douglas R. Colkitt / +Mister-Meeseeks' concurrent PR #703, at commit +358383e2f1b0f292d4d6eb897c06fd8558a4f5e6. That work proves a sharp bound for +the ten Hurwitz lines using 32 orthogonal-pair transversals. Its numerical +Hurwitz bound is not imported here. + +The result concerns whole Gaussian-line supports, scalar binary totals and +the declared pairing-rank charge. It does not cover arbitrary rational +sub-line supports, vector-linear totals, modified fitting patterns, or +other geometries. Translating it into a supplier obstruction requires the +repository's separate frame and accounting assumptions. Finite exact replay +is not a proof-assistant formalization of the multiplication theorem. + +Prepared by Sagar Thakrar (@thakrarsagar) with substantial OpenAI Codex +assistance in the proof, implementation, review and documentation. +Apache-2.0, as specified by the repository license. diff --git a/research/gaussian-all-clique-dual/vendor/pr770-NOTICE.md b/research/gaussian-all-clique-dual/vendor/pr770-NOTICE.md new file mode 100644 index 0000000000..1cbb79cde4 --- /dev/null +++ b/research/gaussian-all-clique-dual/vendor/pr770-NOTICE.md @@ -0,0 +1,72 @@ +# Attribution, source status and license + +Prepared for **@chinmayarvind23** with substantial **OpenAI Codex** assistance +in research selection, proof development, implementation, automated checking, +code review and documentation. Separate AI agents developed the primary and +independent replays. This does not constitute independent human review, and +no human-only authorship or human review is claimed. + +**Concurrent result.** During the final overlap refresh, after this package's +proof and code had been developed, we located **Sagar Thakrar / @thakrarsagar's +[PR #738](https://github.com/CrocSwap/integer-mult-bounds/pull/738)** at +`9671c5d72f3119ba26f3774f40aa7130c67bcf77`. That contribution already states +the same Gaussian copy floor of 40, the closure reduction, the uniform +640-clique certificate, its uniform-weight sharpness and the interval +[40,60]. It was prepared with substantial OpenAI Codex assistance. Those +overlapping conclusions are credited here; this package does not claim a +new discovery of the floor or treat its inclusion of empty-support pairs +as a mathematical advance. No #738 executable code was imported or used +to produce our replays. + +The resulting scope is **independent verification plus an extension**. +The inspected #738 proof gives a ceiling of 48 for general nonnegative +clique weights. Section 5 of our [proof](PROOF.md) strengthens that ceiling +to 40 for all nonnegative weighted inclusion-maximal-clique certificates, +including mixtures of different maximal-clique sizes. It does not address +certificates using non-maximal cliques. The pinned +[#738 proof](https://github.com/CrocSwap/integer-mult-bounds/blob/9671c5d72f3119ba26f3774f40aa7130c67bcf77/research/gaussian-clique-copy-bound/PROOF.md) +documents the comparison rather than relying on its PR summary alone. + +The Gaussian E8 line configuration, extension-ring reduction, decoder +question, symmetric cost-60 result and open copy-floor problem come from +**Joel Pulikkan / GamingPuzzled's +[PR #620](https://github.com/CrocSwap/integer-mult-bounds/pull/620)**, prepared +with Claude Opus 5.5 assistance. Its retained extension-ring files are pinned +in [SOURCES.json](SOURCES.json). This contribution does not claim that +geometry, problem formulation or upper bound as new. + +The weighted-clique rank-averaging approach follows **Douglas R. Colkitt / +Mister-Meeseeks' [PR #703](https://github.com/CrocSwap/integer-mult-bounds/pull/703)** +for the ten Hurwitz E8 lines. The inspected head is +`358383e2f1b0f292d4d6eb897c06fd8558a4f5e6`. Its +[original proof](https://github.com/CrocSwap/integer-mult-bounds/blob/358383e2f1b0f292d4d6eb897c06fd8558a4f5e6/research/hurwitz-asymmetric-copy-floor/PROOF.md) +and [original notice](https://github.com/CrocSwap/integer-mult-bounds/blob/358383e2f1b0f292d4d6eb897c06fd8558a4f5e6/research/hurwitz-asymmetric-copy-floor/NOTICE.md) +are retained byte-for-byte under [vendor/pr703](vendor/pr703), including +their attribution and license statements. Relative links within those +unchanged copies refer to the original package context. + +The source/reader pairing-rank model and associated accounting derive from +**DreamingOfClouds' [#446](https://github.com/CrocSwap/integer-mult-bounds/pull/446) +and [#595](https://github.com/CrocSwap/integer-mult-bounds/pull/595)** work as +used by #620. Their use here is explicit and conditional. Standard E8 root +coordinates, Gram-rank identities and clique rank subadditivity are not +claimed as new. + +The scoped contribution is the independent exact replays and the proof that +nonnegative weighting of inclusion-maximal-clique rank inequalities cannot +exceed 40 in this geometry. The lower bound and closure reduction overlap +with #738. We neither assert global novelty nor claim to settle the remaining +charge interval [40,60]. No predecessor implementation is imported by either +verifier. Pinned source files are read as data for provenance checks. + +The repository base is +`66849e1475c930fd7732b1a0067ffee7e1e95f60`. +[CLAIM.md](CLAIM.md) records the bounded overlap review; unreviewed PR claims +are source context, not adopted mathematical conclusions. The existing +selected construction and its predecessor lineage retain their credit and +assumptions. This package adds no supplier and changes no selected kappa. + +New files are provided under the repository's +[Apache License 2.0](../../LICENSE). The original authorship and license +notices of the retained #703 documents remain in their unchanged copies; +this notice supplements them. diff --git a/research/gaussian-all-clique-dual/vendor/pr770-PROOF.md b/research/gaussian-all-clique-dual/vendor/pr770-PROOF.md new file mode 100644 index 0000000000..ecd7b342e1 --- /dev/null +++ b/research/gaussian-all-clique-dual/vendor/pr770-PROOF.md @@ -0,0 +1,304 @@ +# A copy lower bound for Gaussian E8 scalar decoders + +**Result.** Every fitting binary scalar-total decoder on the +60 Gaussian E8 lines has copy charge at least **40 Gaussian rank units = 80 +rational rank units**, even with asymmetric reader/source sets and arbitrarily +many totals. Every fitting matrix has a row decomposition of charge 60, so the +result leaves the optimal charge in **[40, 60]**. It does not construct a new +supplier or improve the selected multiplication constant. + +**Concurrent overlap and the additional result.** The bound 40, the uniform +weight 1/192 on the 640 maximum cliques, closure to flats, the interval +[40,60], and the conditional three-stage consequence are already present in +Sagar Thakrar / thakrarsagar's concurrent +[PR #738](https://github.com/CrocSwap/integer-mult-bounds/pull/738), discovered +during the final overlap refresh. The inspected head is +`9671c5d72f3119ba26f3774f40aa7130c67bcf77` +([proof](https://github.com/CrocSwap/integer-mult-bounds/blob/9671c5d72f3119ba26f3774f40aa7130c67bcf77/research/gaussian-clique-copy-bound/PROOF.md)). +This package supplies an independent replay of that bound, not a priority +claim for it. Its additional theorem is Section 5: **40 is the optimal +certificate value even with arbitrary nonnegative weights on all +inclusion-maximal cliques**. The inspected #738 proof establishes 40 as the +uniform-weight optimum and gives the weaker ceiling 48 for arbitrary +nonnegative clique weights, including non-maximal cliques. Our ceiling 40 +does not cover that latter, larger class. + +The weighted-clique proof method is adapted from Douglas R. Colkitt / +Mister-Meeseeks' [PR #703](https://github.com/CrocSwap/integer-mult-bounds/pull/703) +on the ten Hurwitz E8 lines. The Gaussian geometry, scalar decoder question, +rank accounting and previously found cost-60 symmetric decoder come from +Joel Pulikkan / GamingPuzzled's +[PR #620](https://github.com/CrocSwap/integer-mult-bounds/pull/620), retained in +[the extension-ring report](../e8-decoder-floors-and-cold14-notes/s1-extension-rings/REPORT.md). +The finite calculations here concern the Gaussian configuration and its full +reader/source pairing ranks. Neither the predecessor's geometry nor the +cost-60 upper bound is claimed as new. + +The inspected #703 proof is pinned at commit +`358383e2f1b0f292d4d6eb897c06fd8558a4f5e6` +([source](https://github.com/CrocSwap/integer-mult-bounds/blob/358383e2f1b0f292d4d6eb897c06fd8558a4f5e6/research/hurwitz-asymmetric-copy-floor/PROOF.md)). +The pairing-rank accounting traces to DreamingOfClouds' #446/#595 work as +used by #620; the bound here is explicitly conditional on using that model. + +## 1. Geometry and decoder model + +Work with the 240 E8 roots in doubled standard coordinates in Q^8: + +- vectors with exactly two nonzero coordinates, both in {−2, 2}; +- vectors in {−1, 1}^8 with an even number of minus signs. + +Let J act on each consecutive coordinate pair by (x, y) -> (−y, x). +Then J^2 = −I, J preserves the roots, and J is orthogonal. It gives Q^8 the +structure of a four-dimensional vector space over K = Q(i). A root r spans +the Gaussian line L_r = span_Q{r, Jr}. The roots partition into 60 distinct +such lines, with four roots on each line. The exact replay checks line +distinctness and the root partition. + +Two different lines are called nonorthogonal when either r dot s or +r dot Js is nonzero. Write G for this nonorthogonality graph. Its complement +on distinct vertices is the orthogonality graph; every vertex of that graph +has degree 15. All ranks and orthogonality tests below use exact arithmetic. + +A fitting matrix B over F2 has + + B_tt = 1, + B_ts = 0 whenever t != s and L_t is nonorthogonal to L_s. + +Its entries on orthogonal pairs are free and need not be symmetric. An +arbitrary scalar-total decomposition is + + B = sum_j 1_{R_j} 1_{A_j}^T over F2, + +with reader sets R_j and source sets A_j. Any finite number of totals is +allowed; sets may be empty and terms may repeat. + +For a set S of lines, let V_S have the rows r and Jr for every representative +r in S. Define the charge of one total by + + q(R,A) = rank_Q(V_R V_A^T) / 2. + +Equivalently, this is the rank over K of the restricted Hermitian pairing +between the K-spans of R and A. In particular it is an integer in {0,1,2,3,4}. +The total charge is Q = sum_j q(R_j,A_j). This is the Gaussian form of the +source/reader pairing-rank charge used by the predecessor's Theorem-C +relaxation. It is not the binary rank of the decoder rectangle, and a total +need not have full Gaussian rank four. The factor two is restored whenever +the charge is expressed in rational rank units. + +## 2. Reducing all supports to finitely many flats + +For a support S, define its closure by + + cl(S) = {t : L_t is contained in span_K(S)}. + +A flat is such a closed set, including the empty set and all 60 lines. +Replacing R and A by their closures preserves q(R,A): every appended row of +V_cl(R) or V_cl(A) is a rational linear combination of existing rows. Thus +the Gram-block rank can neither increase nor decrease. + +For a clique C of G, put + + a_C(R,A) = 1 if C meets both R and A, and 0 otherwise. + +Closing supports can only increase this indicator. Consequently a local +inequality proved for every ordered pair of flats proves the same inequality +for every pair of arbitrary reader/source supports. This reduction concerns +the charge and the local indicator; it does not replace a decoder by a +different decoder or assume its fitting conditions survive closure. + +There are exactly 2,272 flats. Their census, together with the number of +maximum cliques meeting each flat, is: + +| Gaussian rank | Lines in flat | Number of flats | Maximum cliques meeting each flat | +| ---: | ---: | ---: | ---: | +| 0 | 0 | 1 | 0 | +| 1 | 1 | 60 | 128 | +| 2 | 2 | 360 | 256 | +| 2 | 3 | 320 | 308 | +| 2 | 6 | 30 | 320 | +| 3 | 4 | 960 | 436 | +| 3 | 6 | 480 | 492 | +| 3 | 15 | 60 | 512 | +| 4 | 60 | 1 | 640 | + +The closure enumeration is exhaustive: start with the empty flat and the +one-line flats, and extend every rank-r span by every line outside its +closure. Every rank-(r+1) root-spanned subspace has such a basis extension. +Exact row reduction and closure deduplication produce the next level. Rank +four has the unique full flat. This induction proves coverage, rather than +assuming that the displayed census is a complete search domain. + +## 3. The finite pairing-rank certificate + +Let C be the family of all maximum cliques of G. Exhaustive graph search +gives exactly 640 of them, each of size 12, and proves there is no larger +clique. The key finite certificate is + + sum_{C in C} a_C(F,H) <= 192 q(F,H) (1) + +for every pair of flats F,H. + +The primary replay checks (1) for all 2,582,128 unordered pairs with +repetition; both sides are symmetric in F,H, so this covers all ordered +pairs. It computes the exact pairing rank and the number of maximum cliques +meeting both flats. The result is: + +| Pairing rank q | Unordered flat pairs | Largest joint hit count | Allowed count 192q | +| ---: | ---: | ---: | ---: | +| 0 | 4,997 | 0 | 0 | +| 1 | 184,920 | 192 | 192 | +| 2 | 1,316,050 | 384 | 384 | +| 3 | 1,076,160 | 512 | 576 | +| 4 | 1 | 640 | 768 | + +Its exact rank calculation reduces to small cases. Empty or full spans and +a one-dimensional side have immediate ranks. Two rank-two sides use their +two-by-two Gaussian Gram determinant and, when that vanishes, their entries. +For ranks two and three, write the hyperplane as n-perp. The pairing rank is +one if n lies in the rank-two span and two otherwise. For two rank-three +hyperplanes, with normals n and m, the rank is two if n and m are orthogonal +and three otherwise. These formulas all follow from + + q(F,H) = dim_K(F) - dim_K(F intersect H-perp). + +The real-coordinate replay constructs each normal by exact rational nullspace +calculation. Because its spaces are J-invariant, one nonzero real normal +and its J-translate span the whole Gaussian normal line. + +A separate replay uses four Gaussian-integer coordinates, independent flat +generation and exact nonzero minors. For each pair it certifies that q is +at least the ceiling of the joint hit count divided by 192. It may also use +the rigorous bound q(F,H) >= dim_K(F) + dim_K(H) - 4, since the pairing kernel +F intersect H-perp has dimension at most 4 - dim_K(H). This certifies (1) +independently without claiming to recompute the primary rank histogram. +Both exhaustive pair checks pass. They concern the actual source/reader +Gram block, not just the rank of F intersect H, the cardinality of either +support, or an assumed full-rank total. + +When q=0 all lines across the two supports are orthogonal, so no clique can +meet both. Such totals are allowed and contribute zero to both sides. The +flat census and its individual hit counts help reproduce the check, but +they are not substitutes for the pairwise inequality (1). + +By Section 2, (1) holds for arbitrary supports R,A as well. + +## 4. The lower bound, including arbitrary asymmetric decompositions + +Every maximum clique C contains only pairwise nonorthogonal lines, so the +fitting conditions imply B[C,C] = I_12. Over F2, the restriction of a +rectangle 1_R 1_A^T to C by C has rank a_C(R,A). Rank subadditivity gives + + 12 <= sum_j a_C(R_j,A_j). + +Sum this inequality over the 640 maximum cliques and apply (1) to each +total: + + 640 * 12 + <= sum_j sum_{C in C} a_C(R_j,A_j) + <= 192 sum_j q(R_j,A_j). + +Therefore + + Q >= (640 * 12) / 192 = 40. + +This argument handles every finite number of scalar totals. It requires no +symmetry of B, no minimum-rank assumption on B, no limit on its number of +totals, and no uniform rank assumption on the totals. The extension from the +finite local certificate to all decompositions is the displayed rank +argument, rather than an enumeration of decoders. + +For the upper bound, decompose any fitting B into its 60 rows: for row t, +take R_t={t} and A_t equal to the nonzero positions in that row. The diagonal +condition puts t in A_t. Hence the Gram block has Gaussian rank exactly one, +and these 60 totals have total charge 60. In particular this upper bound +holds separately for every fitting matrix. It is an abstract charge bound, +not a claim of a physical supplier realizing it without additional costs. + +## 5. Forty is the limit of this maximal-clique method + +This section is a separate exact limitation of the proof method. It does not +prove that any actual decoder has charge 40. + +For a line t, let H_t be the set of the 15 configuration lines orthogonal to +t. The geometry check verifies that these lines span the whole Gaussian +hyperplane t-perp. If t and u are orthogonal distinct lines, then + + q(H_t,H_u) = 2. + +Indeed H_t and H_u both have dimension three, and the kernel of the pairing +on H_t against H_u is H_t intersect span_K(u) = span_K(u), of dimension one. + +An inclusion-maximal clique C of G meets H_t exactly when t is not in C. +If t is in C, orthogonality excludes every element of H_t. If t is not in C +and C missed H_t, then t would be nonorthogonal to every element of C and +could be added, contrary to maximality. + +Allow arbitrary nonnegative weights w_C on inclusion-maximal cliques. A +proof using only their principal-identity rank inequalities and a local +domination by q would require, for every pair of supports R,A, + + sum_C w_C a_C(R,A) <= q(R,A). (2) + +Its resulting copy lower bound is sum_C |C| w_C. Apply (2) to the 900 ordered +orthogonal pairs through the rectangles (H_t,H_u), and sum. A clique of size +k contains no orthogonal pair. Among the 900 ordered orthogonal pairs, +exactly 15k have their first endpoint in C and exactly 15k have their second +endpoint in C, with no overlap. It therefore contributes + + 900 - 30k + +to the sum of the indicators. Since k <= 12, + + 900 - 30k >= 45k. + +The summed right side of (2) is 900 * 2. Consequently + + 45 sum_C |C| w_C + <= sum_C (900 - 30|C|) w_C + <= 1800, + +and this proof method cannot yield a lower bound exceeding 40. In the +certified uniform construction, the 640 size-12 cliques each have weight +1/192, attaining exactly 40. + +This establishes optimality among such nonnegative weighted +**inclusion-maximal-clique** rank certificates. It does not address +certificates using non-maximal cliques, other submatrices or inequalities, +or additional algebraic information about the decoder. + +## 6. Consequences and limits + +The extension-ring report recorded a computational lower bound of 9 for its +bounded-total searches and a symmetric cost-60 solution. The result here +supplies a lower bound of 40 in the stated all-total asymmetric pairing-rank +model, with normalized charge + + x_K = Q/60 >= 2/3. + +The report's approximate charge threshold for beating its bit-E8 comparison +is about 0.71. Since 2/3 is below that value, this bound does **not** exclude +an improved Gaussian construction. The interval [40,60], including the +region near its reported threshold, remains unresolved. + +Conditionally applying exactly the report's Dfc accounting, Gaussian rank +scaling k=2 and port count v=60, the rational copy charge is at least 80: + + D/T = (s-1) * 120 - s * cst + <= (s-1) * 120 - s * 80 + = 40s - 120. + +Thus this optimistic accounting has no positive deficit for integer stage +counts s <= 3. It gives no exclusion for s >= 4. Helpers, source access, +restoration and recursive work are not supplied or certified here, and the +conditional accounting is not needed for the finite copy-floor theorem. + +The scope is the fixed 60-line Gaussian E8 geometry, binary scalar totals, +the stated fitting pattern, and the source/reader pairing-rank charge. +Other geometries, altered patterns, vector-valued totals, rational sub-line +supports and different supplier formats are outside scope. This is a +finite mathematical argument supported by exact computation, not a +proof-assistant formalization or a proof of the full multiplication theorem. + +Prepared for chinmayarvind23 with substantial OpenAI Codex assistance in +proof development, implementation and checking. No independent human review +is claimed. diff --git a/research/gaussian-all-clique-dual/vendor/selected-result.json b/research/gaussian-all-clique-dual/vendor/selected-result.json new file mode 100644 index 0000000000..1f107b55a2 --- /dev/null +++ b/research/gaussian-all-clique-dual/vendor/selected-result.json @@ -0,0 +1,153 @@ +{ + "status": "Maintainer-reviewed conditional finite construction; see the integration receipt for publication and PR resolution status", + "kappa": "1661634653669567/1000000000000000000", + "decimal": "0.001661634653669567", + "source_prs": [ + 799, + 741, + 699, + 685, + 676, + 664, + 660, + 659, + 656, + 655, + 653, + 658, + 649, + 645, + 635, + 589, + 555, + 545, + 626, + 623, + 622, + 620, + 617, + 615, + 604, + 601, + 596, + 592, + 591, + 593, + 599, + 588, + 543, + 584, + 586, + 583, + 582, + 579, + 576, + 575, + 574, + 571, + 569, + 568, + 567, + 564, + 562, + 561, + 559, + 558, + 552, + 550, + 548, + 541, + 535, + 510, + 503, + 531, + 523, + 493, + 514, + 507, + 484, + 496, + 505, + 522, + 520, + 472, + 458, + 445, + 442, + 425, + 433, + 370, + 361, + 315 + ], + "source_manifest": "research/community-frontier799-audit/SELECTED-SOURCE.json", + "certificate": "research/community-frontier799-audit/ASSEMBLY.json", + "certificate_sha256": "65c7648a8edaeaf4e0b8de3e21eeda94fba124d0935010d45ac9f76375b72cec", + "proof": "docs/research/community-frontier799-review.md", + "proof_supplements": { + "research/e8-bit-r420/README.md": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f", + "research/complex-571-free4fc8/NOTICE.md": "a4c084abdc1c7a9ac683eeb11124335d51cff8a6deba6ee92ba5a12bceaa2c97", + "research/complex-multicold/proof/CONSTRUCTION.md": "27ece5e1c11b90d97a808b56eff897b998c10e61016db95867f84e6e6aef132f", + "research/complex-multicold/vendor/pr559/PROOF.md": "d5d498edc56fdef8c5798af7f5ec66948bd2f66c553b9efe366cdaab01bd3453", + "research/structural-gain/frontier-composition/README.md": "70f0f791cbe3b2603f85d85bb9055aa0ee1df6dc06ba82fc1921356948312887", + "research/complex-joint-prefix/proof/CONSTRUCTION.md": "a92e610e7a598d99c612d1b63d1a03a49c0cd1e15ddd29fa55c465ddd8c18105", + "research/kernel-frame-coalescing/PROOF.md": "fa8b2f36b9590ee80ff45d3f7724f8c7de8ad29a29f366d5133010c77e41fe1b", + "research/complex-571-hpeq5/README.md": "4000b37f6c07c09d971dc4010ceb137c13340f3a8809d3272046ccaf746c3e2b", + "research/hyperplane-end-lean/PROOF.md": "1cbce5cf0ff0152f71e8ae7bef25841d1ce13010af248ff7209182d2328c21c9", + "docs/research/community-hyperplane599-review.md": "3298cd0d451541508af232cac72efbd7c10580e6c6ad493a855ab0faa01ade8c", + "research/complex-571-cold14-b3/README.md": "1945785785c153c7d0e8d4c071adabe626c1091b71721ff85d2d67191b376b96", + "research/complex-571-cold14-b3/PROOF-NOTE.md": "1cf592cbc8ab8e21d2dd8c1e945a5c64c6d5cde1216fb06e05a36c1c6ec6613d", + "scripts/verify_cold617_interface.py": "95d7a9094c05ad975fb72f5ab7605593003245a503c8456764987e512028fa6a", + "docs/research/community-cold617-review.md": "b3f2bcbae1249f1f651032022ce1e6e2bfb3f563ce580bf53671f50a074d7046", + "research/complex-k492-owner-repair/README.md": "ee5a1ace4828f7a073be97e95c2d931988774dd3a29a877e65abdf429aeec902", + "research/complex-k492-owner-repair/PROOF-NOTE.md": "337d70fe7abd9afca1d90954c23bde87f4dc27888cc1a6b4bb80506fd6fbf8c5", + "research/complex-k492-owner-repair/PROOF-NOTE-R.md": "22312bb347bdf159e6a01a45c47675e6170d33b258e2fd9ed52aee88fb92c0ed", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", + "scripts/verify_frontier626.py": "2207bd0ef04a19ef276869085afdedad80a0938fa75db5e1aa7ab73fd3429444", + "scripts/verify_frontier626_bindings.py": "cda63ff41c6d6e2e352c7bf75b84e690c0ce57e4ec6c0355573bb5d9b1f98280", + "scripts/verify_frontier588_bindings.py": "6d1932eea7b1936598118ea8e607b09c29b6e31b749ec41bbe0744ea4f0b606d", + "scripts/verify_hpe_lean_binding.py": "52aa1d23641e4c716b43c98f6b883ad042087dd03a9d01369e8e6a735b07aa03", + "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183", + "docs/research/community-frontier741-review.md": "4634694fa75ea9e749ecf19d3db3e4d82effe3b61a2efdf08ac5a97275fb676a", + "research/complex-sw4-frame8/PROVENANCE.md": "c7648719b01dd93af2c3a2c6e951a54711d13892dc4bd4339d16edb4c37c9bf0", + "research/e8-bit-p111-tuned/tune/README.md": "46c7917fb252949f38b7bcd88cf568efc282e3ea065b61d11e457e41673d0b2d", + "scripts/verify_frontier741.py": "215ee6a12de8dc2392e6811a1b8f2140035f6b2d2a0d2100ff4bd2fdcb8bb39b", + "scripts/verify_frontier741_bindings.py": "eff455167e2fd0bc9a67d35241d0e69d8edc58f3a23e776dcfe8f500ca8e8d67", + "docs/research/community-frontier799-review.md": "bd91c10c67f2a873fd456b95cbb43f715a43dac0e0a66938737d591c6b754052", + "scripts/verify_frontier799.py": "19fe1b32079095160dc00fe2f7df75e0fcbc82cff37f7159b755c8a63bd5ce99", + "scripts/verify_frontier799_bindings.py": "43897b3c99212d6134870898a1840f32898aa1b3679b299e654901568ad7e19b", + "research/gauge44-frames-x/PROOF-NOTE-FRAMES-X4.md": "39c50420ebb6e8813706a49b2cf759f277c4afac9f6780fc0a7ac6a5fb86e036" + }, + "review": "docs/research/community-frontier799-review.md", + "validation": "docs/research/community-frontier799-integration.json", + "reproduce": "make frontier799-verify", + "scope": "Source-bound finite X4 construction and freshly rebuilt bit589/ancestral SW4 supplier checks; optional verified ancestry reuse recorded explicitly. Inherited all-size/compiler, common-label/mutable-source, whole-call hosting, precision/tape and analytic hypotheses remain. Not a full Lean multiplication theorem. Integration Linux CI status is separate.", + "previous_kappa": "1661202643272239/1000000000000000000", + "previous_record": "certificates/checkpoints/frontier741.json", + "audited_source_head": "80e6463157cfc80b85af09e7e2f14748fe2dac60", + "reviewed_dependency_heads": { + "588": "6d0e53b66c29abd17981881a09eaff41ac862d85", + "543": "2065fe4f72a914d907f1046603f5a36f17018535", + "568": "71c99ac935a33bb7b59a1b4a7af8725a939b0b90", + "569": "1424da81263a5305b35e4cf74ef686c275f03f3f", + "571": "b7bdc5a8de18fcf418cfb9c7d83a2b1097a5e4a3", + "575": "eac6f7e378ab622dac50a2fd4b7ef6eab014de44", + "583": "89be768f0157f5a3d8e4db69cf1748768605eac9", + "586": "4846fee5b06af770e9b3a10c36200f673d656725", + "591": "f622547244bf6d895a571a7b035142ba66279806", + "592": "1f471c445c06a45a32e2c47e8d74c8264b68356b", + "593": "fdb6dcc6d7bc29764c5b6b4d32b7fa050acf74a4", + "596": "7732dd5e46863ff294b5e443661cb9d99abf4e01", + "599": "bc13c8a3e000442606bd2dbe8583a17649ba6c32", + "601": "529ab7dcb59d5ea7a5798e9e06cf5b3aee8a1550", + "604": "1b795c5d7dea746ba310572585c0ef067574b4a6", + "615": "bf8a49a34350599763cced8592db81dc62c2c1c0", + "617": "904d62855723c00f8acef9a287a10768598fdeb2", + "622": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "623": "e39a615ca601ce5d62abeb24f3fcdb8644ca1005", + "626": "660de893d27bb7abd1d5b01b1640207528a5c851", + "589": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "741": "e516b1463606840a15f80aac1995d64ce0092e89", + "799": "80e6463157cfc80b85af09e7e2f14748fe2dac60" + } +} diff --git a/research/gaussian-all-clique-dual/verify.py b/research/gaussian-all-clique-dual/verify.py new file mode 100644 index 0000000000..00d4308c35 --- /dev/null +++ b/research/gaussian-all-clique-dual/verify.py @@ -0,0 +1,271 @@ +#!/usr/bin/env python3 +"""Exact all-clique Gaussian E8 dual. William Lawyer / Codex, Apache-2.0.""" + +import argparse +from array import array +from collections import Counter +from fractions import Fraction +import hashlib +from itertools import combinations, product +import json +from pathlib import Path +import struct + +HERE = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def bits(mask): + while mask: + bit = mask & -mask + yield bit.bit_length() - 1 + mask ^= bit + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def rotate(row): + return tuple(x for i in range(0, len(row), 2) + for x in (-row[i + 1], row[i])) + + +def reduced_basis(rows): + """Rational RREF, including all columns and zero-pivot fallback.""" + matrix = [list(map(Fraction, row)) for row in rows] + width = len(matrix[0]) if matrix else 0 + require(all(len(row) == width for row in matrix), 'ragged rank input') + rank = 0 + for column in range(width): + pivot = next((i for i in range(rank, len(matrix)) + if matrix[i][column]), None) + if pivot is None: + continue + matrix[rank], matrix[pivot] = matrix[pivot], matrix[rank] + value = matrix[rank][column] + matrix[rank] = [x / value for x in matrix[rank]] + for i in range(len(matrix)): + if i != rank and matrix[i][column]: + scale = matrix[i][column] + matrix[i] = [x - scale * y for x, y in zip(matrix[i], matrix[rank])] + rank += 1 + return tuple(tuple(row) for row in matrix[:rank]) + + +def roots_and_lines(): + sparse = [] + for first, second in combinations(range(8), 2): + for a, b in product((-2, 2), repeat=2): + row = [0] * 8 + row[first], row[second] = a, b + sparse.append(tuple(row)) + dense = [row for row in product((-1, 1), repeat=8) + if sum(x == -1 for x in row) % 2 == 0] + roots = tuple(sorted((*sparse, *dense))) + require(len(sparse) == 112 and len(dense) == 128, 'root-family census') + require(len(roots) == len(set(roots)) == 240, 'root census or duplication') + require(all(dot(row, row) == 8 for row in roots), 'root norm') + require(set(map(rotate, roots)) == set(roots), 'complex structure does not preserve roots') + orbits = {min(row, rotate(row), tuple(-x for x in row), + tuple(-x for x in rotate(row))) for row in roots} + lines = tuple(sorted(orbits)) + require(len(lines) == 60, 'Gaussian line census') + require(len(reduced_basis(lines)) == 8, 'ambient rank') + require(all(dot(a, b)**2 + dot(a, rotate(b))**2 < 64 + for a, b in combinations(lines, 2)), 'duplicate Gaussian projective line') + return roots, lines + + +def check_orthogonal_graph(orthogonal): + require(len(orthogonal) == 60, 'orthogonal graph order') + require(all(mask.bit_count() == 15 for mask in orthogonal), 'orthogonal degree') + require(all(0 <= mask < (1 << 60) and not mask >> i & 1 + for i, mask in enumerate(orthogonal)), 'orthogonal graph mask or diagonal') + require(all((orthogonal[i] >> j & 1) == (orthogonal[j] >> i & 1) + for i in range(60) for j in range(60)), 'graph symmetry') + + +def graph_data(lines): + orthogonal = tuple(sum(1 << j for j, b in enumerate(lines) + if i != j and dot(a, b) == dot(a, rotate(b)) == 0) + for i, a in enumerate(lines)) + full = (1 << len(lines)) - 1 + adjacency = tuple(full ^ mask ^ (1 << i) + for i, mask in enumerate(orthogonal)) + check_orthogonal_graph(orthogonal) + dual_rows = tuple(sum(1 << j for j in bits(orthogonal[i]) + if (orthogonal[i] & orthogonal[j]).bit_count() == 6) + for i in range(len(lines))) + pairs = tuple((i, j) for i, row in enumerate(dual_rows) for j in bits(row)) + require(len(pairs) == 180 and len(set(pairs)) == 180, 'dual pair census') + require(all(row.bit_count() == 3 for row in dual_rows), 'dual graph degree') + return adjacency, orthogonal, dual_rows, pairs + + +def check_geometry(lines, orthogonal, pairs): + bases = [reduced_basis(row for i in bits(mask) + for row in (lines[i], rotate(lines[i]))) + for mask in orthogonal] + require(all(len(basis) == 6 for basis in bases), 'root hyperplane does not span rank three') + require(all(all(dot(row, lines[i]) == dot(row, rotate(lines[i])) == 0 + for row in bases[i]) for i in range(60)), 'wrong root hyperplane') + ranks = Counter() + for i, j in pairs: + block = tuple(tuple(dot(a, b) for b in bases[j]) for a in bases[i]) + rank = len(reduced_basis(block)) + require(rank == 4, 'dual pair has wrong rational pairing rank') + ranks[rank // 2] += 1 + return dict(sorted(ranks.items())) + + +def frames_from_dual(dual_rows): + left = (1 << len(dual_rows)) - 1 + frames = [] + while left: + i = next(bits(left)) + mask = (1 << i) | dual_rows[i] + require(mask.bit_count() == 4, 'dual component is not a four-frame') + require(all(dual_rows[j] == mask ^ (1 << j) for j in bits(mask)), 'dual component is not K4') + require(mask & left == mask, 'dual components overlap') + left ^= mask + frames.append(mask) + require(len(frames) == 15, 'four-frame partition') + return tuple(frames) + + +def all_cliques(adjacency): + """Ordered extensions: each nonempty clique has a unique increasing path.""" + def visit(chosen, available): + while available: + bit = available & -available + available ^= bit + i = bit.bit_length() - 1 + extended = chosen | bit + yield extended + yield from visit(extended, available & adjacency[i]) + yield from visit(0, (1 << len(adjacency)) - 1) + + +def joint_hit_count(clique, orthogonal, dual_rows): + hit = 0 + for i in bits(clique): + hit |= orthogonal[i] + return sum((row & hit).bit_count() for i, row in enumerate(dual_rows) + if hit >> i & 1) + + +def check_clique(mask, adjacency): + require(0 < mask < (1 << len(adjacency)), 'invalid clique mask') + require(all((mask ^ (1 << i)) & ~adjacency[i] == 0 for i in bits(mask)), + 'orthogonal pair admitted as clique') + + +def check_dual_hit(size, count, multiplier=9): + require(count >= multiplier * size, 'dual incidence does not dominate clique size') + + +def rejected(function, *args): + try: + function(*args) + except ValueError: + return + raise ValueError('negative control unexpectedly accepted: ' + function.__name__) + + +def calculate(): + roots, lines = roots_and_lines() + adjacency, orthogonal, dual_rows, pairs = graph_data(lines) + rank_census = check_geometry(lines, orthogonal, pairs) + frames = frames_from_dual(dual_rows) + census, minima, witnesses = Counter(), {}, {} + packed = array('Q') + for clique in all_cliques(adjacency): + size = clique.bit_count() + count = joint_hit_count(clique, orthogonal, dual_rows) + check_dual_hit(size, count) + census[size] += 1 + packed.append(clique) + if count < minima.get(size, 10**9) or (count == minima.get(size) and clique < witnesses[size]): + minima[size], witnesses[size] = count, clique + # Explicit little-endian encoding is independent of host array byte order. + digest = hashlib.sha256() + ordered = sorted(packed) + require(all(a < b for a, b in zip(ordered, ordered[1:])), 'duplicate clique enumeration') + for mask in ordered: + digest.update(struct.pack('