From 28d68c88f0184835d8c8a7266ab8d0dad3f18a8a Mon Sep 17 00:00:00 2001 From: ross Date: Wed, 14 Oct 2026 01:37:31 +1100 Subject: [PATCH] Prove a scoped cost ceiling for the five-port quadratic star decoder --- .../CERTIFICATE.json | 211 + .../five-port-quadratic-decoder/CLAIM.json | 47 + .../INDEPENDENT.json | 145 + research/five-port-quadratic-decoder/LICENSE | 201 + .../five-port-quadratic-decoder/NOTICE.md | 53 + .../five-port-quadratic-decoder/OVERLAP.json | 246 + research/five-port-quadratic-decoder/PROOF.md | 240 + .../five-port-quadratic-decoder/README.md | 93 + .../five-port-quadratic-decoder/SOURCES.json | 35 + .../five-port-quadratic-decoder/VALIDATION.md | 64 + .../WITNESSES.json | 4650 +++++++++++++++++ .../five-port-quadratic-decoder/discover.py | 138 + .../evidence/checks.json | 50 + .../evidence/clean-export.json | 27 + .../evidence/export-independent.py.txt | 1 + .../evidence/export-verify.py.txt | 1 + .../evidence/package-tests.txt | 11 + .../evidence/primary-python312.txt | 1 + .../evidence/second-python314.txt | 1 + .../evidence/selected-record.txt | 2 + .../independent.py | 146 + .../sources/format-axioms-README.md | 805 +++ .../sources/pr231-README.md | 56 + .../sources/pr446-PROOF.md | 404 ++ .../sources/selected-result-base.json | 170 + .../test_package.py | 106 + .../five-port-quadratic-decoder/verify.py | 250 + 27 files changed, 8154 insertions(+) create mode 100644 research/five-port-quadratic-decoder/CERTIFICATE.json create mode 100644 research/five-port-quadratic-decoder/CLAIM.json create mode 100644 research/five-port-quadratic-decoder/INDEPENDENT.json create mode 100644 research/five-port-quadratic-decoder/LICENSE create mode 100644 research/five-port-quadratic-decoder/NOTICE.md create mode 100644 research/five-port-quadratic-decoder/OVERLAP.json create mode 100644 research/five-port-quadratic-decoder/PROOF.md create mode 100644 research/five-port-quadratic-decoder/README.md create mode 100644 research/five-port-quadratic-decoder/SOURCES.json create mode 100644 research/five-port-quadratic-decoder/VALIDATION.md create mode 100644 research/five-port-quadratic-decoder/WITNESSES.json create mode 100644 research/five-port-quadratic-decoder/discover.py create mode 100644 research/five-port-quadratic-decoder/evidence/checks.json create mode 100644 research/five-port-quadratic-decoder/evidence/clean-export.json create mode 100644 research/five-port-quadratic-decoder/evidence/export-independent.py.txt create mode 100644 research/five-port-quadratic-decoder/evidence/export-verify.py.txt create mode 100644 research/five-port-quadratic-decoder/evidence/package-tests.txt create mode 100644 research/five-port-quadratic-decoder/evidence/primary-python312.txt create mode 100644 research/five-port-quadratic-decoder/evidence/second-python314.txt create mode 100644 research/five-port-quadratic-decoder/evidence/selected-record.txt create mode 100644 research/five-port-quadratic-decoder/independent.py create mode 100644 research/five-port-quadratic-decoder/sources/format-axioms-README.md create mode 100644 research/five-port-quadratic-decoder/sources/pr231-README.md create mode 100644 research/five-port-quadratic-decoder/sources/pr446-PROOF.md create mode 100644 research/five-port-quadratic-decoder/sources/selected-result-base.json create mode 100644 research/five-port-quadratic-decoder/test_package.py create mode 100644 research/five-port-quadratic-decoder/verify.py diff --git a/research/five-port-quadratic-decoder/CERTIFICATE.json b/research/five-port-quadratic-decoder/CERTIFICATE.json new file mode 100644 index 0000000000..ea1e56d164 --- /dev/null +++ b/research/five-port-quadratic-decoder/CERTIFICATE.json @@ -0,0 +1,211 @@ +{ + "schema": "five-port-quadratic-certificate-v1", + "base_commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "witness_sha256": "d646efe099b20098fe02f9249cb8318ba2cdf4f50ef26dc54a8b2577567d2f28", + "source_sha256": { + "sources/pr231-README.md": "2dc89289d1d979aec6709b8c55a2af7cd39d97297bc20fb94adc7d4cdf867cd1", + "sources/format-axioms-README.md": "0fa0d6b2df96ddc06b876c41c5fa8d2335b97f36bc8f17d1371296d23199c263", + "sources/selected-result-base.json": "41fb066ff0f43ce472323195e9088d6d888715c13c54eae7b42e357ed5bfc726", + "sources/pr446-PROOF.md": "7a8c3bab633c08e7d96297dec9f9e7ed68d6bd0e076b73310c7d6b08a16df017" + }, + "prime": 65521, + "ranks": [ + { + "p": 5, + "kind": "corrector", + "rank_lower": 15, + "determinant_mod_prime": 64590 + }, + { + "p": 5, + "kind": "star", + "rank_lower": 11, + "determinant_mod_prime": 7200 + }, + { + "p": 6, + "kind": "corrector", + "rank_lower": 50, + "determinant_mod_prime": 39381 + }, + { + "p": 6, + "kind": "star", + "rank_lower": 35, + "determinant_mod_prime": 16722 + }, + { + "p": 7, + "kind": "corrector", + "rank_lower": 83, + "determinant_mod_prime": 45089 + }, + { + "p": 7, + "kind": "star", + "rank_lower": 60, + "determinant_mod_prime": 48334 + }, + { + "p": 8, + "kind": "corrector", + "rank_lower": 111, + "determinant_mod_prime": 47175 + }, + { + "p": 8, + "kind": "star", + "rank_lower": 84, + "determinant_mod_prime": 40322 + }, + { + "p": 9, + "kind": "corrector", + "rank_lower": 143, + "determinant_mod_prime": 15656 + }, + { + "p": 9, + "kind": "star", + "rank_lower": 112, + "determinant_mod_prime": 42257 + }, + { + "p": 10, + "kind": "corrector", + "rank_lower": 179, + "determinant_mod_prime": 14223 + }, + { + "p": 10, + "kind": "star", + "rank_lower": 144, + "determinant_mod_prime": 38013 + }, + { + "p": 11, + "kind": "corrector", + "rank_lower": 219, + "determinant_mod_prime": 57920 + }, + { + "p": 11, + "kind": "star", + "rank_lower": 170, + "determinant_mod_prime": 40517 + }, + { + "p": 12, + "kind": "corrector", + "rank_lower": 263, + "determinant_mod_prime": 31288 + }, + { + "p": 12, + "kind": "star", + "rank_lower": 210, + "determinant_mod_prime": 37917 + }, + { + "p": 13, + "kind": "corrector", + "rank_lower": 311, + "determinant_mod_prime": 2988 + } + ], + "algebra": { + "literal_decoder_pairs": 37888, + "parity_clique_size": 16, + "affine_label_span_upper": 6, + "logarithm_partial_sum": "3897967/3548160", + "logarithm_lower": "549/500" + }, + "finite_bounds": [ + { + "p": 5, + "ports": 32, + "active_rank_lower": 15, + "star_rank_lower": 11, + "copy_charge_lower": 110, + "positive_deficit_possible": false + }, + { + "p": 6, + "ports": 192, + "active_rank_lower": 50, + "star_rank_lower": 35, + "copy_charge_lower": 420, + "positive_deficit_possible": false + }, + { + "p": 7, + "ports": 672, + "active_rank_lower": 83, + "star_rank_lower": 60, + "copy_charge_lower": 840, + "positive_deficit_possible": false + }, + { + "p": 8, + "ports": 1792, + "active_rank_lower": 111, + "star_rank_lower": 84, + "copy_charge_lower": 1344, + "positive_deficit_possible": true, + "saving_upper": "125/121878" + }, + { + "p": 9, + "ports": 4032, + "active_rank_lower": 143, + "star_rank_lower": 112, + "copy_charge_lower": 2016, + "positive_deficit_possible": true, + "saving_upper": "125/78507" + }, + { + "p": 10, + "ports": 8064, + "active_rank_lower": 179, + "star_rank_lower": 144, + "copy_charge_lower": 2880, + "positive_deficit_possible": true, + "saving_upper": "125/76433" + }, + { + "p": 11, + "ports": 14784, + "active_rank_lower": 219, + "star_rank_lower": 170, + "copy_charge_lower": 3740, + "positive_deficit_possible": true, + "saving_upper": "31375/20198808" + }, + { + "p": 12, + "ports": 25344, + "active_rank_lower": 263, + "star_rank_lower": 210, + "copy_charge_lower": 5040, + "positive_deficit_possible": true, + "saving_upper": "5875/4235352" + } + ], + "all_p_ge_13_tail_upper": "250/170739", + "supplier_saving_strict_upper": "125/76433", + "selected_kappa_at_base": "1661957774647029/1000000000000000000", + "strict_gap": "2028418589596367557/76433000000000000000000", + "stage_scope": "every integer s >= 3 under PROOF.md accounting premises", + "negative_controls": [ + "duplicate minor row", + "self substituted for corrector", + "false determinant residue", + "invalid paired-port label", + "reader outside copied star", + "invoice rank differs from witness", + "unproved logarithm bound", + "linear kernel rejected at overlap three", + "singular matrix detected by elimination" + ], + "new_kappa_claim": false +} diff --git a/research/five-port-quadratic-decoder/CLAIM.json b/research/five-port-quadratic-decoder/CLAIM.json new file mode 100644 index 0000000000..cff11fd7e0 --- /dev/null +++ b/research/five-port-quadratic-decoder/CLAIM.json @@ -0,0 +1,47 @@ +{ + "track": "structural decoder research", + "assignment_seed": 40, + "randomness": "secrets.randbelow(100), operating-system CSPRNG; drawn once at 2026-10-13T14:01:22Z", + "base_commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "started_utc": "2026-10-13T14:01:22Z", + "claim_utc": "2026-10-13T14:10:44.190873+00:00", + "expected_finish_utc": "2026-10-13T14:51:22Z", + "time_budget_minutes": 50, + "verification_reserve_minutes": 12.5, + "coordination": "No pinned issue exists; local claim per sprint instructions. No reservation issue opened.", + "candidates": [ + { + "task": "Five-port level-one star decoder: minimum polynomial degree, natural quadratic pairing and complete optimistic copy/frame budget", + "chosen": true, + "reason": "PR231 explicitly leaves k=5 geometry and complete pricing open; distinct from higher proper-star information thresholds." + }, + { + "task": "Power-of-two proper-star decoder through asymmetric punctures", + "chosen": false, + "reason": "PR669 already gives uniform higher-target results; PR725/732/747/772 overlap." + }, + { + "task": "Stronger Gaussian decoder floor using weighted clique certificates", + "chosen": false, + "reason": "PR868 closes all nonempty cliques at 40; extending this finite search would duplicate a closed class." + } + ], + "object": "Unpunctured signed five-ports on p coordinate pairs, scalar level-one stars and odd-overlap correction; natural symmetric quadratic kernel G(S,T)=2(|S intersect T|-1)(|S intersect T|-3).", + "hypothesis": "The degree-two lift repairs the linear-label obstruction, but its exact star-copy ranks and mandatory active climbs alone cannot beat the selected saving, even if every other expense is zero.", + "method": "Character decomposition over sign flips and exact rational subset-incidence eigenspaces; literal Gram/rank controls at small p; rational optimistic budget with all-p tail.", + "seed_diversification": "The two next odd-port candidates are k=5 and k=7; 40 mod 2 chooses k=5. The seed also fixes finite witness order. This is a new quadratic geometry class, not a re-run of E8 puncture search.", + "expected_deliverable": "Scoped negative-result research note, written rank proof, exact certificate and standalone verifier with adverse controls; no new kappa, supplier or selected-frontier edit.", + "scope_exclusions": [ + "Other asymmetric/non-polynomial decoder geometries", + "Different copy supports or readers", + "Physical all-size implementation", + "Formal proof of multiplication" + ], + "result": { + "status": "completed research note / scoped negative result; ready for external review", + "statement": "Natural five-port quadratic Gram with separate stars and fixed-window accounting has supplier saving < 125/76433 for all p>=5 and s>=3; no new kappa.", + "link": "https://github.com/RossRichardson/integer-mult-bounds/blob/research/structural-decoder-seed40/research/five-port-quadratic-decoder/README.md", + "verification": "17 minors in two implementations, nine primary controls, six package tests, canonical Git-blob export with identical receipts, selected-record integrity", + "completed_utc": "2026-10-13T14:36:20.963267+00:00" + } +} diff --git a/research/five-port-quadratic-decoder/INDEPENDENT.json b/research/five-port-quadratic-decoder/INDEPENDENT.json new file mode 100644 index 0000000000..b1785cb911 --- /dev/null +++ b/research/five-port-quadratic-decoder/INDEPENDENT.json @@ -0,0 +1,145 @@ +{ + "schema": "five-port-second-implementation-v1", + "witness_sha256": "d646efe099b20098fe02f9249cb8318ba2cdf4f50ef26dc54a8b2577567d2f28", + "second_prime": 65519, + "minors": [ + { + "p": 5, + "kind": "corrector", + "dimension": 15, + "determinant_mod_second_prime": 9315 + }, + { + "p": 5, + "kind": "star", + "dimension": 11, + "determinant_mod_second_prime": 9248 + }, + { + "p": 6, + "kind": "corrector", + "dimension": 50, + "determinant_mod_second_prime": 31118 + }, + { + "p": 6, + "kind": "star", + "dimension": 35, + "determinant_mod_second_prime": 62527 + }, + { + "p": 7, + "kind": "corrector", + "dimension": 83, + "determinant_mod_second_prime": 6276 + }, + { + "p": 7, + "kind": "star", + "dimension": 60, + "determinant_mod_second_prime": 51965 + }, + { + "p": 8, + "kind": "corrector", + "dimension": 111, + "determinant_mod_second_prime": 20050 + }, + { + "p": 8, + "kind": "star", + "dimension": 84, + "determinant_mod_second_prime": 34204 + }, + { + "p": 9, + "kind": "corrector", + "dimension": 143, + "determinant_mod_second_prime": 48038 + }, + { + "p": 9, + "kind": "star", + "dimension": 112, + "determinant_mod_second_prime": 21862 + }, + { + "p": 10, + "kind": "corrector", + "dimension": 179, + "determinant_mod_second_prime": 49894 + }, + { + "p": 10, + "kind": "star", + "dimension": 144, + "determinant_mod_second_prime": 16596 + }, + { + "p": 11, + "kind": "corrector", + "dimension": 219, + "determinant_mod_second_prime": 19618 + }, + { + "p": 11, + "kind": "star", + "dimension": 170, + "determinant_mod_second_prime": 65398 + }, + { + "p": 12, + "kind": "corrector", + "dimension": 263, + "determinant_mod_second_prime": 12776 + }, + { + "p": 12, + "kind": "star", + "dimension": 210, + "determinant_mod_second_prime": 41602 + }, + { + "p": 13, + "kind": "corrector", + "dimension": 311, + "determinant_mod_second_prime": 55503 + } + ], + "integer_determinants_p5": [ + { + "kind": "corrector", + "determinant": "1152921504606846976" + }, + { + "kind": "star", + "determinant": "137438953472" + } + ], + "finite_bounds": [ + { + "p": 8, + "upper": "125/121878" + }, + { + "p": 9, + "upper": "125/78507" + }, + { + "p": 10, + "upper": "125/76433" + }, + { + "p": 11, + "upper": "31375/20198808" + }, + { + "p": 12, + "upper": "5875/4235352" + } + ], + "ceiling": "125/76433", + "tail": "250/170739", + "selected_kappa": "1661957774647029/1000000000000000000", + "human_independent_review": false +} diff --git a/research/five-port-quadratic-decoder/LICENSE b/research/five-port-quadratic-decoder/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/five-port-quadratic-decoder/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/five-port-quadratic-decoder/NOTICE.md b/research/five-port-quadratic-decoder/NOTICE.md new file mode 100644 index 0000000000..7895480850 --- /dev/null +++ b/research/five-port-quadratic-decoder/NOTICE.md @@ -0,0 +1,53 @@ +# Attribution, license and assistance + +New proof, witness construction, checkers and packaging: Ross Richardson +(@RossRichardson), 2026. Licensed under the repository's Apache-2.0 license. +Substantial OpenAI Codex assistance was used for task selection, mathematics, +implementation, verification and writing. No independent human peer review +or proof-assistant verification is claimed. + +Predecessors and retained sources: + +- **Joel Pulikkan (@GamingPuzzled), PR231**, head + `3c11e696a2fb2c454585d72710de27cd6bd3be68`: the general k-port parity + identity and the explicit open geometry/pricing question for k=5. Its + incorporated README is retained unchanged from the exact base, including + the original Anthropic Claude assistance disclosure. +- **icekylinx and eumemic**: the paired-cube design, bit decoder and local + construction lineage credited by PR231. We introduce no claim of priority + for the XOR star identity. +- **DreamingOfClouds, PR446**, head + `309482849b6ddf34db998f53612d34c19f6e3233`: the content-frame, stage-rank, + pairing-rank copy and clique arguments. `sources/pr446-PROOF.md` is + retained verbatim from that commit. It was prepared with Anthropic + Claude assistance, as disclosed by the predecessor. Its frame lemma + credit belongs to **Jacob Sussman**; the preceding common-label and + compressed-window lineage includes **Zhihao Chen (@jacklightChen)**. +- **DreamingOfClouds' format-limits package**, incorporated at the base: + the explicit pressure, deficit, window, active-bank and batching axioms. + Its README is retained verbatim, with its original credits and AI notice. + We use the named accounting as explicit premises and do not claim a new + audit of all its other results. +- **Chafik Boukhalfa, Jeremy Kothe, Hao Yan, DreamingOfClouds and eumemic**, + and the earlier contributors in the selected review: the frozen PR890 + conditional benchmark. The selected certificate is copied only as + context, not modified or re-certified by this contribution. + +Related work inspected for overlap: + +- **Sam Sung (@the-missionary-company), PR669** and its credited predecessors + study information obtainable from proper stars after puncturing. Our + unpunctured quadratic geometry and conditional cost obstruction are + distinct; no code or certificates from that PR are used. +- **William Lawyer, PR868**, with the PR738/770 predecessors, closes the + weighted-clique Gaussian certificate class. It motivated rejecting that + candidate task; it is not a dependency of this proof. +- PR201 is a complex three-stage paired-cube ceiling; PR620 concerns E8 + decoder floors; PR912 concerns nonlinear adaptive Hurwitz routing; PR920 + concerns complex parity frames. None supplies the five-port witnesses. + +Only the four text/JSON sources named in `SOURCES.json` are retained. +Their SHA256 and Git blob identities, original paths and exact commit pins +are checked. No predecessor implementation code is imported. Original +sources retain their attribution and license; no literature-wide priority +claim is made for the parity-clique or polynomial-feature techniques. diff --git a/research/five-port-quadratic-decoder/OVERLAP.json b/research/five-port-quadratic-decoder/OVERLAP.json new file mode 100644 index 0000000000..1f9e541f2e --- /dev/null +++ b/research/five-port-quadratic-decoder/OVERLAP.json @@ -0,0 +1,246 @@ +{ + "initial_open_pr_count": 717, + "initial_snapshot_utc": "2026-10-13T14:02:13.107238+00:00", + "pinned_coordination_issues": [], + "inspected_candidates_and_adjacent_work": [ + { + "author": { + "id": "MDQ6VXNlcjEyMTkwNTAw", + "is_bot": false, + "login": "jon314159", + "name": "Jonathan Capalbo" + }, + "headRefName": "codex/t37-whole-owner-bound", + "headRefOid": "1960cfa919a0945d0ca4cb14ea96237000037903", + "number": 942, + "title": "Conditional \u03ba = 0.001661960547713947: T37 whole-owner packing and all-T bound", + "updatedAt": "2026-10-13T13:52:33Z" + }, + { + "author": { + "id": "MDQ6VXNlcjU2NTI3MTY=", + "is_bot": false, + "login": "RossRichardson", + "name": "Ross Richardson" + }, + "headRefName": "research/e8-joint-reader-seed46", + "headRefOid": "3a8ec54d62fb8824c658dc7ed356f99423cac8cf", + "number": 939, + "title": "Scoped negative result: E8 star-copy ratio cannot improve through 55 punctures (no new kappa)", + "updatedAt": "2026-10-13T13:43:55Z" + }, + { + "author": { + "id": "U_kgDODHHRtQ", + "is_bot": false, + "login": "ArnavSwiggy", + "name": "" + }, + "headRefName": "research/complex-parity-frames-seed35", + "headRefOid": "913817423bbfaf241dec1d6b9edb1c7ded349508", + "number": 920, + "title": "Research note: certify shared parity decoder frame dimensions", + "updatedAt": "2026-10-13T12:36:21Z" + }, + { + "author": { + "id": "MDQ6VXNlcjgwMjk5Njgz", + "is_bot": false, + "login": "CubeJerry", + "name": "" + }, + "headRefName": "research/seed42-decoder", + "headRefOid": "945b3da1f1dd87cebd456b3a0459601b15f7ea8b", + "number": 912, + "title": "Research/seed42 decoder", + "updatedAt": "2026-10-13T12:00:26Z" + }, + { + "author": { + "id": "MDQ6VXNlcjg4MjYxNTE2", + "is_bot": false, + "login": "DaysSky", + "name": "" + }, + "headRefName": "research/e7-flat-cover-classification", + "headRefOid": "12c4789c61ac843dcd00e2c71e5388d362298b1a", + "number": 897, + "title": "No new \u03ba: covers of E7 by hyperplane flats are exactly the D4-frame triples; near-covers are the A3s (checked)", + "updatedAt": "2026-10-13T10:57:24Z" + }, + { + "author": { + "id": "MDQ6VXNlcjg4MjYxNTE2", + "is_bot": false, + "login": "DaysSky", + "name": "" + }, + "headRefName": "research/bw16-unit-screen", + "headRefOid": "3bf6fccaf17521ffdb9b3bec2740ba4886478556", + "number": 895, + "title": "No new \u03ba: BW16 as a unit \u2014 window c \u2265 72 puts its ceiling at 0.649\u00d7 E8's (checked)", + "updatedAt": "2026-10-13T10:52:37Z" + }, + { + "author": { + "id": "MDQ6VXNlcjI3NTY4NjE3", + "is_bot": false, + "login": "ToikY", + "name": "" + }, + "headRefName": "research/gaussian-nonlinear-seed44", + "headRefOid": "8c9964b7ab4419409d20762c8d78591701008d04", + "number": 888, + "title": "Research: Gaussian nonlinear message copy floor 40b under explicit width pricing", + "updatedAt": "2026-10-13T10:21:37Z" + }, + { + "author": { + "id": "MDQ6VXNlcjgyODk5MzMx", + "is_bot": false, + "login": "mightyOil", + "name": "" + }, + "headRefName": "research/e8-rank5-boundary-seed46", + "headRefOid": "7f334e4c749fd83d03feb6c1de4e4cda9534c9dc", + "number": 875, + "title": "Scoped negative result: classify the E8 rank-five boundary at 36 punctures", + "updatedAt": "2026-10-13T09:00:22Z" + }, + { + "author": { + "id": "U_kgDOFF-7zg", + "is_bot": false, + "login": "WilliamLawyer", + "name": "William Lawyer" + }, + "headRefName": "codex/decoder-information-audit-40", + "headRefOid": "54cbbea75b587bdf43a1c123e52220f936641d6f", + "number": 868, + "title": "Research: Gaussian E8 all-clique certificate ceiling is 40 (no new kappa)", + "updatedAt": "2026-10-13T08:43:03Z" + }, + { + "author": { + "id": "U_kgDOB_v2mg", + "is_bot": false, + "login": "the-missionary-company", + "name": "" + }, + "headRefName": "research/asymmetric-hypercube-decoder-seed48", + "headRefOid": "7d526020fc368ce4157cd436995c2f4fcf683318", + "number": 669, + "title": "Research: prove higher-target star-code hierarchies and decoder geometry", + "updatedAt": "2026-10-13T09:34:35Z" + }, + { + "author": { + "id": "U_kgDOCiU1ug", + "is_bot": false, + "login": "GamingPuzzled", + "name": "Joel Pulikkan" + }, + "headRefName": "research/e8-decoder-floors-and-cold14-notes", + "headRefOid": "e9cf03bbdf7094b5a83f6dbd1d74bfd77a05fb87", + "number": 620, + "title": "Research notes (no \u03ba claim): E8 decoder floors are tight; #615 levers exhausted; +1.1e-7 \u03ba owner-map headroom on #617", + "updatedAt": "2026-10-13T02:36:29Z" + }, + { + "author": { + "id": "U_kgDOClpS9w", + "is_bot": false, + "login": "DreamingOfClouds", + "name": "" + }, + "headRefName": "format-obstructions", + "headRefOid": "309482849b6ddf34db998f53612d34c19f6e3233", + "number": 446, + "title": "Format obstructions (no new \u03ba): exact bounds on window width, copy cost and label dimension", + "updatedAt": "2026-10-11T15:55:07Z" + }, + { + "author": { + "id": "MDQ6VXNlcjg4MjYxNTE2", + "is_bot": false, + "login": "DaysSky", + "name": "" + }, + "headRefName": "research/design-ceiling", + "headRefOid": "b3c128ec4c3a4ac1a095f45a8d86e387bbda05ec", + "number": 201, + "title": "A \u03ba ceiling of 2.5592e-3 for every word on #144's paired-cube design (no new \u03ba)", + "updatedAt": "2026-10-09T14:27:52Z" + }, + { + "number": 231, + "title": "The paired-cube decoder does not extend to 4-dimensional ports: a Lucas-parity obstruction (no new \u03ba)", + "headRefOid": "3c11e696a2fb2c454585d72710de27cd6bd3be68", + "status": "incorporated source at base" + } + ], + "conclusion": "No inspected PR studies the natural five-port quadratic pairing with the separate coordinate-star copy cost and all-p/all-stage active-climb ceiling.", + "final_refresh": { + "snapshot_utc": "2026-10-13T14:30:45.114614+00:00", + "open_pr_count": 707, + "highest_pr": 954, + "new_arrivals": [ + { + "headRefOid": "a98219aa708e1bd2ae4ca90e720e66569f7f0147", + "number": 954, + "title": "Scoped negative result: classify E8's first decoder rank drop (no new kappa)", + "updatedAt": "2026-10-13T14:29:38Z" + }, + { + "headRefOid": "5f052969846b0882ac4e22d9e818dd8ac05ea56f", + "number": 953, + "title": "Research construction: optimal dyadic-run BIT query batches (no new kappa)", + "updatedAt": "2026-10-13T14:28:46Z" + }, + { + "headRefOid": "11d24706f06e95271804c9438869546724c67aab", + "number": 952, + "title": "Finite bit construction: whole six-wire synthesis saves 38 further ADDs beyond PR936 (no new kappa)", + "updatedAt": "2026-10-13T14:30:05Z" + }, + { + "headRefOid": "de0c8641dcf1a4cd0abde9b897fa946de2bede49", + "number": 951, + "title": "Research: two additive cyclic inverse calls with no dirty connector (no new kappa)", + "updatedAt": "2026-10-13T14:25:45Z" + }, + { + "headRefOid": "5bafe2c91e045d10de207b9e5b21630dfebb9cd2", + "number": 950, + "title": "Tooling: 1.61x faster exact historical central-factor audit (no new kappa)", + "updatedAt": "2026-10-13T14:24:06Z" + }, + { + "headRefOid": "102ddfb47d11c8ad66121350907d4a2cc04cea8c", + "number": 949, + "title": "Scoped negative result: exact 73-primitive factory scale optimum (no new kappa)", + "updatedAt": "2026-10-13T14:21:00Z" + }, + { + "headRefOid": "eb11543094825c193c4bccece4857601fcd1620a", + "number": 948, + "title": "Independent verification: symbolic PR479 chirp state transitions (no new kappa)", + "updatedAt": "2026-10-13T14:15:54Z" + }, + { + "headRefOid": "b6f6418bdcae748b267cea72a5949d551feb7bb2", + "number": 947, + "title": "Scoped negative result: exact constant-row center shear optimum (no new kappa)", + "updatedAt": "2026-10-13T14:16:22Z" + } + ], + "pinned_coordination_issues": [], + "overlap_found": false, + "method": "Refresh of all open PR metadata; compare new arrivals and decoder/geometry keywords against the frozen scope.", + "main_head": "007664306fff84fbb1c9a1b4053b69f439764034", + "selected_kappa": "1661957774647029/1000000000000000000", + "selected_changed_since_base": false, + "pr954_body_checked": "E8 first rank-drop boundary, distinct from signed five-port quadratic geometry.", + "consumed_open_source_446_unchanged": true + } +} diff --git a/research/five-port-quadratic-decoder/PROOF.md b/research/five-port-quadratic-decoder/PROOF.md new file mode 100644 index 0000000000..57d6abf193 --- /dev/null +++ b/research/five-port-quadratic-decoder/PROOF.md @@ -0,0 +1,240 @@ +# Five-port quadratic decoder: a scoped format obstruction + +This is a written mathematical argument with exact finite rank certificates. +It is **not** a proof-assistant verification, an unrestricted decoder lower +bound, or a new integer-multiplication construction. + +## 1. Object and statement + +Let `p >= 5`. The ports are the `v = 32 binom(p,5)` five-element subsets of +`{0,...,2p-1}` containing at most one element of each pair `{2i,2i+1}`. +Write `j = |S intersect T|`. The five-port, level-one star identity over F2 is + +``` +x_T = sum_(a in T) z_a + sum_(S: |S intersect T| in {1,3}) x_S, +z_a = sum_(S: a in S) x_S. +``` + +The coefficient of `x_S` on the right is `j + 1_{j in {1,3}} (mod 2)`. +It is zero for `j = 0,...,4` and one for `j = 5`, which means `S = T`. +Joel Pulikkan's PR231 establishes the parity context and explicitly leaves +the geometry and cost of `k=5` open. We investigate **one** geometry: + +``` +G(S,T) = 2(j-1)(j-3). +``` + +The theorem concerns every rational common-label realization of this Gram +matrix, with the displayed correction terms delivered drop-free and each +of the `2p` coordinate-star totals gathered drop-free and copied separately +to all its coordinate-star readers in each stage, under the accounting +premises in section 4. The copy of one total may use a tree or split its +readers; mixing different totals into a new coded message is outside scope. + +**Theorem.** In this class, no positive supplier saving is possible at +`p=5,6,7`. For every `p >= 5` and every integer number of stages `s >= 3`, +any positive supplier saving `gamma` satisfies + +``` +gamma < 125/76433 = 0.0016354192560804888... . +``` + +This is below the **frozen, maintainer-reviewed** selected +`kappa = 1661957774647029/10^18` at base +`47481c89fd30a43f8f882eb4b391e89c29273fd0`. Since the inherited assembly +requires kappa below its bit supplier saving, this decoder class cannot +improve that selected result, even if the other supplier is free. The +number above is an upper bound on a proposed supplier class, **not a +new certified kappa**. + +## 2. Why a new geometry is needed + +Fix five coordinate pairs. Among their 32 orientations, take the 16 whose +number of odd coordinates is even. Two distinct such ports differ in two +or four coordinates, hence have intersection three or one. The decoder +requires a drop-free correction between every two distinct ports in this +set. Under the common-label frame rule, their nonisotropic rank-one labels +must be pairwise orthogonal. They are therefore linearly independent. + +In contrast, affine functions of the five orientation bits span a space +of dimension at most six. Any linear transformation of the original +ten incidence coordinates, even with a constant coordinate and an +arbitrary symmetric rational bilinear form, still has label span at most +six on this cube. Thus the old incidence-linear geometry cannot realize +this correction pattern. This is not merely a failure of a symmetric +choice of bilinear form. + +A quadratic lift does realize the required zeros. Use feature coordinates +`1`, `1_{a in S}`, and `1_{{a,b} subset S}` for pairs of coordinates from +distinct coordinate pairs. Give the three groups diagonal form weights +`6`, `-6`, and `4`, respectively. The resulting rational symmetric form is +nondegenerate on this feature space, and + +``` + = 6 - 6j + 4 binom(j,2) = 2(j-1)(j-3). +``` + +In particular the diagonal is 16 and both correction classes are +orthogonal. The form is indefinite; positive definiteness is not claimed +or needed for the retained rational frame model. Up to scaling, this is +the unique nonzero polynomial in `j` of degree at most two that vanishes +at one and three. The 16-orientation clique attains rank 16 inside one +cube for this lift. The rest of this note shows why algebraic admissibility +alone does not make the lift useful. + +## 3. Finite rank certificates and the infinite tail + +Let `N_T` be all ports intersecting target `T` in one or three coordinates. +Let `P_a` be all ports containing coordinate `a`. The two needed ranks are: + +- `d_p <= rank G[N_T,N_T]`, a lower bound on the bilinear rank of the + drop-free corrector space; +- `r_p <= rank G[P_a,P_a]`, a lower bound on the source/reader pairing rank + for the separate total `z_a`. + +Permuting coordinate pairs and swapping the two coordinates of any pair +preserves both the port family and `G`. This group acts transitively on +targets and on coordinates. A witness at the canonical target +`{0,2,4,6,8}` and coordinate `0` therefore applies to **every** target or +star at that `p`. + +| p | v | d_p | r_p | c_p = 2p r_p | +|---|---:|---:|---:|---:| +| 5 | 32 | 15 | 11 | 110 | +| 6 | 192 | 50 | 35 | 420 | +| 7 | 672 | 83 | 60 | 840 | +| 8 | 1,792 | 111 | 84 | 1,344 | +| 9 | 4,032 | 143 | 112 | 2,016 | +| 10 | 8,064 | 179 | 144 | 2,880 | +| 11 | 14,784 | 219 | 170 | 3,740 | +| 12 | 25,344 | 263 | 210 | 5,040 | +| 13 | 41,184 | 311 | not needed | granted zero in tail | + +`WITNESSES.json` contains the row and column ports of 17 square minors, +their dimensions, and their nonzero determinants modulo **65521**. Each +entry is an integer. A determinant nonzero modulo a prime is a nonzero +integer determinant, so each minor proves the stated **rational lower +bound**. This implication is exact; it is not a probabilistic modular-rank +estimate and needs no determinant height bound. The row and column sets +may differ; both lie in the same stated neighborhood or star. + +The proof needs only these lower bounds. It does not assume that the +listed ranks are maximal. In particular it does **not** extrapolate the +ordinary star values to 180 at `p=11` or 220 at `p=12`: discovery found +degenerate pairings there, and the actual witnesses certify 170 and 210. +No all-parameter rank formula or unverified numerical rank is a premise. + +For **every `p >= 13`**, fix any target and choose eight additional +coordinate pairs. The 13 selected pairs contain an isometric copy of the +entire `p=13` configuration, including its corrector minor. Consequently +every target has corrector rank at least **311**. This embedding, together +with the finite certificate, proves the all-p tail statement. It is not +an inference from failure to find a better candidate in a finite search. + +## 4. Explicit accounting premises and optimistic budget + +We retain the following common-label, compressed-window accounting +premises. They specialize DreamingOfClouds' PR446 Theorems B/C and the +format-limit axioms `(P)`, `(Dfc)`, `(Win)`, `(Sch)`, `(Bat)` to the present +decoder. The retained sources are pinned in `SOURCES.json`. We do not +claim to prove their all-size machine realization here. + +1. There are `s >= 3` stages, one active source/target bank pair per stage, + rank-one data labels, drop-free delivery of the displayed correctors, + and a common stage climb `a`. Corrector rank forces `a >= d_p`. + The retained fixed-window `(Win)` accounting requires ambient dimension + `m >= 1+s*a`. This last relation is an explicit format premise; the + rank witnesses alone would only force `m >= 1+s*d_p`. +2. At each stage, each of the `2p` totals is gathered **drop-free** from + `P_a` and delivered to `P_a` through its own rooted copy tree. The + pairing-rank drop bound is paid **additively + for these separate totals**, so per-stage copy charge `c >= c_p`. +3. Per replica, the pressure deficit obeys + `D <= (s-1)v - s*c`. For paid recursive children of ranks `00`, `exp(x)-1 >= x` and `m/a > s >= 3` give + +``` +D >= 2sva((m/a)^gamma - 1) + > 2sv d_p gamma log(3). +``` + +Combining with the deficit bound and discarding the favorable `-1/s` +term yields + +``` +gamma < (1 - c_p/v) / (2 d_p log(3)). +``` + +If `c_p >= v`, the deficit is negative at every positive `s`; this +settles `p=5,6,7` before implementing any supplier. + +For a rational bound, the first six positive terms of + +``` +log(3) = 2 sum_(i>=0) (1/2)^(2i+1)/(2i+1) +``` + +already exceed `549/500`. The verifier checks that strict inequality +using `Fraction`, with no logarithm library or floating point. Substitution +gives the following strict supplier upper bounds: + +| p | rational upper bound | +|---|---| +| 8 | `125/121878` | +| 9 | `125/78507` | +| 10 | **`125/76433`** | +| 11 | `31375/20198808` | +| 12 | `5875/4235352` | + +For `p >= 13`, grant **even the copies** zero cost and use `d_p >= 311`: + +``` +gamma < 1/(2*311*log(3)) < 250/170739 < 125/76433. +``` + +All comparisons, including the strict gap to the frozen selected kappa, +are rational and reproduced by the checker. No stage-count cutoff is +used: `s>=3` was eliminated algebraically. This completes the theorem. + +## 5. Boundaries + +This closes the **specified natural quadratic Gram / separate coordinate +star / compressed-window accounting** class. It does not close other +quadratic label pairings, asymmetric labels, coded combinations of stars, +punctured ports, higher-star decoders, retained cross-stage information, +paid non-drop-free gathers or corrections, or a different bank schedule. +It makes no claim that a stronger kappa +exists in those classes. + +There is no circuit, hosted profile, all-size compiler or assembly +certificate here. Realization, common-label/mutable-source validity, +whole-call hosting, restoration, precision/tape, bit H1–H5 and analytic +transfer remain inherited obligations for any actual construction. +Finite exact rank verification does not discharge them. diff --git a/research/five-port-quadratic-decoder/README.md b/research/five-port-quadratic-decoder/README.md new file mode 100644 index 0000000000..065527f923 --- /dev/null +++ b/research/five-port-quadratic-decoder/README.md @@ -0,0 +1,93 @@ +# Five-port quadratic decoder: an optimistic cost obstruction + +**Research note / scoped negative result. No new kappa or physical supplier.** + +PR231 shows that five-coordinate ports admit a level-one XOR star decoder, +but leaves its geometry and pricing open. This package checks the natural +quadratic pairing `G(S,T)=2(|S intersect T|-1)(|S intersect T|-3)`. + +The old incidence-linear geometry is impossible: 16 mutually orthogonal +nonzero labels inside one cube would have to fit in dimension at most six. +The quadratic lift supplies the required geometry, but its copied stars +and active frame work alone imply + +``` +supplier saving < 125/76433 = 0.0016354192560804888... +``` + +This is below the selected conditional **kappa = 0.001661957774647029** at +base **47481c89fd30a43f8f882eb4b391e89c29273fd0**. It covers every `p>=5` +coordinate-pair count and every `s>=3` stage count **within the explicit +separate-star, drop-free-correction, compressed-window premises**. +All other work is optimistically granted zero cost. This is a ceiling on +one proposed format, not an achievable bound or an unrestricted decoder +impossibility theorem. Read [PROOF.md](PROOF.md) for the precise premises. + +## Reproduce + +From the repository root, offline, Python 3.10+ and the standard library: + +```sh +python3 -I -B research/five-port-quadratic-decoder/verify.py +``` + +Expected: + +```text +PASS_FIVE_PORT_QUADRATIC_DECODER witnesses=17 ceiling=125/76433 tail=250/170739 controls=9 no_new_kappa +``` + +The script checks 17 literal integer minors modulo the checked prime +65521, 37,888 small-instance source/target coefficients, the 16-port parity +clique, the rational logarithm and cost inequalities, four source pins, +and nine adverse controls. A nonzero modular minor is exact evidence of +a rational rank **lower bound**, not a numerical rank estimate. + +Two supplementary commands check the same rank obligations using a +separately written feature-pairing implementation and fraction-free +elimination at prime 65519, and exercise six package tests: + +```sh +python3 -I -B research/five-port-quadratic-decoder/independent.py +python3 -I -B research/five-port-quadratic-decoder/test_package.py +``` + +The second implementation also computes two integer determinants exactly. +It was written by the same AI-assisted contributor and is **not independent +human review**. Both checkers support optimized Python and compare their +computed receipts to the committed JSON. `--write-certificate PATH` creates +a new receipt exclusively, so an existing file is never overwritten. + +## Evidence and scope + +- [WITNESSES.json](WITNESSES.json): explicit row/column port labels for + corrector minors at `p=5..13` and separate-star minors at `p=5..12`. +- [CERTIFICATE.json](CERTIFICATE.json) and [INDEPENDENT.json](INDEPENDENT.json): + exact residues and rational comparisons, including the strict gap to + the selected value frozen at the base commit. +- [PROOF.md](PROOF.md): the scalar identity, linear-label obstruction, + quadratic lift, finite rank implications, all-p embedding and all-stage + cost argument. The infinite tail uses the `p=13` minor, not a search + extrapolation. +- [SOURCES.json](SOURCES.json) and [NOTICE.md](NOTICE.md): dependency pins, + original attribution and AI disclosure. +- [CLAIM.json](CLAIM.json), [OVERLAP.json](OVERLAP.json) and + [VALIDATION.md](VALIDATION.md): sprint scope, overlap and handoff evidence. + +`discover.py` records a deterministic witness-construction pass with seed +40. It enumerates the full candidate port families, shuffles each list, +and stops each greedy feature-basis selection at the size recorded in +`WITNESSES.json`. It then extracts a nonsingular pairing minor. There is +no optimizer or search-optimality premise; discovery is not imported by +either checker. It refuses to overwrite its committed witnesses. + +Different Gram pairings, coded totals, punctures, paid non-drop-free +corrections/gathers, and different stage accounting are outside scope. +The selected frontier and `upstream/` are unchanged. All-size realization, +common-label/mutable-source validity, hosting, precision/tape, bit H1–H5, +and analytic transfer remain inherited obligations for any actual supplier. +No complete multiplication theorem, hosted CI pass, or new kappa is claimed. + +Prepared by **Ross Richardson (@RossRichardson)** with substantial **OpenAI +Codex assistance**. Apache-2.0. The written argument and second checker +still need external review. diff --git a/research/five-port-quadratic-decoder/SOURCES.json b/research/five-port-quadratic-decoder/SOURCES.json new file mode 100644 index 0000000000..af60a41067 --- /dev/null +++ b/research/five-port-quadratic-decoder/SOURCES.json @@ -0,0 +1,35 @@ +{ + "repository": "CrocSwap/integer-mult-bounds", + "base_commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "files": [ + { + "path": "sources/pr231-README.md", + "source_path": "research/hypercube-decoder-parity/README.md", + "commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "sha256": "2dc89289d1d979aec6709b8c55a2af7cd39d97297bc20fb94adc7d4cdf867cd1", + "git_blob_sha1": "3a13dfd89b801a0a72db7ef50be7d324addc7949" + }, + { + "path": "sources/format-axioms-README.md", + "source_path": "research/format-limits/README.md", + "commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "sha256": "0fa0d6b2df96ddc06b876c41c5fa8d2335b97f36bc8f17d1371296d23199c263", + "git_blob_sha1": "2f7aaf5b8225717394fe6adda6b313026eaf8090" + }, + { + "path": "sources/selected-result-base.json", + "source_path": "certificates/selected-result.json", + "commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "sha256": "41fb066ff0f43ce472323195e9088d6d888715c13c54eae7b42e357ed5bfc726", + "git_blob_sha1": "5dbfac5424703adbb97f38edbdcaea4627215132" + }, + { + "path": "sources/pr446-PROOF.md", + "source_path": "research/format-obstructions/PROOF.md", + "commit": "309482849b6ddf34db998f53612d34c19f6e3233", + "pr": 446, + "sha256": "7a8c3bab633c08e7d96297dec9f9e7ed68d6bd0e076b73310c7d6b08a16df017", + "git_blob_sha1": "d2e0ffc6639bf3504b68bccc381a0ee172f98fef" + } + ] +} diff --git a/research/five-port-quadratic-decoder/VALIDATION.md b/research/five-port-quadratic-decoder/VALIDATION.md new file mode 100644 index 0000000000..7bc5cf7443 --- /dev/null +++ b/research/five-port-quadratic-decoder/VALIDATION.md @@ -0,0 +1,64 @@ +# Verification and handoff + +Exact base: `47481c89fd30a43f8f882eb4b391e89c29273fd0`. +Branch: `research/structural-decoder-seed40`. +Contribution type: **research note / scoped negative result**. + +## Completed checks + +- CPython **3.12.12**, isolated optimized execution: the primary checker + accepts all 17 explicit minors, exact decoder/coefficient checks, rational + ceiling and nine mathematical/contract rejection controls. +- CPython **3.14.6**, isolated optimized execution: the separately written + set-feature / Bareiss checker accepts all 17 minors at a second prime, + computes two integer determinants, and obtains the identical rational ceiling. +- All **six package tests** pass. They compare both elimination implementations + with the permutation definition on 123 matrices, reject omitted obligations + and changed source text, exercise a singular minor with distinct valid labels, + and distinguish a scalar-valid decoder from invalid linear geometry. +- A clean export of the canonical staged Git blobs to a directory containing + spaces passes both optimized checkers. Both regenerated receipts are + **byte-identical** to the committed receipts. Existing output-file preservation + is checked through the real CLI: rejection leaves the sentinel bytes intact. +- `make selected-record-check` passes. The selected certificate and `upstream/` + have no changes. Staged whitespace validation passes. + +Exact commands, exit statuses, runtimes and the exported tree identity are +in `evidence/checks.json` and `evidence/clean-export.json`; stdout is retained +beside them. Timings are evidence of completion, not a performance claim. + +## Coverage and limits + +The 17 minors cover corrector rank at p=5..13 and star pairing rank at p=5..12. +Their validity extends to every target/star by the written permutation argument. +The p>=13 extension is proved by embedding the p=13 corrector witness; the +all-stage result follows from the displayed inequalities for every s>=3. +No failed finite search is called an impossibility theorem. + +The result assumes the exact quadratic Gram, independent source variables, +drop-free gathers and corrections, separately charged star totals, and the +fixed-window pressure/active-climb accounting. It implements no supplier. +All-size realization, common-label/mutable-source, hosting, precision/tape, +bit H1-H5 and analytic obligations remain. Neither checker is a formal +multiplication proof; both implementations were prepared by the same +AI-assisted contributor and need external review. + +Full repository-wide `make verify`, unchanged supplier cold replays, Linux +and hosted CI were **not run or claimed** for this isolated research package. +No shared generator, existing test, global certificate or selected source was +changed. Reproduction of this result takes only the standalone commands in +README.md. + +## Overlap and current context + +The initial snapshot contained 717 open PRs. The final full refresh contained +707 through PR954, with no duplicate five-port quadratic result. PR954's body +was read: it concerns E8's first punctured-reader rank loss and is distinct. +PR446's consumed head is unchanged. The newly fetched main is +`007664306fff84fbb1c9a1b4053b69f439764034`; it still selects PR890 at +`1661957774647029/10^18`. The contribution retains its exact earlier base and +immutable source pins. Its new package path is absent from refreshed main. + +There is no pinned sprint coordination issue. The claim is local; the completed +result is linked there. Publication and CI status belong to the PR handoff, +not to the finite mathematical certificate. No merge is authorized or attempted. diff --git a/research/five-port-quadratic-decoder/WITNESSES.json b/research/five-port-quadratic-decoder/WITNESSES.json new file mode 100644 index 0000000000..5e6724c373 --- /dev/null +++ b/research/five-port-quadratic-decoder/WITNESSES.json @@ -0,0 +1,4650 @@ +{ + "schema": "five-port-quadratic-rank-witnesses-v1", + "seed": 40, + "prime": 65521, + "kernel_coefficients": [ + 6, + -8, + 2 + ], + "witnesses": [ + { + "p": 5, + "kind": "corrector", + "target": 341, + "rank_lower": 15, + "rows": [ + 406, + 681, + 613, + 421, + 666, + 601, + 409, + 618, + 346, + 598, + 661, + 361, + 678, + 426, + 358 + ], + "columns": [ + 406, + 681, + 613, + 421, + 666, + 601, + 409, + 618, + 346, + 598, + 661, + 361, + 678, + 426, + 358 + ], + "determinant_mod_prime": 64590, + "candidate_count": 15, + "candidates_visited": 15, + "feature_basis_size": 15 + }, + { + "p": 5, + "kind": "star", + "target": 1, + "rank_lower": 11, + "rows": [ + 409, + 357, + 361, + 597, + 617, + 425, + 661, + 601, + 613, + 345, + 681 + ], + "columns": [ + 409, + 357, + 361, + 597, + 617, + 425, + 661, + 601, + 613, + 345, + 681 + ], + "determinant_mod_prime": 7200, + "candidate_count": 16, + "candidates_visited": 11, + "feature_basis_size": 11 + }, + { + "p": 6, + "kind": "corrector", + "target": 341, + "rank_lower": 50, + "rows": [ + 1562, + 1110, + 2449, + 1605, + 2629, + 2581, + 2706, + 361, + 613, + 2202, + 1113, + 618, + 1620, + 1418, + 2149, + 1193, + 2712, + 1577, + 1557, + 406, + 1697, + 1670, + 1673, + 2401, + 2137, + 1362, + 1442, + 1125, + 2386, + 2374, + 409, + 1428, + 2377, + 2341, + 2598, + 2664, + 601, + 2326, + 1302, + 1190, + 2452, + 2658, + 1368, + 346, + 2442, + 1173, + 1574, + 2214, + 2154, + 2437 + ], + "columns": [ + 1562, + 1110, + 2449, + 1605, + 2629, + 2581, + 2706, + 361, + 613, + 2202, + 1113, + 618, + 1620, + 1418, + 2149, + 1193, + 2712, + 1577, + 1557, + 406, + 1697, + 1670, + 1673, + 2401, + 2137, + 1362, + 1442, + 1125, + 2386, + 2374, + 409, + 1428, + 2377, + 2341, + 2598, + 2664, + 601, + 2326, + 1302, + 1190, + 2452, + 2658, + 1368, + 346, + 2442, + 1173, + 1574, + 2214, + 2154, + 2437 + ], + "determinant_mod_prime": 39381, + "candidate_count": 95, + "candidates_visited": 63, + "feature_basis_size": 50 + }, + { + "p": 6, + "kind": "star", + "target": 1, + "rank_lower": 35, + "rows": [ + 1441, + 1129, + 2341, + 681, + 2217, + 2705, + 2201, + 2133, + 2441, + 1125, + 2585, + 425, + 1109, + 2449, + 1573, + 2633, + 2373, + 1577, + 1617, + 2325, + 2345, + 421, + 617, + 1305, + 2377, + 1177, + 1173, + 1377, + 2581, + 409, + 1681, + 2465, + 1361, + 665, + 1353 + ], + "columns": [ + 1441, + 1129, + 2341, + 681, + 2217, + 2705, + 2201, + 2133, + 2441, + 1125, + 2585, + 425, + 1109, + 2449, + 1573, + 2633, + 2373, + 1577, + 1617, + 2325, + 2345, + 421, + 617, + 1305, + 2377, + 1177, + 1173, + 1377, + 2581, + 409, + 1681, + 2465, + 1361, + 665, + 1353 + ], + "determinant_mod_prime": 16722, + "candidate_count": 80, + "candidates_visited": 42, + "feature_basis_size": 35 + }, + { + "p": 7, + "kind": "corrector", + "target": 341, + "rank_lower": 83, + "rows": [ + 2452, + 2712, + 5761, + 10321, + 9800, + 4202, + 4485, + 10881, + 5728, + 6278, + 1425, + 661, + 9350, + 2374, + 8785, + 2137, + 1574, + 9257, + 10344, + 2341, + 1577, + 9761, + 5641, + 613, + 1670, + 8730, + 10309, + 6468, + 8868, + 10314, + 8545, + 9764, + 2149, + 10536, + 8490, + 5668, + 1634, + 2697, + 6170, + 1448, + 4425, + 8470, + 2472, + 2466, + 6434, + 8802, + 8856, + 1110, + 1173, + 4629, + 2386, + 1130, + 10785, + 2581, + 4250, + 8593, + 4634, + 4742, + 2437, + 681, + 2598, + 10404, + 1178, + 6480, + 5141, + 8778, + 9320, + 2134, + 10576, + 1350, + 1377, + 5393, + 2721, + 361, + 8346, + 9368, + 4677, + 5386, + 6680, + 10506, + 5416, + 8581, + 10278 + ], + "columns": [ + 2452, + 2712, + 5761, + 10321, + 9800, + 4202, + 4485, + 10881, + 5728, + 6278, + 1425, + 661, + 9350, + 2374, + 8785, + 2137, + 1574, + 9257, + 10344, + 2341, + 1577, + 9761, + 5641, + 613, + 1670, + 8730, + 10309, + 6468, + 8868, + 10314, + 8545, + 9764, + 2149, + 10536, + 8490, + 5668, + 1634, + 2697, + 6170, + 1448, + 4425, + 8470, + 2472, + 2466, + 6434, + 8802, + 8856, + 1110, + 1173, + 4629, + 2386, + 1130, + 10785, + 2581, + 4250, + 8593, + 4634, + 4742, + 2437, + 681, + 2598, + 10404, + 1178, + 6480, + 5141, + 8778, + 9320, + 2134, + 10576, + 1350, + 1377, + 5393, + 2721, + 361, + 8346, + 9368, + 4677, + 5386, + 6680, + 10506, + 5416, + 8581, + 10278 + ], + "determinant_mod_prime": 45089, + "candidate_count": 335, + "candidates_visited": 83, + "feature_basis_size": 83 + }, + { + "p": 7, + "kind": "star", + "target": 1, + "rank_lower": 60, + "rows": [ + 2641, + 10501, + 5441, + 8361, + 6217, + 2133, + 6213, + 6673, + 8357, + 10513, + 8741, + 1321, + 2149, + 2657, + 8729, + 6665, + 5381, + 4393, + 5217, + 10385, + 8585, + 9505, + 2597, + 4677, + 8841, + 8521, + 357, + 5281, + 8849, + 1561, + 1109, + 2325, + 4689, + 5257, + 9477, + 2693, + 9793, + 8341, + 421, + 1417, + 1413, + 4769, + 5157, + 4377, + 4265, + 9289, + 10277, + 1441, + 4245, + 8837, + 1189, + 405, + 10265, + 8345, + 5649, + 4681, + 5253, + 2721, + 4629, + 597 + ], + "columns": [ + 2641, + 10501, + 5441, + 8361, + 6217, + 2133, + 6213, + 6673, + 8357, + 10513, + 8741, + 1321, + 2149, + 2657, + 8729, + 6665, + 5381, + 4393, + 5217, + 10385, + 8585, + 9505, + 2597, + 4677, + 8841, + 8521, + 357, + 5281, + 8849, + 1561, + 1109, + 2325, + 4689, + 5257, + 9477, + 2693, + 9793, + 8341, + 421, + 1417, + 1413, + 4769, + 5157, + 4377, + 4265, + 9289, + 10277, + 1441, + 4245, + 8837, + 1189, + 405, + 10265, + 8345, + 5649, + 4681, + 5253, + 2721, + 4629, + 597 + ], + "determinant_mod_prime": 48334, + "candidate_count": 240, + "candidates_visited": 60, + "feature_basis_size": 60 + }, + { + "p": 8, + "kind": "corrector", + "target": 341, + "rank_lower": 111, + "rows": [ + 18768, + 17794, + 34313, + 37984, + 34340, + 5254, + 1425, + 26888, + 22017, + 35460, + 33066, + 34184, + 26660, + 2149, + 6417, + 5761, + 22564, + 4202, + 16773, + 20617, + 1442, + 38017, + 42512, + 21636, + 32857, + 37382, + 24713, + 6213, + 21600, + 42050, + 17477, + 20549, + 25094, + 17986, + 6800, + 9512, + 2641, + 2154, + 8586, + 25184, + 43152, + 39425, + 18530, + 17512, + 16713, + 40986, + 1130, + 26116, + 17042, + 42242, + 17000, + 33192, + 34208, + 598, + 358, + 33833, + 41236, + 426, + 4485, + 4377, + 17057, + 27152, + 17446, + 32854, + 27008, + 2341, + 16785, + 661, + 4754, + 2706, + 22600, + 41124, + 5189, + 22624, + 35137, + 35140, + 33121, + 16682, + 34068, + 32934, + 6405, + 17732, + 38272, + 18722, + 20521, + 6305, + 20554, + 24674, + 34436, + 37960, + 43140, + 4182, + 8865, + 10770, + 5776, + 41616, + 5416, + 37250, + 41544, + 35472, + 2449, + 18950, + 6281, + 37001, + 24837, + 8788, + 6480, + 41538, + 21001, + 26690, + 37412 + ], + "columns": [ + 18768, + 17794, + 34313, + 37984, + 34340, + 5254, + 1425, + 26888, + 22017, + 35460, + 33066, + 34184, + 26660, + 2149, + 6417, + 5761, + 22564, + 4202, + 16773, + 20617, + 1442, + 38017, + 42512, + 21636, + 32857, + 37382, + 24713, + 6213, + 21600, + 42050, + 17477, + 20549, + 25094, + 17986, + 6800, + 9512, + 2641, + 2154, + 8586, + 25184, + 43152, + 39425, + 18530, + 17512, + 16713, + 40986, + 1130, + 26116, + 17042, + 42242, + 17000, + 33192, + 34208, + 598, + 358, + 33833, + 41236, + 426, + 4485, + 4377, + 17057, + 27152, + 17446, + 32854, + 27008, + 2341, + 16785, + 661, + 4754, + 2706, + 22600, + 41124, + 5189, + 22624, + 35137, + 35140, + 33121, + 16682, + 34068, + 32934, + 6405, + 17732, + 38272, + 18722, + 20521, + 6305, + 20554, + 24674, + 34436, + 37960, + 43140, + 4182, + 8865, + 10770, + 5776, + 41616, + 5416, + 37250, + 41544, + 35472, + 2449, + 18950, + 6281, + 37001, + 24837, + 8788, + 6480, + 41538, + 21001, + 26690, + 37412 + ], + "determinant_mod_prime": 47175, + "candidate_count": 895, + "candidates_visited": 111, + "feature_basis_size": 111 + }, + { + "p": 8, + "kind": "star", + "target": 1, + "rank_lower": 84, + "rows": [ + 4769, + 1173, + 32873, + 43265, + 16709, + 26881, + 41121, + 33045, + 2325, + 26689, + 10881, + 20741, + 8837, + 2581, + 20753, + 20521, + 6665, + 6185, + 20625, + 37441, + 25665, + 34177, + 6409, + 10757, + 33413, + 16721, + 9253, + 43521, + 1413, + 2133, + 4633, + 41097, + 5141, + 5649, + 18569, + 32937, + 24601, + 37249, + 34853, + 6433, + 24597, + 20561, + 6289, + 4681, + 1681, + 22657, + 6305, + 8609, + 17545, + 21121, + 33361, + 39169, + 2377, + 10281, + 2641, + 5189, + 17429, + 16965, + 18697, + 17729, + 24657, + 5393, + 4741, + 21761, + 36937, + 17541, + 2329, + 2697, + 33169, + 6673, + 17697, + 20865, + 16489, + 16933, + 34081, + 4513, + 33441, + 8745, + 8473, + 36997, + 18469, + 4645, + 5441, + 32853 + ], + "columns": [ + 4769, + 1173, + 32873, + 43265, + 16709, + 26881, + 41121, + 33045, + 2325, + 26689, + 10881, + 20741, + 8837, + 2581, + 20753, + 20521, + 6665, + 6185, + 20625, + 37441, + 25665, + 34177, + 6409, + 10757, + 33413, + 16721, + 9253, + 43521, + 1413, + 2133, + 4633, + 41097, + 5141, + 5649, + 18569, + 32937, + 24601, + 37249, + 34853, + 6433, + 24597, + 20561, + 6289, + 4681, + 1681, + 22657, + 6305, + 8609, + 17545, + 21121, + 33361, + 39169, + 2377, + 10281, + 2641, + 5189, + 17429, + 16965, + 18697, + 17729, + 24657, + 5393, + 4741, + 21761, + 36937, + 17541, + 2329, + 2697, + 33169, + 6673, + 17697, + 20865, + 16489, + 16933, + 34081, + 4513, + 33441, + 8745, + 8473, + 36997, + 18469, + 4645, + 5441, + 32853 + ], + "determinant_mod_prime": 40322, + "candidate_count": 560, + "candidates_visited": 84, + "feature_basis_size": 84 + }, + { + "p": 9, + "kind": "corrector", + "target": 341, + "rank_lower": 143, + "rows": [ + 98345, + 71746, + 24657, + 131605, + 147746, + 131688, + 140324, + 17681, + 100484, + 65625, + 140321, + 164481, + 66209, + 82450, + 2721, + 6800, + 37028, + 37394, + 4245, + 67605, + 37160, + 18569, + 34058, + 41058, + 67168, + 25666, + 66074, + 74384, + 1173, + 37154, + 131496, + 168512, + 20998, + 42008, + 99841, + 22032, + 141825, + 65930, + 87041, + 41346, + 148489, + 1620, + 149576, + 73826, + 9602, + 18596, + 71752, + 147792, + 140546, + 9353, + 71172, + 8730, + 91392, + 163861, + 163938, + 41993, + 136321, + 67138, + 172161, + 24680, + 33066, + 151588, + 16937, + 131745, + 132248, + 35457, + 86400, + 4434, + 156176, + 136456, + 98565, + 106568, + 70150, + 166176, + 98441, + 140804, + 34310, + 82465, + 9350, + 135554, + 135713, + 16473, + 68168, + 164385, + 98450, + 168032, + 6728, + 35092, + 6680, + 4394, + 9794, + 168320, + 74246, + 21768, + 6752, + 8742, + 25220, + 10561, + 18453, + 1302, + 4262, + 16662, + 35424, + 86529, + 33444, + 99904, + 168194, + 42512, + 16538, + 98882, + 67078, + 8745, + 151576, + 139905, + 661, + 9632, + 136228, + 147525, + 4677, + 10374, + 34977, + 65834, + 164113, + 4377, + 99424, + 132674, + 72064, + 20554, + 165152, + 67718, + 165954, + 9254, + 1577, + 141336, + 74372, + 41601, + 98456, + 33426, + 139525, + 157712, + 9824, + 131425, + 35140 + ], + "columns": [ + 98345, + 71746, + 24657, + 131605, + 147746, + 131688, + 140324, + 17681, + 100484, + 65625, + 140321, + 164481, + 66209, + 82450, + 2721, + 6800, + 37028, + 37394, + 4245, + 67605, + 37160, + 18569, + 34058, + 41058, + 67168, + 25666, + 66074, + 74384, + 1173, + 37154, + 131496, + 168512, + 20998, + 42008, + 99841, + 22032, + 141825, + 65930, + 87041, + 41346, + 148489, + 1620, + 149576, + 73826, + 9602, + 18596, + 71752, + 147792, + 140546, + 9353, + 71172, + 8730, + 91392, + 163861, + 163938, + 41993, + 136321, + 67138, + 172161, + 24680, + 33066, + 151588, + 16937, + 131745, + 132248, + 35457, + 86400, + 4434, + 156176, + 136456, + 98565, + 106568, + 70150, + 166176, + 98441, + 140804, + 34310, + 82465, + 9350, + 135554, + 135713, + 16473, + 68168, + 164385, + 98450, + 168032, + 6728, + 35092, + 6680, + 4394, + 9794, + 168320, + 74246, + 21768, + 6752, + 8742, + 25220, + 10561, + 18453, + 1302, + 4262, + 16662, + 35424, + 86529, + 33444, + 99904, + 168194, + 42512, + 16538, + 98882, + 67078, + 8745, + 151576, + 139905, + 661, + 9632, + 136228, + 147525, + 4677, + 10374, + 34977, + 65834, + 164113, + 4377, + 99424, + 132674, + 72064, + 20554, + 165152, + 67718, + 165954, + 9254, + 1577, + 141336, + 74372, + 41601, + 98456, + 33426, + 139525, + 157712, + 9824, + 131425, + 35140 + ], + "determinant_mod_prime": 15656, + "candidate_count": 2015, + "candidates_visited": 194, + "feature_basis_size": 143 + }, + { + "p": 9, + "kind": "star", + "target": 1, + "rank_lower": 112, + "rows": [ + 2601, + 132241, + 74369, + 172545, + 66693, + 9297, + 67605, + 2437, + 37897, + 33413, + 163865, + 147977, + 66581, + 10385, + 26657, + 84225, + 67681, + 69769, + 133761, + 75009, + 84033, + 66145, + 41029, + 8281, + 4649, + 67729, + 37009, + 6185, + 82305, + 43041, + 10373, + 132673, + 9353, + 8489, + 65925, + 139397, + 102465, + 73873, + 5145, + 83977, + 75785, + 35457, + 2217, + 98825, + 65865, + 157697, + 26641, + 139345, + 151809, + 41093, + 131489, + 74017, + 148609, + 82017, + 34321, + 4249, + 20997, + 82441, + 141825, + 147973, + 136257, + 67857, + 155681, + 165953, + 33321, + 34853, + 65621, + 38401, + 22545, + 4197, + 33953, + 2377, + 164881, + 38017, + 601, + 155665, + 173057, + 139409, + 32873, + 100361, + 4513, + 82057, + 164357, + 139781, + 9733, + 98881, + 74049, + 66597, + 131157, + 38945, + 26113, + 139785, + 23041, + 6169, + 70209, + 147589, + 83985, + 106625, + 37249, + 132625, + 17985, + 91137, + 21509, + 147717, + 67849, + 35337, + 67745, + 169985, + 20865, + 76033, + 136225, + 81993 + ], + "columns": [ + 2601, + 132241, + 74369, + 172545, + 66693, + 9297, + 67605, + 2437, + 37897, + 33413, + 163865, + 147977, + 66581, + 10385, + 26657, + 84225, + 67681, + 69769, + 133761, + 75009, + 84033, + 66145, + 41029, + 8281, + 4649, + 67729, + 37009, + 6185, + 82305, + 43041, + 10373, + 132673, + 9353, + 8489, + 65925, + 139397, + 102465, + 73873, + 5145, + 83977, + 75785, + 35457, + 2217, + 98825, + 65865, + 157697, + 26641, + 139345, + 151809, + 41093, + 131489, + 74017, + 148609, + 82017, + 34321, + 4249, + 20997, + 82441, + 141825, + 147973, + 136257, + 67857, + 155681, + 165953, + 33321, + 34853, + 65621, + 38401, + 22545, + 4197, + 33953, + 2377, + 164881, + 38017, + 601, + 155665, + 173057, + 139409, + 32873, + 100361, + 4513, + 82057, + 164357, + 139781, + 9733, + 98881, + 74049, + 66597, + 131157, + 38945, + 26113, + 139785, + 23041, + 6169, + 70209, + 147589, + 83985, + 106625, + 37249, + 132625, + 17985, + 91137, + 21509, + 147717, + 67849, + 35337, + 67745, + 169985, + 20865, + 76033, + 136225, + 81993 + ], + "determinant_mod_prime": 42257, + "candidate_count": 1120, + "candidates_visited": 112, + "feature_basis_size": 112 + }, + { + "p": 10, + "kind": "corrector", + "target": 341, + "rank_lower": 179, + "rows": [ + 133638, + 6308, + 301057, + 18962, + 591968, + 283137, + 664580, + 329220, + 327844, + 163924, + 131473, + 413700, + 71776, + 409, + 131428, + 530468, + 74258, + 533636, + 156032, + 86148, + 361024, + 172041, + 657552, + 139872, + 528518, + 397336, + 1682, + 541729, + 6228, + 336448, + 530438, + 264728, + 163986, + 623105, + 25696, + 148513, + 18530, + 430144, + 297476, + 16722, + 524677, + 262760, + 17033, + 280612, + 74264, + 591136, + 279570, + 82018, + 19016, + 530696, + 135444, + 24897, + 590090, + 66117, + 76040, + 41296, + 108548, + 565632, + 32934, + 8548, + 147777, + 67905, + 557380, + 33890, + 34208, + 4500, + 90256, + 151561, + 139585, + 43152, + 296224, + 401417, + 332804, + 8773, + 528405, + 165377, + 43392, + 589862, + 99424, + 18506, + 88128, + 92176, + 280705, + 16553, + 264488, + 655752, + 135458, + 100358, + 533510, + 102544, + 263504, + 333888, + 328833, + 149600, + 663681, + 296068, + 336912, + 172161, + 279936, + 332864, + 168002, + 32874, + 35137, + 151558, + 335968, + 590884, + 330256, + 136720, + 4440, + 106514, + 164226, + 655776, + 301312, + 428288, + 659465, + 148498, + 165921, + 294938, + 21522, + 100376, + 665616, + 164161, + 34337, + 6182, + 133776, + 165897, + 526473, + 542984, + 692228, + 43584, + 659984, + 65874, + 287236, + 18950, + 272960, + 333056, + 133506, + 17674, + 559113, + 526597, + 22786, + 590872, + 106760, + 140312, + 397318, + 155654, + 137222, + 100484, + 590085, + 43080, + 594208, + 42056, + 4742, + 264218, + 36885, + 525381, + 533513, + 279064, + 155684, + 99457, + 280594, + 132134, + 548897, + 69796, + 70024, + 18473, + 296969, + 532804, + 81946, + 164993, + 147717, + 558212, + 427024, + 393285, + 102418, + 284676, + 131466, + 70692, + 98385 + ], + "columns": [ + 133638, + 6308, + 301057, + 18962, + 591968, + 283137, + 664580, + 329220, + 327844, + 163924, + 131473, + 413700, + 71776, + 409, + 131428, + 530468, + 74258, + 533636, + 156032, + 86148, + 361024, + 172041, + 657552, + 139872, + 528518, + 397336, + 1682, + 541729, + 6228, + 336448, + 530438, + 264728, + 163986, + 623105, + 25696, + 148513, + 18530, + 430144, + 297476, + 16722, + 524677, + 262760, + 17033, + 280612, + 74264, + 591136, + 279570, + 82018, + 19016, + 530696, + 135444, + 24897, + 590090, + 66117, + 76040, + 41296, + 108548, + 565632, + 32934, + 8548, + 147777, + 67905, + 557380, + 33890, + 34208, + 4500, + 90256, + 151561, + 139585, + 43152, + 296224, + 401417, + 332804, + 8773, + 528405, + 165377, + 43392, + 589862, + 99424, + 18506, + 88128, + 92176, + 280705, + 16553, + 264488, + 655752, + 135458, + 100358, + 533510, + 102544, + 263504, + 333888, + 328833, + 149600, + 663681, + 296068, + 336912, + 172161, + 279936, + 332864, + 168002, + 32874, + 35137, + 151558, + 335968, + 590884, + 330256, + 136720, + 4440, + 106514, + 164226, + 655776, + 301312, + 428288, + 659465, + 148498, + 165921, + 294938, + 21522, + 100376, + 665616, + 164161, + 34337, + 6182, + 133776, + 165897, + 526473, + 542984, + 692228, + 43584, + 659984, + 65874, + 287236, + 18950, + 272960, + 333056, + 133506, + 17674, + 559113, + 526597, + 22786, + 590872, + 106760, + 140312, + 397318, + 155654, + 137222, + 100484, + 590085, + 43080, + 594208, + 42056, + 4742, + 264218, + 36885, + 525381, + 533513, + 279064, + 155684, + 99457, + 280594, + 132134, + 548897, + 69796, + 70024, + 18473, + 296969, + 532804, + 81946, + 164993, + 147717, + 558212, + 427024, + 393285, + 102418, + 284676, + 131466, + 70692, + 98385 + ], + "determinant_mod_prime": 14223, + "candidate_count": 4015, + "candidates_visited": 254, + "feature_basis_size": 179 + }, + { + "p": 10, + "kind": "star", + "target": 1, + "rank_lower": 144, + "rows": [ + 336001, + 529425, + 655401, + 4513, + 529441, + 83973, + 33861, + 393313, + 528905, + 542785, + 305153, + 2217, + 100361, + 5189, + 284673, + 65641, + 262473, + 147841, + 557321, + 299521, + 533569, + 677, + 18693, + 131621, + 65621, + 548929, + 661, + 263209, + 18457, + 10277, + 131425, + 22561, + 70721, + 86021, + 267281, + 33321, + 22017, + 9297, + 303233, + 655889, + 84097, + 566273, + 75009, + 266785, + 9349, + 148001, + 41993, + 24645, + 16549, + 82053, + 264213, + 5193, + 67625, + 164129, + 34321, + 360465, + 4373, + 147985, + 17445, + 295429, + 282657, + 163913, + 6241, + 133253, + 559109, + 6169, + 280705, + 541953, + 4181, + 1561, + 327721, + 346113, + 409729, + 148737, + 82449, + 66601, + 264273, + 41989, + 33865, + 344097, + 155657, + 565377, + 598033, + 140417, + 16473, + 6185, + 548869, + 328721, + 137729, + 327777, + 328197, + 524377, + 71713, + 83009, + 139289, + 657473, + 10881, + 541249, + 541193, + 525601, + 279169, + 526409, + 279617, + 4769, + 67137, + 272393, + 20521, + 696321, + 25121, + 34337, + 557093, + 10265, + 286753, + 34057, + 17489, + 534593, + 39425, + 1557, + 4649, + 70273, + 21513, + 397441, + 592129, + 681, + 163861, + 280585, + 131681, + 1361, + 24897, + 18753, + 99585, + 294953, + 663557, + 18705, + 688161, + 4185, + 331905, + 525449, + 328769, + 156673, + 25665, + 2325, + 20505, + 41093 + ], + "columns": [ + 336001, + 529425, + 655401, + 4513, + 529441, + 83973, + 33861, + 393313, + 528905, + 542785, + 305153, + 2217, + 100361, + 5189, + 284673, + 65641, + 262473, + 147841, + 557321, + 299521, + 533569, + 677, + 18693, + 131621, + 65621, + 548929, + 661, + 263209, + 18457, + 10277, + 131425, + 22561, + 70721, + 86021, + 267281, + 33321, + 22017, + 9297, + 303233, + 655889, + 84097, + 566273, + 75009, + 266785, + 9349, + 148001, + 41993, + 24645, + 16549, + 82053, + 264213, + 5193, + 67625, + 164129, + 34321, + 360465, + 4373, + 147985, + 17445, + 295429, + 282657, + 163913, + 6241, + 133253, + 559109, + 6169, + 280705, + 541953, + 4181, + 1561, + 327721, + 346113, + 409729, + 148737, + 82449, + 66601, + 264273, + 41989, + 33865, + 344097, + 155657, + 565377, + 598033, + 140417, + 16473, + 6185, + 548869, + 328721, + 137729, + 327777, + 328197, + 524377, + 71713, + 83009, + 139289, + 657473, + 10881, + 541249, + 541193, + 525601, + 279169, + 526409, + 279617, + 4769, + 67137, + 272393, + 20521, + 696321, + 25121, + 34337, + 557093, + 10265, + 286753, + 34057, + 17489, + 534593, + 39425, + 1557, + 4649, + 70273, + 21513, + 397441, + 592129, + 681, + 163861, + 280585, + 131681, + 1361, + 24897, + 18753, + 99585, + 294953, + 663557, + 18705, + 688161, + 4185, + 331905, + 525449, + 328769, + 156673, + 25665, + 2325, + 20505, + 41093 + ], + "determinant_mod_prime": 38013, + "candidate_count": 2016, + "candidates_visited": 144, + "feature_basis_size": 144 + }, + { + "p": 11, + "kind": "corrector", + "target": 341, + "rank_lower": 219, + "rows": [ + 2101514, + 1197120, + 1065481, + 149636, + 2719748, + 263444, + 90241, + 600320, + 86040, + 2107650, + 657504, + 2625824, + 282690, + 549377, + 1581152, + 2491396, + 33318, + 2375968, + 393552, + 1056849, + 1050244, + 598082, + 1082000, + 2097478, + 1085473, + 598052, + 1200384, + 2170952, + 17704, + 272642, + 690192, + 1345600, + 673793, + 174336, + 2101640, + 10386, + 2494468, + 165122, + 1311762, + 655681, + 1589377, + 295556, + 86400, + 18596, + 663840, + 331908, + 34065, + 1187876, + 75136, + 529537, + 1351696, + 141696, + 39425, + 132488, + 295568, + 76292, + 533088, + 262250, + 1120260, + 2099466, + 10513, + 131682, + 1081385, + 2392592, + 135266, + 2625632, + 1409025, + 2623632, + 5441, + 2168064, + 2131016, + 1122820, + 278609, + 99592, + 41496, + 140324, + 2236425, + 299296, + 2115728, + 593944, + 1327632, + 1329153, + 1116193, + 156673, + 72208, + 43104, + 2232344, + 279058, + 1212482, + 263252, + 70689, + 2105425, + 8586, + 1212560, + 2132352, + 360454, + 268417, + 2098592, + 2099841, + 2203904, + 1114258, + 561728, + 336001, + 1066080, + 1347648, + 663558, + 360712, + 278801, + 6480, + 5257, + 1380356, + 135434, + 1573382, + 692225, + 1051172, + 2637890, + 295208, + 6278, + 2113640, + 75809, + 1200192, + 1071360, + 524437, + 659522, + 1581344, + 65637, + 2101346, + 2363416, + 2097318, + 71968, + 2163266, + 279585, + 1378305, + 1130625, + 2368064, + 66146, + 1214528, + 268321, + 2622530, + 272897, + 1118466, + 1082434, + 1572890, + 1474561, + 1311136, + 1575428, + 1147144, + 344640, + 1181714, + 2361728, + 2361368, + 1704008, + 139554, + 1067017, + 286816, + 1197057, + 139680, + 1073224, + 266818, + 2261508, + 1193, + 2703616, + 2180352, + 1050758, + 1344064, + 1058882, + 1065496, + 2361632, + 1639425, + 2117896, + 2394128, + 36890, + 1070144, + 1204225, + 33426, + 2228497, + 2703364, + 1214465, + 533528, + 88080, + 2163329, + 1055296, + 2114818, + 526470, + 168449, + 1090052, + 26720, + 148612, + 264584, + 266576, + 71704, + 409609, + 533025, + 131653, + 2631681, + 344328, + 66194, + 164388, + 164448, + 18848, + 591908, + 67096, + 540809, + 43521, + 534564, + 2101769, + 395396, + 34337, + 1049734, + 67610, + 2654280, + 135444, + 278612, + 67860, + 1056789, + 1048920, + 1317, + 2130181, + 131350 + ], + "columns": [ + 2101514, + 1197120, + 1065481, + 149636, + 2719748, + 263444, + 90241, + 600320, + 86040, + 2107650, + 657504, + 2625824, + 282690, + 549377, + 1581152, + 2491396, + 33318, + 2375968, + 393552, + 1056849, + 1050244, + 598082, + 1082000, + 2097478, + 1085473, + 598052, + 1200384, + 2170952, + 17704, + 272642, + 690192, + 1345600, + 673793, + 174336, + 2101640, + 10386, + 2494468, + 165122, + 1311762, + 655681, + 1589377, + 295556, + 86400, + 18596, + 663840, + 331908, + 34065, + 1187876, + 75136, + 529537, + 1351696, + 141696, + 39425, + 132488, + 295568, + 76292, + 533088, + 262250, + 1120260, + 2099466, + 10513, + 131682, + 1081385, + 2392592, + 135266, + 2625632, + 1409025, + 2623632, + 5441, + 2168064, + 2131016, + 1122820, + 278609, + 99592, + 41496, + 140324, + 2236425, + 299296, + 2115728, + 593944, + 1327632, + 1329153, + 1116193, + 156673, + 72208, + 43104, + 2232344, + 279058, + 1212482, + 263252, + 70689, + 2105425, + 8586, + 1212560, + 2132352, + 360454, + 268417, + 2098592, + 2099841, + 2203904, + 1114258, + 561728, + 336001, + 1066080, + 1347648, + 663558, + 360712, + 278801, + 6480, + 5257, + 1380356, + 135434, + 1573382, + 692225, + 1051172, + 2637890, + 295208, + 6278, + 2113640, + 75809, + 1200192, + 1071360, + 524437, + 659522, + 1581344, + 65637, + 2101346, + 2363416, + 2097318, + 71968, + 2163266, + 279585, + 1378305, + 1130625, + 2368064, + 66146, + 1214528, + 268321, + 2622530, + 272897, + 1118466, + 1082434, + 1572890, + 1474561, + 1311136, + 1575428, + 1147144, + 344640, + 1181714, + 2361728, + 2361368, + 1704008, + 139554, + 1067017, + 286816, + 1197057, + 139680, + 1073224, + 266818, + 2261508, + 1193, + 2703616, + 2180352, + 1050758, + 1344064, + 1058882, + 1065496, + 2361632, + 1639425, + 2117896, + 2394128, + 36890, + 1070144, + 1204225, + 33426, + 2228497, + 2703364, + 1214465, + 533528, + 88080, + 2163329, + 1055296, + 2114818, + 526470, + 168449, + 1090052, + 26720, + 148612, + 264584, + 266576, + 71704, + 409609, + 533025, + 131653, + 2631681, + 344328, + 66194, + 164388, + 164448, + 18848, + 591908, + 67096, + 540809, + 43521, + 534564, + 2101769, + 395396, + 34337, + 1049734, + 67610, + 2654280, + 135444, + 278612, + 67860, + 1056789, + 1048920, + 1317, + 2130181, + 131350 + ], + "determinant_mod_prime": 57920, + "candidate_count": 7295, + "candidates_visited": 624, + "feature_basis_size": 219 + }, + { + "p": 11, + "kind": "star", + "target": 1, + "rank_lower": 170, + "rows": [ + 43265, + 2105921, + 2098249, + 8773, + 149521, + 1130501, + 148513, + 131397, + 2261505, + 2228485, + 590913, + 165905, + 393349, + 2106881, + 2232337, + 137281, + 263189, + 6277, + 332033, + 137221, + 426049, + 266757, + 2114065, + 525337, + 1130529, + 163977, + 591937, + 167941, + 1572945, + 270853, + 34177, + 1617, + 5141, + 1311809, + 1589253, + 2138145, + 41477, + 41537, + 344577, + 139537, + 1081729, + 264737, + 1086465, + 1081985, + 1116673, + 1301, + 4201, + 107521, + 296449, + 344081, + 75265, + 657425, + 21513, + 98569, + 2131201, + 525349, + 67089, + 1681, + 90129, + 26629, + 328769, + 280581, + 409617, + 613, + 540741, + 73989, + 10373, + 17449, + 1378305, + 528517, + 17433, + 526361, + 2629889, + 1114153, + 2163717, + 598025, + 1311749, + 1056805, + 1069569, + 16921, + 655681, + 16713, + 2654225, + 1573, + 41249, + 1051265, + 8581, + 591361, + 2627585, + 2449, + 1442817, + 98373, + 403457, + 42113, + 1122337, + 98465, + 1048745, + 279057, + 21121, + 530561, + 67137, + 86081, + 2170897, + 172161, + 135713, + 68113, + 524625, + 1081505, + 2597, + 1050897, + 2425345, + 1049669, + 303121, + 8521, + 17697, + 1065221, + 98385, + 2099585, + 1328129, + 2168833, + 589961, + 2134049, + 267777, + 6529, + 2229761, + 82193, + 1180169, + 299041, + 10513, + 16709, + 278549, + 1633, + 139841, + 271365, + 2424865, + 1114245, + 1573185, + 8741, + 4753, + 2162709, + 6305, + 1638529, + 2115649, + 299025, + 74817, + 295073, + 2629, + 1122313, + 2623505, + 264329, + 655457, + 594049, + 2228357, + 2113573, + 2130949, + 1118721, + 1605, + 1609, + 2625541, + 2658305, + 8529, + 532501, + 270357, + 82241, + 18501, + 2245633, + 2105481, + 1318917, + 2102305, + 534785 + ], + "columns": [ + 43265, + 2105921, + 2098249, + 8773, + 149521, + 1130501, + 148513, + 131397, + 2261505, + 2228485, + 590913, + 165905, + 393349, + 2106881, + 2232337, + 137281, + 263189, + 6277, + 332033, + 137221, + 426049, + 266757, + 2114065, + 525337, + 1130529, + 163977, + 591937, + 167941, + 1572945, + 270853, + 34177, + 1617, + 5141, + 1311809, + 1589253, + 2138145, + 41477, + 41537, + 344577, + 139537, + 1081729, + 264737, + 1086465, + 1081985, + 1116673, + 1301, + 4201, + 107521, + 296449, + 344081, + 75265, + 657425, + 21513, + 98569, + 2131201, + 525349, + 67089, + 1681, + 90129, + 26629, + 328769, + 280581, + 409617, + 613, + 540741, + 73989, + 10373, + 17449, + 1378305, + 528517, + 17433, + 526361, + 2629889, + 1114153, + 2163717, + 598025, + 1311749, + 1056805, + 1069569, + 16921, + 655681, + 16713, + 2654225, + 1573, + 41249, + 1051265, + 8581, + 591361, + 2627585, + 2449, + 1442817, + 98373, + 403457, + 42113, + 1122337, + 98465, + 1048745, + 279057, + 21121, + 530561, + 67137, + 86081, + 2170897, + 172161, + 135713, + 68113, + 524625, + 1081505, + 2597, + 1050897, + 2425345, + 1049669, + 303121, + 8521, + 17697, + 1065221, + 98385, + 2099585, + 1328129, + 2168833, + 589961, + 2134049, + 267777, + 6529, + 2229761, + 82193, + 1180169, + 299041, + 10513, + 16709, + 278549, + 1633, + 139841, + 271365, + 2424865, + 1114245, + 1573185, + 8741, + 4753, + 2162709, + 6305, + 1638529, + 2115649, + 299025, + 74817, + 295073, + 2629, + 1122313, + 2623505, + 264329, + 655457, + 594049, + 2228357, + 2113573, + 2130949, + 1118721, + 1605, + 1609, + 2625541, + 2658305, + 8529, + 532501, + 270357, + 82241, + 18501, + 2245633, + 2105481, + 1318917, + 2102305, + 534785 + ], + "determinant_mod_prime": 40517, + "candidate_count": 3360, + "candidates_visited": 180, + "feature_basis_size": 180 + }, + { + "p": 12, + "kind": "corrector", + "target": 341, + "rank_lower": 263, + "rows": [ + 6307936, + 266321, + 266788, + 4265024, + 2102305, + 37912, + 4362256, + 1442176, + 1057858, + 34128, + 2113574, + 151585, + 10520580, + 4260358, + 1056929, + 8454185, + 168976, + 541960, + 395648, + 68162, + 9505024, + 1183777, + 8520833, + 267288, + 10526724, + 266561, + 2165312, + 533792, + 1050945, + 565272, + 671750, + 2179096, + 132417, + 540945, + 279576, + 9703488, + 4195349, + 2261508, + 5341185, + 4194470, + 8413316, + 25729, + 4720898, + 2392130, + 8978450, + 4489240, + 9076737, + 25984, + 10487826, + 42008, + 2492420, + 8652836, + 548960, + 8781896, + 4723216, + 672257, + 9437318, + 10618944, + 4589632, + 1147908, + 10813441, + 9474052, + 673024, + 2180160, + 2105442, + 133393, + 4194585, + 21513, + 1605, + 131425, + 344070, + 6312000, + 1639488, + 606280, + 1090112, + 4456474, + 1377, + 10649616, + 10748048, + 10503184, + 1380, + 2233345, + 526872, + 131221, + 4490241, + 8394244, + 1409088, + 4522020, + 659840, + 9699361, + 10503169, + 9457665, + 70024, + 2166820, + 4268098, + 608272, + 10486416, + 34065, + 599056, + 2134529, + 2396416, + 5374468, + 533600, + 8659472, + 4329544, + 8491012, + 71704, + 4524096, + 4784392, + 8485, + 2392577, + 4554816, + 70180, + 6291525, + 2202, + 10487904, + 33094, + 2099784, + 4259861, + 66069, + 2132352, + 590342, + 17569, + 4228480, + 1181792, + 6554128, + 9441424, + 2490434, + 2662416, + 10491920, + 2163206, + 4325528, + 4329736, + 9568289, + 2164228, + 9441316, + 75872, + 100448, + 10748288, + 360472, + 2654241, + 1376514, + 4278288, + 4422, + 141378, + 8393986, + 546832, + 139302, + 10748432, + 1052948, + 8395016, + 2623584, + 1316096, + 9703428, + 5506049, + 8915520, + 8388937, + 75908, + 8425604, + 592004, + 1312128, + 8685572, + 5254, + 135752, + 541217, + 4754, + 173312, + 8918272, + 10506496, + 533513, + 8415248, + 5277697, + 5537796, + 9046017, + 4268416, + 4211329, + 67201, + 284928, + 1638532, + 2102404, + 139872, + 296320, + 2101400, + 559140, + 331794, + 8520264, + 20644, + 6410, + 5898256, + 4276740, + 1458192, + 149008, + 20741, + 2360833, + 10616868, + 2637890, + 327749, + 2101544, + 133410, + 8407058, + 4457736, + 1085956, + 1575425, + 4198978, + 24710, + 4294912, + 41346, + 1051202, + 2363536, + 655681, + 4719113, + 9969728, + 2228250, + 4328000, + 1073728, + 4204562, + 4261897, + 2691073, + 8913042, + 393512, + 8388952, + 2364432, + 4264964, + 6422624, + 8913186, + 4735489, + 6291608, + 4335617, + 34068, + 1577488, + 2166880, + 2097705, + 4196618, + 8423556, + 1605704, + 82216, + 2163009, + 2228497, + 8390168, + 2752770, + 8778, + 34328, + 5771520, + 10551392, + 4210825, + 656004, + 332816, + 6422912, + 2134592, + 4203544, + 18049, + 1118241, + 8519832, + 1392896, + 305168, + 287808, + 4751492, + 4726802, + 267270, + 6291477, + 6324512, + 6560, + 524374 + ], + "columns": [ + 6307936, + 266321, + 266788, + 4265024, + 2102305, + 37912, + 4362256, + 1442176, + 1057858, + 34128, + 2113574, + 151585, + 10520580, + 4260358, + 1056929, + 8454185, + 168976, + 541960, + 395648, + 68162, + 9505024, + 1183777, + 8520833, + 267288, + 10526724, + 266561, + 2165312, + 533792, + 1050945, + 565272, + 671750, + 2179096, + 132417, + 540945, + 279576, + 9703488, + 4195349, + 2261508, + 5341185, + 4194470, + 8413316, + 25729, + 4720898, + 2392130, + 8978450, + 4489240, + 9076737, + 25984, + 10487826, + 42008, + 2492420, + 8652836, + 548960, + 8781896, + 4723216, + 672257, + 9437318, + 10618944, + 4589632, + 1147908, + 10813441, + 9474052, + 673024, + 2180160, + 2105442, + 133393, + 4194585, + 21513, + 1605, + 131425, + 344070, + 6312000, + 1639488, + 606280, + 1090112, + 4456474, + 1377, + 10649616, + 10748048, + 10503184, + 1380, + 2233345, + 526872, + 131221, + 4490241, + 8394244, + 1409088, + 4522020, + 659840, + 9699361, + 10503169, + 9457665, + 70024, + 2166820, + 4268098, + 608272, + 10486416, + 34065, + 599056, + 2134529, + 2396416, + 5374468, + 533600, + 8659472, + 4329544, + 8491012, + 71704, + 4524096, + 4784392, + 8485, + 2392577, + 4554816, + 70180, + 6291525, + 2202, + 10487904, + 33094, + 2099784, + 4259861, + 66069, + 2132352, + 590342, + 17569, + 4228480, + 1181792, + 6554128, + 9441424, + 2490434, + 2662416, + 10491920, + 2163206, + 4325528, + 4329736, + 9568289, + 2164228, + 9441316, + 75872, + 100448, + 10748288, + 360472, + 2654241, + 1376514, + 4278288, + 4422, + 141378, + 8393986, + 546832, + 139302, + 10748432, + 1052948, + 8395016, + 2623584, + 1316096, + 9703428, + 5506049, + 8915520, + 8388937, + 75908, + 8425604, + 592004, + 1312128, + 8685572, + 5254, + 135752, + 541217, + 4754, + 173312, + 8918272, + 10506496, + 533513, + 8415248, + 5277697, + 5537796, + 9046017, + 4268416, + 4211329, + 67201, + 284928, + 1638532, + 2102404, + 139872, + 296320, + 2101400, + 559140, + 331794, + 8520264, + 20644, + 6410, + 5898256, + 4276740, + 1458192, + 149008, + 20741, + 2360833, + 10616868, + 2637890, + 327749, + 2101544, + 133410, + 8407058, + 4457736, + 1085956, + 1575425, + 4198978, + 24710, + 4294912, + 41346, + 1051202, + 2363536, + 655681, + 4719113, + 9969728, + 2228250, + 4328000, + 1073728, + 4204562, + 4261897, + 2691073, + 8913042, + 393512, + 8388952, + 2364432, + 4264964, + 6422624, + 8913186, + 4735489, + 6291608, + 4335617, + 34068, + 1577488, + 2166880, + 2097705, + 4196618, + 8423556, + 1605704, + 82216, + 2163009, + 2228497, + 8390168, + 2752770, + 8778, + 34328, + 5771520, + 10551392, + 4210825, + 656004, + 332816, + 6422912, + 2134592, + 4203544, + 18049, + 1118241, + 8519832, + 1392896, + 305168, + 287808, + 4751492, + 4726802, + 267270, + 6291477, + 6324512, + 6560, + 524374 + ], + "determinant_mod_prime": 31288, + "candidate_count": 12335, + "candidates_visited": 278, + "feature_basis_size": 263 + }, + { + "p": 12, + "kind": "star", + "target": 1, + "rank_lower": 210, + "rows": [ + 8655361, + 2360449, + 4718661, + 5275713, + 2597, + 8389281, + 5244033, + 8521217, + 6307969, + 1114185, + 263433, + 8684545, + 1114385, + 2375685, + 4263941, + 1067137, + 2097541, + 657425, + 139285, + 8391185, + 82977, + 9044001, + 140353, + 1052769, + 41537, + 1066017, + 6291529, + 33169, + 5276161, + 9453601, + 4196737, + 140293, + 99457, + 395777, + 524641, + 1179913, + 4259937, + 524617, + 9584641, + 8716417, + 25729, + 1458177, + 8458369, + 172037, + 4199429, + 167945, + 8454305, + 558593, + 137233, + 262421, + 75009, + 8421537, + 8463361, + 2261249, + 4326433, + 2098245, + 5242949, + 8460289, + 1573001, + 136705, + 9489, + 4524033, + 131353, + 2163777, + 526357, + 1089545, + 10502153, + 589897, + 529025, + 9568273, + 66073, + 659461, + 132165, + 8454405, + 558337, + 8650913, + 4276289, + 6356997, + 4360193, + 5308433, + 1573153, + 10487817, + 4196641, + 8393737, + 16537, + 34309, + 5243025, + 264337, + 139361, + 5247489, + 10485829, + 164481, + 4270081, + 524961, + 1048665, + 4335617, + 264261, + 33321, + 4489345, + 18961, + 1319937, + 2131977, + 270977, + 266265, + 5259273, + 8455425, + 8913041, + 18565, + 2581, + 4459009, + 262233, + 671777, + 8393225, + 98329, + 148513, + 8520001, + 4458505, + 133641, + 557189, + 8422529, + 1066049, + 4194885, + 1187873, + 4331521, + 21121, + 4260869, + 8388933, + 33873, + 541249, + 533009, + 10486801, + 656513, + 1058833, + 2097733, + 598529, + 2099281, + 4786177, + 2172929, + 5832705, + 10485905, + 8913029, + 8745, + 1114373, + 4264065, + 8841, + 1312833, + 8392729, + 2113697, + 66821, + 4325761, + 5373985, + 659713, + 90177, + 11042817, + 33417, + 8398857, + 5505153, + 2687489, + 141329, + 9502729, + 2228305, + 2179105, + 4265985, + 4235273, + 8357, + 393377, + 2130437, + 2130241, + 8389189, + 1409025, + 8406081, + 1376513, + 565281, + 9445393, + 66721, + 1122337, + 280581, + 135441, + 4720645, + 163977, + 2114569, + 163881, + 9060353, + 41989, + 303169, + 33861, + 331781, + 4784257, + 4522241, + 5308673, + 264229, + 172041, + 17481, + 4341825, + 4227649, + 11010057, + 131473, + 83457, + 426113, + 2785281, + 5505029, + 1050769, + 8945669, + 2359433, + 270433, + 5252097, + 1180289, + 332801, + 37025, + 8421401 + ], + "columns": [ + 8655361, + 2360449, + 4718661, + 5275713, + 2597, + 8389281, + 5244033, + 8521217, + 6307969, + 1114185, + 263433, + 8684545, + 1114385, + 2375685, + 4263941, + 1067137, + 2097541, + 657425, + 139285, + 8391185, + 82977, + 9044001, + 140353, + 1052769, + 41537, + 1066017, + 6291529, + 33169, + 5276161, + 9453601, + 4196737, + 140293, + 99457, + 395777, + 524641, + 1179913, + 4259937, + 524617, + 9584641, + 8716417, + 25729, + 1458177, + 8458369, + 172037, + 4199429, + 167945, + 8454305, + 558593, + 137233, + 262421, + 75009, + 8421537, + 8463361, + 2261249, + 4326433, + 2098245, + 5242949, + 8460289, + 1573001, + 136705, + 9489, + 4524033, + 131353, + 2163777, + 526357, + 1089545, + 10502153, + 589897, + 529025, + 9568273, + 66073, + 659461, + 132165, + 8454405, + 558337, + 8650913, + 4276289, + 6356997, + 4360193, + 5308433, + 1573153, + 10487817, + 4196641, + 8393737, + 16537, + 34309, + 5243025, + 264337, + 139361, + 5247489, + 10485829, + 164481, + 4270081, + 524961, + 1048665, + 4335617, + 264261, + 33321, + 4489345, + 18961, + 1319937, + 2131977, + 270977, + 266265, + 5259273, + 8455425, + 8913041, + 18565, + 2581, + 4459009, + 262233, + 671777, + 8393225, + 98329, + 148513, + 8520001, + 4458505, + 133641, + 557189, + 8422529, + 1066049, + 4194885, + 1187873, + 4331521, + 21121, + 4260869, + 8388933, + 33873, + 541249, + 533009, + 10486801, + 656513, + 1058833, + 2097733, + 598529, + 2099281, + 4786177, + 2172929, + 5832705, + 10485905, + 8913029, + 8745, + 1114373, + 4264065, + 8841, + 1312833, + 8392729, + 2113697, + 66821, + 4325761, + 5373985, + 659713, + 90177, + 11042817, + 33417, + 8398857, + 5505153, + 2687489, + 141329, + 9502729, + 2228305, + 2179105, + 4265985, + 4235273, + 8357, + 393377, + 2130437, + 2130241, + 8389189, + 1409025, + 8406081, + 1376513, + 565281, + 9445393, + 66721, + 1122337, + 280581, + 135441, + 4720645, + 163977, + 2114569, + 163881, + 9060353, + 41989, + 303169, + 33861, + 331781, + 4784257, + 4522241, + 5308673, + 264229, + 172041, + 17481, + 4341825, + 4227649, + 11010057, + 131473, + 83457, + 426113, + 2785281, + 5505029, + 1050769, + 8945669, + 2359433, + 270433, + 5252097, + 1180289, + 332801, + 37025, + 8421401 + ], + "determinant_mod_prime": 37917, + "candidate_count": 5280, + "candidates_visited": 299, + "feature_basis_size": 220 + }, + { + "p": 13, + "kind": "corrector", + "target": 341, + "rank_lower": 311, + "rows": [ + 2097253, + 17858578, + 35717144, + 5260289, + 18874952, + 8914304, + 2232464, + 8978456, + 74276, + 1204240, + 4260004, + 696321, + 8421954, + 33595680, + 133441, + 33822724, + 86082, + 16842833, + 8528160, + 1577056, + 2113812, + 2170889, + 17039696, + 35717249, + 102688, + 8929304, + 17170438, + 37818369, + 5245441, + 106514, + 8405316, + 33558852, + 26218512, + 4464928, + 155777, + 27296000, + 41975940, + 2130980, + 25235460, + 1315392, + 20981764, + 8425508, + 2639936, + 1574984, + 139290, + 17041936, + 524961, + 33562945, + 33049, + 8917505, + 34083074, + 8782852, + 16785489, + 1081508, + 17826208, + 33558609, + 16785446, + 65625, + 8423457, + 34627588, + 19140672, + 5245312, + 2236422, + 303140, + 8913938, + 2375824, + 4456714, + 17367046, + 1606720, + 8389796, + 34086978, + 2269188, + 33624328, + 8405090, + 5261313, + 2103332, + 21037188, + 2346, + 2621524, + 8458384, + 17850369, + 44041217, + 4227593, + 5416, + 1085464, + 24897, + 33570914, + 327841, + 27263000, + 2490500, + 6389776, + 33621028, + 18942016, + 2626561, + 44040336, + 98441, + 4196993, + 295568, + 590854, + 42074148, + 10649664, + 8915520, + 10338, + 35202, + 21495841, + 33689618, + 6292612, + 2429184, + 6326273, + 21496848, + 35131396, + 25301056, + 4460928, + 35656196, + 132432, + 18878752, + 1132548, + 74788, + 38799424, + 8921112, + 42116, + 1052996, + 4457616, + 2101634, + 1575008, + 11010624, + 66200, + 593944, + 591968, + 16859172, + 34152512, + 27263489, + 524586, + 8388697, + 16910402, + 84064, + 22020192, + 35668544, + 43008001, + 4227362, + 2360416, + 18891136, + 18939940, + 18907202, + 1575176, + 528905, + 37749254, + 8653058, + 5406724, + 10486152, + 33702146, + 41944193, + 1458180, + 2622977, + 2163074, + 42991904, + 1345600, + 4325397, + 4360256, + 264273, + 524934, + 33559136, + 4727297, + 9584641, + 135441, + 1314882, + 33560864, + 541193, + 37759040, + 1441888, + 4718916, + 10486026, + 22021184, + 42090512, + 38801664, + 20972161, + 8411200, + 287296, + 4456840, + 4198561, + 6328321, + 2694, + 2105880, + 8413193, + 44042244, + 4792324, + 4457856, + 8427524, + 2752578, + 663624, + 1312912, + 34742276, + 630848, + 33626116, + 34603049, + 4326688, + 8914178, + 33624352, + 4595968, + 35692800, + 598082, + 9701632, + 559176, + 35783744, + 33702976, + 70689, + 33816617, + 35659905, + 5505408, + 2114593, + 4735264, + 1196290, + 2639876, + 33625152, + 33853444, + 394498, + 2167312, + 266309, + 18104384, + 524374, + 16777610, + 1573912, + 65865, + 33694784, + 8487176, + 16908386, + 16785704, + 5441, + 33685656, + 23077120, + 4202522, + 33882148, + 9242, + 2115650, + 21496336, + 9965584, + 33094, + 16793876, + 5247120, + 43008064, + 328324, + 263189, + 35652120, + 82066, + 6293528, + 42008600, + 1083656, + 4325450, + 17318401, + 264261, + 4200577, + 17956, + 33898512, + 33580036, + 18940192, + 4218976, + 33693825, + 4214808, + 9076752, + 8520198, + 10404, + 4212754, + 395360, + 26738752, + 5245000, + 4743232, + 1312786, + 33587334, + 33690113, + 16846881, + 11010432, + 34112001, + 83457, + 534546, + 33621088, + 1089545, + 1048914, + 4276296, + 33830, + 38027328, + 34111506, + 17850432, + 1184260, + 4211272, + 39428, + 403472, + 655494, + 17170960, + 37753096, + 5505288, + 17055753, + 35128336, + 8407112, + 9441298, + 8913444, + 10553360, + 8913552, + 8405126, + 2124032, + 8388709, + 8658977, + 34097408, + 8929316, + 35660816, + 2232452, + 35670272, + 2101892, + 25297472, + 655621, + 33554821, + 131665 + ], + "columns": [ + 2097253, + 17858578, + 35717144, + 5260289, + 18874952, + 8914304, + 2232464, + 8978456, + 74276, + 1204240, + 4260004, + 696321, + 8421954, + 33595680, + 133441, + 33822724, + 86082, + 16842833, + 8528160, + 1577056, + 2113812, + 2170889, + 17039696, + 35717249, + 102688, + 8929304, + 17170438, + 37818369, + 5245441, + 106514, + 8405316, + 33558852, + 26218512, + 4464928, + 155777, + 27296000, + 41975940, + 2130980, + 25235460, + 1315392, + 20981764, + 8425508, + 2639936, + 1574984, + 139290, + 17041936, + 524961, + 33562945, + 33049, + 8917505, + 34083074, + 8782852, + 16785489, + 1081508, + 17826208, + 33558609, + 16785446, + 65625, + 8423457, + 34627588, + 19140672, + 5245312, + 2236422, + 303140, + 8913938, + 2375824, + 4456714, + 17367046, + 1606720, + 8389796, + 34086978, + 2269188, + 33624328, + 8405090, + 5261313, + 2103332, + 21037188, + 2346, + 2621524, + 8458384, + 17850369, + 44041217, + 4227593, + 5416, + 1085464, + 24897, + 33570914, + 327841, + 27263000, + 2490500, + 6389776, + 33621028, + 18942016, + 2626561, + 44040336, + 98441, + 4196993, + 295568, + 590854, + 42074148, + 10649664, + 8915520, + 10338, + 35202, + 21495841, + 33689618, + 6292612, + 2429184, + 6326273, + 21496848, + 35131396, + 25301056, + 4460928, + 35656196, + 132432, + 18878752, + 1132548, + 74788, + 38799424, + 8921112, + 42116, + 1052996, + 4457616, + 2101634, + 1575008, + 11010624, + 66200, + 593944, + 591968, + 16859172, + 34152512, + 27263489, + 524586, + 8388697, + 16910402, + 84064, + 22020192, + 35668544, + 43008001, + 4227362, + 2360416, + 18891136, + 18939940, + 18907202, + 1575176, + 528905, + 37749254, + 8653058, + 5406724, + 10486152, + 33702146, + 41944193, + 1458180, + 2622977, + 2163074, + 42991904, + 1345600, + 4325397, + 4360256, + 264273, + 524934, + 33559136, + 4727297, + 9584641, + 135441, + 1314882, + 33560864, + 541193, + 37759040, + 1441888, + 4718916, + 10486026, + 22021184, + 42090512, + 38801664, + 20972161, + 8411200, + 287296, + 4456840, + 4198561, + 6328321, + 2694, + 2105880, + 8413193, + 44042244, + 4792324, + 4457856, + 8427524, + 2752578, + 663624, + 1312912, + 34742276, + 630848, + 33626116, + 34603049, + 4326688, + 8914178, + 33624352, + 4595968, + 35692800, + 598082, + 9701632, + 559176, + 35783744, + 33702976, + 70689, + 33816617, + 35659905, + 5505408, + 2114593, + 4735264, + 1196290, + 2639876, + 33625152, + 33853444, + 394498, + 2167312, + 266309, + 18104384, + 524374, + 16777610, + 1573912, + 65865, + 33694784, + 8487176, + 16908386, + 16785704, + 5441, + 33685656, + 23077120, + 4202522, + 33882148, + 9242, + 2115650, + 21496336, + 9965584, + 33094, + 16793876, + 5247120, + 43008064, + 328324, + 263189, + 35652120, + 82066, + 6293528, + 42008600, + 1083656, + 4325450, + 17318401, + 264261, + 4200577, + 17956, + 33898512, + 33580036, + 18940192, + 4218976, + 33693825, + 4214808, + 9076752, + 8520198, + 10404, + 4212754, + 395360, + 26738752, + 5245000, + 4743232, + 1312786, + 33587334, + 33690113, + 16846881, + 11010432, + 34112001, + 83457, + 534546, + 33621088, + 1089545, + 1048914, + 4276296, + 33830, + 38027328, + 34111506, + 17850432, + 1184260, + 4211272, + 39428, + 403472, + 655494, + 17170960, + 37753096, + 5505288, + 17055753, + 35128336, + 8407112, + 9441298, + 8913444, + 10553360, + 8913552, + 8405126, + 2124032, + 8388709, + 8658977, + 34097408, + 8929316, + 35660816, + 2232452, + 35670272, + 2101892, + 25297472, + 655621, + 33554821, + 131665 + ], + "determinant_mod_prime": 2988, + "candidate_count": 19695, + "candidates_visited": 879, + "feature_basis_size": 311 + } + ] +} diff --git a/research/five-port-quadratic-decoder/discover.py b/research/five-port-quadratic-decoder/discover.py new file mode 100644 index 0000000000..4c15844247 --- /dev/null +++ b/research/five-port-quadratic-decoder/discover.py @@ -0,0 +1,138 @@ +#!/usr/bin/env python3 +"""Construct finite rank witnesses; not trusted by verify.py. + +Copyright 2026 Ross Richardson. Apache-2.0. +Prepared with substantial OpenAI Codex assistance. +""" +from itertools import combinations, product +from pathlib import Path +import json +import random + +HERE = Path(__file__).resolve().parent +PRIME = 65521 +SEED = 40 + + +def ports(p): + return [sum(1 << (2 * i + b) for i, b in zip(indices, bits)) + for indices in combinations(range(p), 5) + for bits in product(range(2), repeat=5)] + + +def gram(a, b): + j = (a & b).bit_count() + return 2 * (j - 1) * (j - 3) + + +def feature_basis(candidates, p, target_size): + coordinates = [(i, j) for i in range(2 * p) for j in range(i + 1, 2 * p) + if i // 2 != j // 2] + basis = {} + chosen = [] + visited = 0 + for port in candidates: + visited += 1 + row = [1] + [(port >> i) & 1 for i in range(2 * p)] + row += [int(bool(port & (1 << i)) and bool(port & (1 << j))) + for i, j in coordinates] + for col in sorted(basis): + if row[col]: + factor = row[col] + other = basis[col] + row[col:] = [(x - factor * y) % PRIME + for x, y in zip(row[col:], other[col:])] + pivot = next((i for i, x in enumerate(row) if x), None) + if pivot is None: + continue + inv = pow(row[pivot], -1, PRIME) + basis[pivot] = [(x * inv) % PRIME for x in row] + chosen.append(port) + if len(chosen) == target_size: + return chosen, visited + raise RuntimeError((p, target_size, len(chosen))) + + +def minor(matrix): + rows = [row[:] for row in matrix] + original = list(range(len(rows))) + row_ids, col_ids = [], [] + rank = 0 + for col in range(len(rows[0])): + pivot = next((i for i in range(rank, len(rows)) if rows[i][col] % PRIME), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + original[rank], original[pivot] = original[pivot], original[rank] + row_ids.append(original[rank]) + col_ids.append(col) + inv = pow(rows[rank][col], -1, PRIME) + row = [(x * inv) % PRIME for x in rows[rank]] + rows[rank] = row + for i in range(rank + 1, len(rows)): + factor = rows[i][col] % PRIME + if factor: + rows[i][col:] = [(x - factor * y) % PRIME + for x, y in zip(rows[i][col:], row[col:])] + rank += 1 + return row_ids, col_ids + + +def determinant(matrix): + rows = [row[:] for row in matrix] + det = 1 + for col in range(len(rows)): + pivot = next((i for i in range(col, len(rows)) if rows[i][col] % PRIME), None) + if pivot is None: + return 0 + if pivot != col: + rows[col], rows[pivot] = rows[pivot], rows[col] + det = -det + value = rows[col][col] % PRIME + det = det * value % PRIME + inv = pow(value, -1, PRIME) + for i in range(col + 1, len(rows)): + factor = rows[i][col] * inv % PRIME + if factor: + rows[i][col:] = [(x - factor * y) % PRIME + for x, y in zip(rows[i][col:], rows[col][col:])] + return det % PRIME + + +def main(): + witnesses = [] + target = sum(1 << (2 * i) for i in range(5)) + for p in range(5, 14): + domain = ports(p) + for kind in ('corrector', 'star'): + if p == 13 and kind == 'star': + continue + if kind == 'corrector': + candidates = [x for x in domain if (x & target).bit_count() in (1, 3)] + size = {5: 15, 6: 50}.get(p, 2 * p * (p - 1) - 1) + else: + candidates = [x for x in domain if x & 1] + size = {5: 11, 6: 35}.get(p, 2 * (p - 1) * (p - 2)) + random.Random(SEED + 100 * p + (kind == 'star')).shuffle(candidates) + basis, visited = feature_basis(candidates, p, size) + rows, cols = minor([[gram(a, b) for b in basis] for a in basis]) + left, right = [basis[i] for i in rows], [basis[i] for i in cols] + det = determinant([[gram(a, b) for b in right] for a in left]) + if not det: + raise RuntimeError('singular selected minor') + witnesses.append(dict(p=p, kind=kind, target=target if kind == 'corrector' else 1, + rank_lower=len(rows), rows=left, columns=right, + determinant_mod_prime=det, + candidate_count=len(candidates), candidates_visited=visited, + feature_basis_size=len(basis))) + print(p, kind, 'rank >=', len(rows), 'visited', visited, '/', len(candidates), flush=True) + output = dict(schema='five-port-quadratic-rank-witnesses-v1', seed=SEED, prime=PRIME, + kernel_coefficients=[6, -8, 2], witnesses=witnesses) + path = HERE / 'WITNESSES.json' + if path.exists(): + raise SystemExit('refusing to overwrite WITNESSES.json') + path.write_text(json.dumps(output, indent=2) + '\n') + + +if __name__ == '__main__': + main() diff --git a/research/five-port-quadratic-decoder/evidence/checks.json b/research/five-port-quadratic-decoder/evidence/checks.json new file mode 100644 index 0000000000..935104ed61 --- /dev/null +++ b/research/five-port-quadratic-decoder/evidence/checks.json @@ -0,0 +1,50 @@ +{ + "verified_utc": "2026-10-13T14:30:05.595342+00:00", + "checks": [ + { + "command": [ + "python3.12", + "-I", + "-O", + "-B", + "research/five-port-quadratic-decoder/verify.py" + ], + "exit_code": 0, + "elapsed_seconds": 3.988, + "output": "evidence/primary-python312.txt" + }, + { + "command": [ + "python3.14", + "-I", + "-O", + "-B", + "research/five-port-quadratic-decoder/independent.py" + ], + "exit_code": 0, + "elapsed_seconds": 6.575, + "output": "evidence/second-python314.txt" + }, + { + "command": [ + "python3.12", + "-I", + "-O", + "-B", + "research/five-port-quadratic-decoder/test_package.py" + ], + "exit_code": 0, + "elapsed_seconds": 0.415, + "output": "evidence/package-tests.txt" + }, + { + "command": [ + "make", + "selected-record-check" + ], + "exit_code": 0, + "elapsed_seconds": 0.33, + "output": "evidence/selected-record.txt" + } + ] +} diff --git a/research/five-port-quadratic-decoder/evidence/clean-export.json b/research/five-port-quadratic-decoder/evidence/clean-export.json new file mode 100644 index 0000000000..c5aa1eb88a --- /dev/null +++ b/research/five-port-quadratic-decoder/evidence/clean-export.json @@ -0,0 +1,27 @@ +{ + "utc": "2026-10-13T14:34:33.700200+00:00", + "staged_tree": "b9e0cd6fd0792057c8e10f189b0a3a86f1364bba", + "files_exported": 23, + "source": "canonical staged Git blobs", + "relocated_path_contains_spaces": true, + "checks": [ + { + "check": "verify.py", + "exit_code": 0, + "elapsed_seconds": 2.249, + "receipt_byte_identical": true + }, + { + "check": "independent.py", + "exit_code": 0, + "elapsed_seconds": 4.072, + "receipt_byte_identical": true + }, + { + "check": "existing output preservation", + "exit_code": 1, + "expected_rejection": true, + "bytes_preserved": true + } + ] +} diff --git a/research/five-port-quadratic-decoder/evidence/export-independent.py.txt b/research/five-port-quadratic-decoder/evidence/export-independent.py.txt new file mode 100644 index 0000000000..be497c7e94 --- /dev/null +++ b/research/five-port-quadratic-decoder/evidence/export-independent.py.txt @@ -0,0 +1 @@ +PASS_FIVE_PORT_SECOND_IMPLEMENTATION minors=17 prime=65519 exact_integer_determinants=2 ceiling=125/76433 no_new_kappa diff --git a/research/five-port-quadratic-decoder/evidence/export-verify.py.txt b/research/five-port-quadratic-decoder/evidence/export-verify.py.txt new file mode 100644 index 0000000000..71d26dcf0c --- /dev/null +++ b/research/five-port-quadratic-decoder/evidence/export-verify.py.txt @@ -0,0 +1 @@ +PASS_FIVE_PORT_QUADRATIC_DECODER witnesses=17 ceiling=125/76433 tail=250/170739 controls=9 no_new_kappa diff --git a/research/five-port-quadratic-decoder/evidence/package-tests.txt b/research/five-port-quadratic-decoder/evidence/package-tests.txt new file mode 100644 index 0000000000..e6c58bc292 --- /dev/null +++ b/research/five-port-quadratic-decoder/evidence/package-tests.txt @@ -0,0 +1,11 @@ +test_all_named_controls (__main__.ProofRelevantControls.test_all_named_controls) ... ok +test_changed_source_rejected (__main__.ProofRelevantControls.test_changed_source_rejected) ... ok +test_distinct_valid_labels_can_make_a_singular_minor (__main__.ProofRelevantControls.test_distinct_valid_labels_can_make_a_singular_minor) ... ok +test_missing_obligation_rejected (__main__.ProofRelevantControls.test_missing_obligation_rejected) ... ok +test_two_eliminations_against_definition (__main__.ProofRelevantControls.test_two_eliminations_against_definition) ... ok +test_valid_scalar_geometry_failure_is_visible (__main__.ProofRelevantControls.test_valid_scalar_geometry_failure_is_visible) ... ok + +---------------------------------------------------------------------- +Ran 6 tests in 0.020s + +OK diff --git a/research/five-port-quadratic-decoder/evidence/primary-python312.txt b/research/five-port-quadratic-decoder/evidence/primary-python312.txt new file mode 100644 index 0000000000..71d26dcf0c --- /dev/null +++ b/research/five-port-quadratic-decoder/evidence/primary-python312.txt @@ -0,0 +1 @@ +PASS_FIVE_PORT_QUADRATIC_DECODER witnesses=17 ceiling=125/76433 tail=250/170739 controls=9 no_new_kappa diff --git a/research/five-port-quadratic-decoder/evidence/second-python314.txt b/research/five-port-quadratic-decoder/evidence/second-python314.txt new file mode 100644 index 0000000000..be497c7e94 --- /dev/null +++ b/research/five-port-quadratic-decoder/evidence/second-python314.txt @@ -0,0 +1 @@ +PASS_FIVE_PORT_SECOND_IMPLEMENTATION minors=17 prime=65519 exact_integer_determinants=2 ceiling=125/76433 no_new_kappa diff --git a/research/five-port-quadratic-decoder/evidence/selected-record.txt b/research/five-port-quadratic-decoder/evidence/selected-record.txt new file mode 100644 index 0000000000..34654ca6d1 --- /dev/null +++ b/research/five-port-quadratic-decoder/evidence/selected-record.txt @@ -0,0 +1,2 @@ +python3 -B scripts/verify_selected_result.py +PASS selected record, exact kappa, original source inventory and proof supplement: 1661957774647029/1000000000000000000 diff --git a/research/five-port-quadratic-decoder/independent.py b/research/five-port-quadratic-decoder/independent.py new file mode 100644 index 0000000000..ed3dfcdbe1 --- /dev/null +++ b/research/five-port-quadratic-decoder/independent.py @@ -0,0 +1,146 @@ +#!/usr/bin/env python3 +"""Separately implemented check: set features and fraction-free elimination. + +Imports neither the primary verifier nor discovery code. Uses a second prime +and recomputes the pricing from the literal minor dimensions. +Copyright 2026 Ross Richardson. Apache-2.0. Substantial OpenAI Codex assistance. +This is a second implementation by the same AI-assisted contributor, not +independent human peer review. +""" +from fractions import Fraction +from itertools import combinations, product +from math import comb, isqrt +from pathlib import Path +import argparse +import hashlib +import json + +ROOT = Path(__file__).resolve().parent +MODULUS = 65519 + + +def check(condition, text): + if not condition: + raise ValueError(text) + + +def decode(mask, p): + check(type(mask) is int and 0 <= mask < 4**p, 'encoded port') + coordinates = frozenset(i for i in range(2 * p) if mask // (2**i) % 2) + check(len(coordinates) == 5 and len({i // 2 for i in coordinates}) == 5, 'five distinct pairs') + return coordinates + + +def feature_entry(left, right): + # Evaluate the bilinear form on explicit constant, singleton and pair + # features, independently of the primary overlap-polynomial routine. + common_singles = len(left.intersection(right)) + left_pairs = {frozenset(pair) for pair in combinations(left, 2)} + right_pairs = {frozenset(pair) for pair in combinations(right, 2)} + return 6 - 6 * common_singles + 4 * len(left_pairs.intersection(right_pairs)) + + +def bareiss(matrix, modulus=None): + """Fraction-free elimination over Z, or its second-prime field image.""" + array = [list(row) for row in matrix] + size = len(array) + check(size > 0 and all(len(row) == size for row in array), 'square matrix') + previous, sign = 1, 1 + for k in range(size - 1): + pivot_row = next((i for i in range(k, size) + if (array[i][k] % modulus if modulus else array[i][k])), None) + if pivot_row is None: + return 0 + if pivot_row != k: + array[k], array[pivot_row] = array[pivot_row], array[k] + sign = -sign + pivot = array[k][k] + if modulus: + inverse = pow(previous, -1, modulus) + for i in range(k + 1, size): + for j in range(k + 1, size): + numerator = pivot * array[i][j] - array[i][k] * array[k][j] + if modulus: + array[i][j] = numerator * inverse % modulus + else: + check(numerator % previous == 0, 'exact Bareiss division') + array[i][j] = numerator // previous + array[i][k] = 0 + previous = pivot % modulus if modulus else pivot + result = sign * array[-1][-1] + return result % modulus if modulus else result + + +def verify(): + check(all(MODULUS % i for i in range(2, isqrt(MODULUS) + 1)), 'second prime') + raw = (ROOT / 'WITNESSES.json').read_bytes() + evidence = json.loads(raw) + check(evidence['seed'] == 40, 'assignment seed') + expected = {(p, 'corrector') for p in range(5, 14)} | {(p, 'star') for p in range(5, 13)} + actual = {(row['p'], row['kind']) for row in evidence['witnesses']} + check(actual == expected and len(evidence['witnesses']) == 17, 'complete minor coverage') + dimensions, residues, exact_small = {}, [], [] + canonical = frozenset((0, 2, 4, 6, 8)) + for witness in evidence['witnesses']: + p, kind = witness['p'], witness['kind'] + left = [decode(mask, p) for mask in witness['rows']] + right = [decode(mask, p) for mask in witness['columns']] + check(len(left) == len(set(left)) == len(right) == len(set(right)), 'minor dimensions and uniqueness') + for label in left + right: + check((len(label & canonical) in (1, 3)) if kind == 'corrector' else 0 in label, + 'neighborhood/reader membership') + matrix = [[feature_entry(x, y) for y in right] for x in left] + determinant = bareiss(matrix, MODULUS) + check(determinant != 0, 'second-prime nonsingularity') + check(len(left) == witness['rank_lower'], 'claimed dimension') + dimensions[p, kind] = len(left) + residues.append(dict(p=p, kind=kind, dimension=len(left), determinant_mod_second_prime=determinant)) + if p == 5: + integer_det = bareiss(matrix) + check(integer_det != 0 and integer_det % MODULUS == determinant, 'integer determinant') + check(integer_det % evidence['prime'] == witness['determinant_mod_prime'], 'primary residue cross-check') + exact_small.append(dict(kind=kind, determinant=str(integer_det))) + # Independently construct the parity-class labels and their diagonal Gram. + even_words = [word for word in product((0, 1), repeat=5) if sum(word) % 2 == 0] + clique = [frozenset(2 * i + bit for i, bit in enumerate(word)) for word in even_words] + check(len(clique) == 16, 'clique cardinality') + check(all(feature_entry(x, y) == (16 if x == y else 0) for x in clique for y in clique), + 'quadratic parity clique') + log_lower = Fraction(549, 500) + series = sum((Fraction(1, 4**j * (2*j + 1)) for j in range(6)), Fraction()) + check(series > log_lower, 'logarithm certificate') + bounds = [] + for p in range(5, 13): + volume = 2**5 * comb(p, 5) + copies = 2 * p * dimensions[p, 'star'] + if copies < volume: + bound = Fraction(volume - copies, volume) / (2 * dimensions[p, 'corrector'] * log_lower) + bounds.append(dict(p=p, upper=str(bound))) + else: + check(p in (5, 6, 7), 'nonpositive-deficit cases') + ceiling = max(Fraction(row['upper']) for row in bounds) + tail = Fraction(1, 2 * dimensions[13, 'corrector']) / log_lower + frozen = json.loads((ROOT / 'sources/selected-result-base.json').read_text()) + check(tail < ceiling < Fraction(frozen['kappa']), 'strict comparison to frozen selection') + return dict(schema='five-port-second-implementation-v1', witness_sha256=hashlib.sha256(raw).hexdigest(), + second_prime=MODULUS, minors=residues, integer_determinants_p5=exact_small, + finite_bounds=bounds, ceiling=str(ceiling), tail=str(tail), + selected_kappa=frozen['kappa'], human_independent_review=False) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-certificate', type=Path) + args = parser.parse_args() + report = verify() + if args.write_certificate: + with args.write_certificate.open('x') as handle: + handle.write(json.dumps(report, indent=2) + '\n') + else: + check(json.loads((ROOT / 'INDEPENDENT.json').read_text()) == report, 'second receipt equality') + print('PASS_FIVE_PORT_SECOND_IMPLEMENTATION minors=17 prime=65519 exact_integer_determinants=2 ' + 'ceiling=125/76433 no_new_kappa') + + +if __name__ == '__main__': + main() diff --git a/research/five-port-quadratic-decoder/sources/format-axioms-README.md b/research/five-port-quadratic-decoder/sources/format-axioms-README.md new file mode 100644 index 0000000000..2f7aaf5b82 --- /dev/null +++ b/research/five-port-quadratic-decoder/sources/format-axioms-README.md @@ -0,0 +1,805 @@ +# Format limits (no κ claim): a certified ceiling, a spec census, structural lemmas and helper bounds + +This package states results about the limits of the current construction format (B_K compressed windows, star +copies, whole-residual hosting) and checks the ones that can be checked. **It makes no κ claim and ships no word.** +Each result comes with its scope and assumptions. Each is marked: + +- **checked**: `verify.sh` recomputes it from the files listed below (exact or certified arithmetic unless stated); +- **argued**: a proof or proof sketch in this README; +- **recorded**: an input taken from a run or a PR that `verify.sh` does not repeat (the file and its source are named). + +```sh +python3 -m pip install -r research/format-limits/requirements.txt +bash research/format-limits/verify.sh /fresh/output/dir # from a checkout or `git archive` of the whole repository +``` + +Python ≥ 3.11 with numpy, scipy, sympy, python-sat and ortools (`requirements.txt` pins a tested set). Step 0 +checks the package against `MANIFEST.sha256`, the vendored inputs against the git blob ids of their PR commits +(`SOURCES.json`) and the files of main it reads (`DEPENDS.json`). Steps A–E print one `PASS`/`FAIL` line per claim. +About 2 minutes on 12 cores (six checks at a time). + +**Tested environments** (fresh `git archive`, every claim PASS): + +| Python | numpy | scipy | sympy | python-sat | ortools | how installed | +|---|---|---|---|---|---|---| +| 3.11.17 | 2.4.6 | 1.17.1 | 1.14.0 | 1.9.dev15 | 9.15.6755 | fresh venv from `requirements.txt` | +| 3.14.7 | 2.4.6 | 1.17.1 | 1.14.0 | 1.9.dev15 | 9.15.6755 | fresh venv from `requirements.txt` | +| 3.14.7 | 2.5.4 | 1.18.1 | 1.14.0 | 1.9.dev15 | 9.15.6755 | fresh venv, latest releases | +| 3.14.7 | 2.3.5 | 1.17.0 | 1.14.0 | 1.9.dev15 | 9.15.6755 | development venv | + +Values that come from floating-point solvers (the hosting LP, the coupled-cover MILP) are compared with explicit +tolerances; the certified roots are rational intervals. + +## Results at a glance + +| id | result | status | +|---|---|---| +| A | **Format ceiling, rev. 2.** Under the accounting axioms of §A.1, every supplier in the format has saving a ≤ X(s, h/k, x) (root of the slot-domination bound). On the realised units, X* = 6.0005·10⁻³ (bit, 111 lines, decoder constant 63) and 5.1863·10⁻³ (complex, 112 ports, copy cost 64), both at s = 5, so **κ ≤ 5.1595·10⁻³** (complex binds). | theorem argued; every number checked (`a1`–`a5`) | +| A.4 | The axioms hold on the frontier words #555 (bit) and #568 (complex): published values reproduced from their profiles, deficit identity with equality, B_K idle windows literal, slot domination at nine values of q. | checked (`a3`); (Bat)/(Hst) for #568 argued from its README | +| A.5 | At s = 9 the frontier sits 2.66× (bit) / 2.50× (complex) under the ceiling; 87% / 93% of the log-gap is helper cost, 19% / 25% data-run fragmentation, and hosting recovers 7% / 18%. | checked (`a4`); #568 uses a recorded idle remainder | +| A.6 | The rev. 1 scope x = 3/5 (κ ≤ 4.5151·10⁻³) is superseded: the punctured units have x = 63/111 and 64/112. | checked (`a1`) | +| B | 25 format rules classified as spec / proved / convention, with file:line evidence in the upstream paper and the hub's checkers, and the corrections the census found. | anchors checked (`b`); classification argued | +| C.1 | Frame sandwich: a register's frame lies between the span of what it carries and the orthogonal of what it will serve; the three complex frame walls are its faces; leaving it is exact and costs d(f, g). | argued; toy checked (`c1`) | +| C.2 | Lemma N: the per-target rank-1 port factor is a gauge of the endpoint frames, always paid; any detour off the geodesic interval costs exactly 2. | proof argued; toys checked (`c2`) | +| C.3 | Lemma R: complement sinks w_t^⊥ (w·u = 1) are legal at zero rank and port cost, and forced to w_t = u_t on every target of the four complex words checked (#531; #569 width-7 and four-cold; #571 combined). | checked (`c3_gate0`, `c3_taint`) | +| C.4 | Lemma Q: a degenerate-label unit is dominated by its quotient (copy cost and window), so degenerate spans give no new (w, x) points. | proof argued; toys and families checked (`c4`) | +| C.5 | Lemma λ: a phase-frame butterfly needs λ = ±i (and 2 invertible) in its payload ring; b < c is the price of √−1, and the outer already uses shift twiddles. | argued; instances checked (`c5`), anchors (`b`) | +| C.6 | At the E8 decoder pattern with window ≤ 9 the label pairing B = W·Uᵀ is unique (= B0); every W ≠ U is a gauge. Window 8 is impossible. | checked (`c6`, SAT without proof logs) | +| C.7 | A rank-r descent costs 2r data mass in every call (−5.63% c on #555, −5.65% b on #568 per rank-1 descent); within that price class a schedule with a paid descent is dominated. | toy and prices checked (`c7`); dominance argued | +| C.8 | Splitting one helper residual across two hosting streams meets a trace obstruction under every invertible storage change; uncharged, it is worth at most +0.67% b on the current complex frontier. | argued | +| D | Design-free helper floors in the drop-free monotone-chain model: bit ≥ 212 (sink-only targets) / 138 (strict) vs 439 shipped; complex ≥ 107 / 0 vs 496. Coupling the levels adds 0. The "224 carriers" complex floor is a design choice, and carriers are register-neutral in the calibrated ledger. | checked (`d1`–`d3`), given the argued crossing lemma | +| E | Complex helper price by class and width on #569 (0.039–0.140% b per helper at k = 1; the hosting offset depends on width only), and the moment-cost census by class on #555 and #569. | k = 1 prices, control and census checked (`e1`, `e2`); k > 1 rows recorded | +| F | Cost structure: a change paid in every local word must buy about 2.8% of the supplier value per rank unit; open problems: per-word enablers, a non-star decoder, the schedule/ρ freedom, new skeletons. | conclusion from checked prices | + +Earlier statements this package relies on: Theorems A–C of #446 (DreamingOfClouds, open; content-frame invariant, +stage-window additivity, pairing-rank copy floor). They are cited as premises and are not re-proved here. #446 states +Theorem B for rank-1 labels (every number in this package is at k = 1), and its Theorem C value 72 for the bit E8 +unit is computed there and not replayed here. + +## A. Format ceiling, rev. 2 + +### A.1 Scope S2 (accounting axioms) + +A word is a B_K compressed-window block for one supplier (bit or complex), replicated T times, with s = 2K + 1 +stages, v ports of label rank k and stage window h, copy rank cst per stage, and any helper network (any R, widths, +local programs), any banking or hosting rule and any halving depth. Writing z_r for the number of paid children of rank +r and g_q(r) = r((m/r)^q − 1): + +- **(P) pressure identity.** The supplier saving a is the root q of Σ_r z_r g_q(r) = D. (The hub pricers add a + nonnegative fallback term, which only lowers their root.) +- **(Dfc) deficit.** D = T[(s − 1)vk − s·cst], with cst ≥ cst_min(U), the star floor of the unit U (the pairing-rank + floor of #446 Theorem C holds for any copy tree; the star form β_j ≥ k·w_in is the scope assumption). +- **(Win) window.** Every data register climbs a ≥ h − k per stage and m = k + s·a (#446 Theorem B gives + m ≥ k + s(h − k); #386's compressed windows attain it). X is non-increasing in a, so a = h − k is the extreme case. +- **(Sch) B_K schedule.** Stage j activates one bank pair (2 data registers per port per replica); pair 0 is active at + stages 0, 1, 2 and pair p ≥ 1 at 2p + 1, 2p + 2. Idle frame changes per copy (2v copies): pair 0 has [(2K − 2)a]; + pair p ∈ 1..K − 1 has [2pa, a, (2K − 2p − 2)a] (a bridge read splits the pre-stretch). +- **(Bat) batching.** A paid child executes part of one frame change Δ and has rank ≤ rank Δ (Δ is a register's + frame change, or, as in #448, one idle change across the copies of one idle child). Local children have rank ≤ a + (data registers) and ≤ h (helpers, copies). +- **(Hst) hosting is accounting.** A hosted helper child is a local child (rank ≤ h) that executes coordinates of an + idle frame change; the rest of that change is paid in children of rank ≤ its rank; an unhosted helper lives on a bank + wire. + +### A.2 Theorem and proof sketch + +Per port (v and T cancel), the **forced slots** are: the active climbs (mass 2sa, cap a), the copy drops (mass s·x, +x = cst/v, cap h) and each idle frame change of rank r of the schedule (mass 2r, cap max(r, h)). Let +F_s(q) = Σ_slots mass · ((m/cap)^q − 1) and D_s = (s − 1)k − s·x. + +**Theorem.** For every word in S2 on a unit U, a ≤ X(s, h/k, x_U) := the root q of F_s(q) = D_s, with +x_U = cst_min(U)/v(U). Since e^y − 1 ≥ y, also X ≤ D_s/Cost_s with Cost_s = Σ_slots mass · ln(m/cap). + +*Proof sketch.* (1) Monotonicity: each g_q(r) increases in q for r < m, so a(z, D) ≤ a(z', D') whenever f_z ≥ f_z' +pointwise and D ≤ D'. (2) Slot domination: by (P) the paid mass executes every coordinate of every forced slot; by +(Win), (Sch), (Bat) and (Hst) every child touching a slot has rank ≤ its cap; φ_q(r) = (m/r)^q − 1 decreases in r, so +splitting each child's mass over the slots it touches gives f_N(q) ≥ F_s(q; cst_N); children touching no slot +contribute ≥ 0. (3) Helpers never shift D or m (call this Lemma H): Theorem B bounds m with target frames only; a bank wire is restored +scratch, so its saving is ≤ 0; a data register saves ≤ k whoever executes its coordinates; copies cost ≥ cst_min for +any tree. X is non-increasing in a (d/da of each slot term is ≥ 0 by Bernoulli's inequality). The cap max(r, h) on +idle slots absorbs the one place where hosting lowers paid cost (a width-h helper child on a single-stage idle slot); +it costs 1% against the literal R = 0 profile. (4) F_s increases and D_s decreases in cst, so cst_N may be replaced by +cst_min. Apply (1). + +**General k (argued; no number here uses it).** Scaling every rank by k (a = k(w − 1), h = kw, m = k(1 + s(w − 1)), +every slot mass and D multiplied by k at fixed x/k) leaves each ratio m/cap unchanged, so X depends only on +(s, w = h/k, x/k). Every number in this package is at k = 1. + +**κ.** The outer assembly seeds s0 = min(c, (1 − β)b) − 10⁻²⁴ and bootstraps x ↦ (1 − s0)s0 + s0·x from below; the map +is increasing with fixed point s0, so κ ≤ X/(1 + X) with X = min(X_bit*, X_cx*), each side at its own best s. + +### A.3 Numbers (certified; `a1_ceiling_roots.py`, `a2_ceiling_sup.py`) + +| unit | x | s = 3 | **s = 5** | s = 7 | s = 9 | s = 11 | s = 13 | +|---|---|---|---|---|---|---|---| +| bit, 111 live lines, decoder constant 63 (#545, #555), h = 8 | 0.5676 | 5.9474e-3 | **6.0005e-3** | 5.2095e-3 | 4.6072e-3 | 4.1490e-3 | 3.7879e-3 | +| complex, 112 ports, copy cost 64 (#523 → #569), h = 9 | 0.5714 | 5.0474e-3 | **5.1863e-3** | 4.5130e-3 | 3.9946e-3 | 3.5989e-3 | 3.2865e-3 | + +Roots are rational-interval brackets of width < 10⁻¹⁵; the upper end is the certified value. + +- **κ ≤ 5.1594938·10⁻³ < 5.1595·10⁻³**; the complex side binds. The bit-only corollary is c/(1 + c) ≤ 5.9647·10⁻³. +- **The supremum over s is at s = 5** on both units. For odd s = 7..401, the certified D_s/Cost_s stays below X(5); + the largest values are 5.2311·10⁻³ (bit) and 4.5292·10⁻³ (complex), both at s = 7. For s ≥ 403 a tail bound applies: + Cost_s/v ≥ 2Σ_{p 2Ka), and + Σ_{p=1}^{K−1} p ln(K/p) ≥ K²/4 − K/e − K/2. Then X ≤ D_s/Cost_s < (1 − x)s/(4a(K²/4 − K/e − K/2)), which is + decreasing in K and equals 6.27·10⁻⁴ (bit) / 5.44·10⁻⁴ (complex) at s = 403. + - *Proof of the inequality (erratum to rev. 1, which invoked "trapezoid error for a concave function", the wrong + direction).* f(p) = p ln(K/p) is concave, so by Hermite–Hadamard f(p) ≥ ∫_{p−1/2}^{p+1/2} f. Summing gives + Σ_{p=1}^{K−1} f(p) ≥ ∫_{1/2}^{K−1/2} f = K²/4 − ∫_0^{1/2} f − ∫_{K−1/2}^K f. Both removed pieces are small: + the first is (1/8)(ln K + ln 2 + 1/2), and the second is ≤ (K/2)·ln(K/(K − 1/2)) ≤ K/(4K − 2) ≤ 1/3. Their sum is + ≤ K/e + K/2 for every K ≥ 2. The script also checks the inequality numerically for K = 2..5000. +- **Frontier against the ceiling at s = 9.** X(9)/c = 2.658 for #555 (c = 1.733053·10⁻³), and X(9)/b = 2.499 for + #568 (b = 1.598685·10⁻³). +- **Copy charge.** One copy-rank unit per stage (bit cst 63 → 62) raises X by +3.90% (s = 5), +2.82% (s = 9) and + +2.65% (s = 11). + +### A.4 The axioms on the frontier words (`a3_axioms.py`, checked) + +| check | words | result | +|---|---|---| +| (P): certified root of the published global profile at the word's (m, D) vs its published value | #510 R480 s9, #543 R420 s9/s11, #545 p111 s11, #555 p111 s9/s11, #568 | root ≥ published; relative difference 1.2–1.7·10⁻⁹ on the bit pipelines (consistent with their nonnegative 10⁻¹⁶ fallback term), 5·10⁻¹⁸ on #568 | +| (Dfc): m·W − rank mass = T[(s − 1)v − s·cst] with integral W | same seven profiles | equality (e.g. #555: 64·28416 − 1,808,352 = 10,272; #568: 73·7168 − 520,704 = 2,560) | +| (Win): m = k + s(h − k); largest child = literal idle remainder (2K − 2)a | same | m = 64/78/73; largest child 42/56/48 on #543, #545, #555, #568 (#510's largest child is 8) | +| (Sch): active + copies + idle slot mass = rank mass | #555, #568 | 447,552 + 18,144 + 1,342,656 = 1,808,352; 129,024 + 4,608 + 387,072 = 520,704 | +| (Sch): idle windows per replica = idle_slots(K = 4, a = 8) on both banks | #568 PLAN, 8 replicas | {8: 6, 16: 4, 32: 4, 48: 4} on every replica | +| (Hst): helpers hosted whole, no banks | #555 | bank assignments 0; hosted residuals 126,432 = 439·288 | +| Lemma 2 on a grid: min of f_N(q)/F_s(q; cst_N) over nine values of q in [10⁻⁵, 1] | all seven | 2.29–2.66 (≥ 1) | + +**(Bat) at child level.** #555's helper runs have rank ≤ 5 ≤ h (checked by the replay in `a4_gap.py`). #568's helper +children have rank ≤ 6 ≤ h (its implied helper histogram in `a4_gap.py`). #568's README (commit 71c99ac, +research/complex-multicold/README.md:22) reports one whole owner for all 36,288 helpers, no auxiliary banks and 27,679 +cross-replica roles; a cross-replica role hosts helper children of one idle change at rank ≤ h, so it falls inside +(Bat)/(Hst) (argued). No structural axiom is violated by #555 or #568. + +### A.5 Gap decomposition at s = 9 (`a4_gap.py`, checked) + +| step | #555 bit | #568 complex | +|---|---|---| +| A: theorem skeleton (R-free; idle slots at cap max(r, h)) | 4.6072e-3 | 3.9946e-3 | +| B: literal R = 0 (each idle slot one child of its own rank) | 4.5661e-3 | 3.9631e-3 | +| C: B with the real data-register runs and copy children | 3.7868e-3 | 3.1544e-3 | +| D: C plus every helper run paid unhosted (the only step with more rank mass) | 1.6183e-3 | 1.3517e-3 | +| E: the real word (helpers hosted whole, idle remainders paid) | 1.7331e-3 | 1.5987e-3 | + +Shares of ln(A/E) (0.978 / 0.916): + +| component | #555 | #568 | +|---|---|---| +| helpers | 87% | 93% | +| data fragmentation | 19% | 25% | +| literal vs cap | 1% | 1% | +| hosting | −7% | −18% | + +Steps A, B, C and E have the same rank mass, m·W − D (1,808,352 and 520,704). + +Inputs: + +- **#555.** Data, helper and copy runs are replayed from the published word. The replay matches #555's local + histogram, and the helper mass is 8R. The idle remainder is the published profile minus 288 × the local profile; + 75.3% of the skeleton idle mass is hosted. +- **#568.** The data-register runs per call come from #569's four-cold provider word (the same x/y ladders). The paid + idle remainder {1: 93, 2: 93, 3: 2118, 7: 1, 48: 1713} is **recorded** from our replay of #568's hosting + (`data/ceiling/gap568-inputs.json`). Its 4,018 children match the "4,018 positive idle remainders" of #568's README + (checked), and the implied helper histogram is nonnegative (checked). + +The headroom under S2 is therefore almost entirely helper cost. Even with zero helper cost and real data +fragmentation, the words would sit 2.19× (bit) / 1.97× (complex) above today. + +### A.6 The superseded numeric scope of (Dfc) + +Rev. 1 of this ceiling fixed cst_min = 72 and x = 3/5 (the full 120-line E8 unit) on both sides. That gave X_bit* = +5.1598·10⁻³, X_cx* = 4.5356·10⁻³ and κ ≤ 4.5151·10⁻³ (checked, `A1.rev1-superseded`). + +The punctured units that the frontier now uses have smaller x: + +- bit: #545/#555 keep 111 live lines with decoder constant 63; +- complex: the #523 lineage has 112 ports with copy cost 64. + +So x = 63/111 = 0.5676 and 64/112 = 0.5714. With x_U taken from the realised units the ceiling is §A.3's +κ ≤ 5.1595·10⁻³. The structural axioms are unchanged. + +Status of cst_min per unit: + +| unit | cst_min | status | +|---|---|---| +| bit 120/72 | 72 | proved given #446 Theorem C: the F2 decoder of the E8 pattern needs 9 totals (its F2 minrank is 9; c = 8 is UNSAT, checked in `c6`), and each star total costs β = 8, the Gram rank of an 8-line in-cap clique (premise, not replayed) | +| bit 111/63 | 63 | the star floor among punctures of p ≤ 25 lines: Δcst ≤ min(p, 9), from an exact matroid-greedy search over the 9-dimensional code that this package does not reproduce (**argued**, not checked here). For 26 ≤ p ≤ 52 only the total D gain s·Δcst − (s − 1)p ≤ 9 is bounded, which does not pin x. | +| complex 112/64 | 64 | 8 × 8, the star floor at w_in = 8, attained (**argued**) | + +A unit with smaller x would move X by about +2.8% per copy-rank unit at s = 9 (§A.3). For scale, two units with +smaller x that no word realises are checked as well (`A1.outside-scope`): bit x = 54/102 gives X* = 8.2457·10⁻³ and +complex x = 56/104 gives X* = 6.8000·10⁻³, both at s = 3. They lie outside the realised-unit scope of the theorem. + +### A.7 What each scope rule is worth (`a5_scope_multipliers.py`, checked) + +Multiplier of the ceiling if one rule is dropped. Each cell is best-s multiplier / s = 9 multiplier. + +| rule dropped | bit 111/63 | complex 112/64 | +|---|---|---| +| star scope (copy charge x → 0) | ×6.77 / ×2.79 | ×6.91 / ×2.83 | +| B_K idle frame changes free | ×1.67 / ×2.14 | ×1.68 / ×2.15 | +| all idle changes of a copy in one child | ×1.19 / ×1.55 | ×1.20 / ×1.55 | +| bridges off the idle stretches (no split) | ×1.15 / ×1.18 | ×1.15 / ×1.18 | +| data local climbs batched to h (cross-register) | ×1.12 / ×1.03 | ×1.08 / ×1.02 | +| idle free and local batching together | ×1.79 / ×2.28 | ×1.79 / ×2.27 | +| family window one smaller at the same x | ×1.16 / ×1.16 | ×1.14 / ×1.14 | + +Hosting cannot raise the ceiling (step (3) of the proof in §A.2). Full relaxation of (Bat), with arbitrary batching up to rank m, +would give no bound, because rank-m children cost 0. + +**Not covered:** + +- non-B_K schedules (a different number of active pairs per stage changes (Sch) and (Dfc)); +- non-star decoders (totals with β_j < k·w_in), and units with smaller x than the realised ones (see A.6); +- labels outside the cross-field unit; +- any change to (P), such as children of rank larger than their frame change, or a new outer assembly. + +## B. Spec versus convention census + +`b_census_anchors.py` checks every file:line anchor of the rule table (B.2), 73 in all, and the four corrections +marked "checked" in B.3. Line numbers are as of the base commit 7dfa22b. Each anchor's quoted text must lie within two +lines of the cited line, except in docs/research/ (the hub's ledgers and reviews, which main rewrites often), where it +is matched by text anywhere in the file. The line ranges cited in the prose of B.1 and B.3 were read by hand at +7dfa22b and are not machine-checked. Paths are relative to the repository root, and `U/` is +`upstream/build/sections/`. The classification is argued: + +- **S**: mandated by the upstream paper or interfaces; +- **P**: proved necessary given the cited S/C rules; +- **C**: a convention of the paper's instance or of the hub's checkers and templates, changeable if the replacement is + proved. + +### B.1 What upstream imposes + +- **Bit contract** (the only bit-side interface), U/04-swap.tex:105-123. A finite circuit of W wires whose pointwise + bit gates induce a *permutation* ρ. There is one rational m×m matrix per terminal and per gate, common to every wire + at that gate. The cost is s = Σ rank_Q(M_head − M_tail), with M_out(ρ(w)) − M_in(w) = I_m on every role and s < Wm. + The recurrence is F_k ≤ (s/W)F_{k−1} + O(1) (:197-211). No subspaces, nesting, banks, pairs or nondegeneracy appear. +- **Complex interface**: + - frames C_U = H^m diag(i^{q_U}) H^m, with q_U(x) = wt(P_U x) mod 4 for nondegenerate binary U (U/03-motifs.tex:528-561); + - an edge is a product of one kernel (aI + bX_v)^{±1} per vector of an orthonormal basis of the residual of + comparable labels (:568-583); + - endpoint C^{⊗m} on every role after free per-role corrections (:579-582, :641-668; U/05-layers.tex:127-154); + - the implementation P_M conjugation needs only invertible M (U/05-layers.tex:86-103). +- **Common-frame identity** for any invertible D_v: U/03-motifs.tex:154-186. +- **The paper's instance**: + - nondegenerate nested labels (U/03-motifs.tex:199-208, 351-364); + - terminal labels X_a: U_a → F, Y_a: 0 → U_a^⊥ (:235-243); + - the signed exchange of X_a and Y_a (:89-100); + - arbitrary, restored scratch (:34-46). +- **Outer.** Two suppliers are composed through 08-assembly.tex (:16-48, κ at :849-866, :995-1000). The transforms + are Nussbaumer synthetic transforms whose roots are signed shifts (U/00-introduction.tex:44-56, U/06-transforms.tex). +- **The maintainer's interface list**, docs/research/community-pr531-review.md:116-125: + - all-size compilation; + - common-label and mutable-basis realization; + - normalized residual wrappers as uniformly priced operations; + - whole-call correlated-helper hosting; + - compressed windows and restored rows; + - grids, tape, precision; + - the analytic transfer. + + The same review of #531's integration says the fixed-word ceiling and family-optimality discussions it carries + were "not independently certified" (:130-134). + +### B.2 Rule table + +Multipliers are from §A.7 (best s / s = 9, bit unit unless stated). + +| # | rule | class | anchors (file:line) | evidence and history | ceiling multiplier if relaxed | +|---|---|---|---|---|---| +| 1 | Common frame at every gate | S | U/03-motifs.tex:157; U/04-swap.tex:111; legality_h.cpp:11; audit_local.py:64; LemmaG/Stream.lean:106 | never changed; an ADD across frames needs an adapter edge priced d(f, g) | 1.00 | +| 2 | Frames are nondegenerate subspaces | spec: any invertible D_v (S); nondegenerate subspaces: the paper's instance (C) | U/03-motifs.tex:154, :203; U/04-swap.tex:110; gram_frames.py:46; notes/general-clifford-frames.tex:21 | #130's general frame lemma covers arbitrary (also degenerate) binary subspaces, d = dim U + dim V − 2 dim(U ∩ V); main has its TeX note and Python checks, its Lean proof is in an external repository (a conditional interface); degenerate labels are dominated by their quotient (C.4) | none by itself (only through x) | +| 3 | Nesting: climbs along a register's life; drops only as copies or centre steps | C (priced, not forbidden) | U/03-motifs.tex:352 (the paper has decreasing edges); U/05-layers.tex:83; legality_h.cpp:11; audit_local.py:45, :128; LemmaG/Stream.lean:111 | #425's full → 0 centre copies; a non-nested step is exact and costs d(f, g) (C.1, C.7) | 1.00 (two nested edges) | +| 4 | Exact restoration of helpers and dirty registers | S (same endpoint operator on every role; scratch arbitrary); "ρ fixes scratch" is C | U/03-motifs.tex:46, :98, :581; U/05-layers.tex:150; columns_k.cpp:57; audit_local.py:101 | no PR permutes scratch | 1.00 | +| 5 | ρ = signed exchange of X_a and Y_a, pairwise | C (any permutation ρ is legal) | U/04-swap.tex:107; U/03-motifs.tex:99, :628; bit_global.py:55; columns_k.cpp:56 | never varied | not quantified | +| 6 | Terminal labels X_a: U_a → F, Y_a: 0 → U_a^⊥; targets inside u_t^⊥ | C (the paper's choice; the ⊥ relations then follow from #446 Thm A) | U/03-motifs.tex:235, :240; U/05-layers.tex:128, :146 | complement sinks are legal at zero cost but forced on every current decoder (C.3) | 1.00 on current decoders | +| 7 | Rank-1 labels (k = 1) | C | U/03-motifs.tex:233 | X depends only on (s, h/k, x/k) (§A.2) | through (w, x) | +| 8 | Star copies (cst = Σβ_j, β_j ≥ k·w_in) | scope assumption of the ceiling; the pairing-rank floor itself is proved for any copy tree (#446 Thm C) | legality_h.cpp:1; columns_k.cpp:39 | every PR's totals are star | ×6.77 / ×2.79 (complex ×6.91 / ×2.83); +2.8% per copy-rank unit at s = 9 | +| 9 | E8 cross-field unit (h = 8 bit, 9 complex) | C (family) | U/03-motifs.tex:221, :225 ("the scalar domain need not equal the label field") | — | window one smaller: ×1.16 (complex ×1.14) | +| 10 | Window m = k + s(h − k) | P (#446 Thm B) | — | attained by #386 | 1.00 in model | +| 11 | Deficit D = T[(s − 1)vk − s·cst] | P given rows 8 and 12; spec form D = mW − s | U/04-swap.tex:122; U/03-motifs.tex:360 | equality on seven profiles (§A.4) | through rows 8, 12 | +| 12 | B_K schedule (one dependency chain, alternating locals, bridges, idle children) | P given row 13 | bit_global.py:49; columns_k.cpp:46; Work__Bridge__Net.lean:56 | no other schedule on record | idle free ×1.67 / ×2.14; one idle child ×1.19 / ×1.55; no split ×1.15 / ×1.18 | +| 13 | One (X, Y) bank pair per invocation (LOCAL = 2V + R) | C | bit_global.py:12; columns_k.cpp:31; Work__Bridge__Net.lean:55 (one I : Inv for all stages) | no local on two pairs on record | feeds row 12 | +| 14 | (Bat): a paid child executes one frame change | axiom of the ceiling: one register across a local/bridge is the equal-frame rule; cross-register batching is open | docs/research/pr-ledger.md:403, :405 (#448 and #451 unreviewed) | #451's trace obstruction to #448's split residuals (C.8) | local batching ×1.12 / ×1.03; with idle free ×1.79 / ×2.28 | +| 15 | Whole-residual hosting | accepted conditional interface | community-pr531-review.md:122; idle-axis-hosting/PROOF.md:43 | #442 accepted; split residuals disputed (C.8) | 1.00 (Lemma H, §A.2) | +| 16 | One owner per stream (#458) | P inside #442's stream model | LemmaA/Realize.lean:95 (`one_owner_needed`) | relaxed to disjoint footprints | 1.00 | +| 17 | Source registers never destinations | C (#370's checker assertion) | e8-bit-carrier-skeleton/README.md:67-68 | sufficient, not necessary (#425); relaxed by #433, #493 | already taken | +| 18 | Payload bounds (2^104 bit, 2^192 complex prefix, 2^80 prime witnesses) | C, never binding | columns_h.cpp:25; columns_k.cpp:34; finite_check.py:98; audit_local.py:103; gram_frames.py:17 | — | 1.00 | +| 19 | F2 payload coefficients | C | columns_h.cpp:27 | — | 1.00 | +| 20 | Replication T | C | bit_global.py:11; finite_check.py:86 | #505 asynchronous replicas | 1.00 (T cancels) | +| 21 | 47-inequality outer assembly | structure S, constants C | outer.py:27; U/08-assembly.tex:37; assembly-domain-audit.md:21 | the 1/32 domain cap is conservative and not binding | 1.00 | +| 22 | κ is the composition of the two suppliers | S | U/08-assembly.tex:37; outer.py:29, :30 | — | — | +| 23 | Two suppliers: complex butterfly layer, bit address shear | S | U/00-introduction.tex:48, :56, :118; U/06-transforms.tex:12 | shift twiddles are already in the outer (C.5) | — | +| 24 | Pressure identity (a rank-r child priced as a fraction of a call) | inherited conditional ("normalized residual wrappers as uniformly priced operations") on the paper's rank-1 recurrence | U/04-swap.tex:197; community-pr531-review.md:122 | — | defines the ceiling | +| 25 | Bridges X → X and Y → Y only | P (X wires contain q, Y wires do not) | columns_k.cpp:43 | — | — | + +Abbreviations: + +- `legality_h.cpp`, `columns_h.cpp`, `columns_k.cpp` and `gram_frames.py` are in + research/e8-bit-carrier-skeleton/code/bit/checkers/; +- `audit_local.py` is research/direct-delivery504-global/code/audit_local.py; +- `bit_global.py` is research/e8-early-reset-kernel/bit_global.py; +- `Work__Bridge__Net.lean` is in research/five-stage-gen4-banks/inputs/complex/sources/; +- `finite_check.py` is research/five-stage-gen4-banks/finite_check.py; +- `outer.py` is research/e8-bit-carrier-skeleton/code/pricing/outer.py; +- `LemmaG/`, `LemmaA/` are under research/e8-lemma-g-lean/ and research/e8-lemma-a-lean/; +- `community-pr531-review.md` and `assembly-domain-audit.md` are under docs/research/. + +### B.3 Corrections, as the census found them + +1. **The bit interface is the shear contract alone** (U/04-swap.tex:105-123). Subspace labels, nesting, Gram + orthogonality, bank pairs and the pair exchange are construction-layer choices of the paper's instance + (:199-243, 351-364), not interface requirements. +2. **Nesting is priced, not forbidden.** + - The paper itself has decreasing edges (U/03-motifs.tex:352-353). + - The paper counts kernels on decreasing edges (U/05-layers.tex:83). + - #130's frame lemma prices non-comparable labels by d(f, g). + - The checkers enforce nesting as a pricing rule. +3. **The bit legality checker** keeps its MOVE (nested and exactly priced), ADD (common frame) and COPY-lifecycle rules + on legality_h.cpp:11; line 10 holds the containment helper and the owner/helper selection (checked). +4. **The invariant `Inv`/`GInv`** used by the complex five-stage bridge is imported (`import Work.Bridge.Inv`) and + defined nowhere in main (checked). "One X bank and one Y bank per invariant" therefore rests on its use in + `Bridge2` and in bit_global.py / columns_k.cpp, not on a definition in the repository. +5. **#370's assertion "x registers are never destinations"** is a sufficient, not a necessary, condition (#425's + scalar-interface lemma; #493's README) (checked). +6. **The outer already uses shift twiddles** (Nussbaumer synthetic transforms; U/00-introduction.tex:44-50); the + complex supplier is the H_0 butterfly layer (:114-121). A ring change does not remove it (C.5). +7. **Complement sinks** (sink = any complement of the source label, w·u = 1) are not covered by the earlier phase-frame + null result: the sink stays a plain label with a new projection. They are legal (C.3, gate 0), and Lemma R closes + them on every current decoder. +8. **The only untested spec freedom with a ceiling term ≥ ×1.15** is the schedule/ρ family (rows 5, 12, 13). The + large multipliers (×6.8 copy charge, ×1.16 window) are scope and family terms, not rules. + +Caveats of the census itself: + +- "Sink = any complement of the source label" (row 6) was the census's own reading of U/05-layers.tex:145-148; it is now + settled by C.3. +- "A plain swap of two scratch roles cannot gain" (row 4: shared gate frames give ≥ 2m on the swapped pair) is the + census's own argument and is not re-derived here. +- #448 and #451 are unreviewed in the hub's ledger, so the "conceded" status of split-residual hosting rests on the + contributors' own record. + +## C. Structural lemmas + +### C.1 Frame sandwich and the complex frame walls (argued; toy `c1_sandwich_toy.py` checked) + +**Lemma (sandwich).** Let R be a register at time t, and consider paths that carry no priced drop. Then + + span{frame(r, t′) : r's content reached R drop-free by t} ⊆ frame(R, t) ⊆ (span{L_q : target q that R's content reaches drop-free after t})^⊥. + +*Proof sketch.* The lower side is #446 Theorem A, applied with any register as origin. For the upper side, a target q +ends at L_q^⊥ because its terminal label absorbs the port gate (T_{u^⊥} = F·C_u^{−1} up to monomials). Chains are +monotone, and a copy taken at t sits at its parent's frame (common frame at the copy gate), so it inherits the +parent's future. Exactness uses neither side: both are accounting. + +**Consequences** on the complex unit (labels in F_2^9, 112 ports): + +- **(W1)** The common station of a term whose readers span u_a^⊥ is the point ⟨u_a⟩. A cut shared by all readers of a + term is therefore one point per term. +- **(W2)** A copy serving a face of four targets of rank-3 span has frame dimension ≤ 6. A group of eight copies whose + faces span rank 4 has a common frame of dimension ≤ 5. +- **(W3)** Run backwards on the cleanup, the lower side gives end(X) ≥ the join of the frames of every register that + X's restoration reads. + +**Leaving the sandwich is legal and priced.** The toy (n = 4) puts three readers whose labels span u_a^⊥ at a station +⟨w⟩ outside every u_i^⊥ and then takes a non-nested step to u_i^⊥: + +- both networks are exact on 64/64 basis columns; +- every child's Clifford rank equals d(A, B) = dim A + dim B − 2 dim(A ∩ B), including the non-nested rank-4 steps; +- the charge is 18 = 13 + 3·2 − 1 against the standard network's 13. + +Relaxing "targets avoid u_t" costs +2 data mass per relaxed target per call (C.7 prices this). + +### C.2 Lemma N: the port factor is a gauge, always paid (`c2_port_gauge.py`) + +**Setting.** C_v = ((1 + i)I + (1 − i)X_v)/2, so C_v² = X_v. The full transform is F = Π_{w ∈ orthonormal basis} C_w, +and T_{q^⊥} = F·C_q^{−1} (#514's repeated-axis identities). In the hub's controller a source family runs +⟨q⟩ → … → F and a target family runs 0 → … → q^⊥. Each data family saves exactly one unit (m − 1 instead of m), which +is the C_q gauge: (s − 1)vkT = 8·112·8 = 7168 on the complex side, of which copies take 4608 and D = 2560 remains. + +**Lemma N.** For a parent child Z = C^{⊗A}, + +- rank(C_q^{±1}Z) = rank Z − 1 if q ∈ span(A) with odd support; +- rank(C_q^{±1}Z) = rank Z + 1 if q ∉ span(A) and q ⊥ A. + +**Theorem N (proof).** With d(f, g) = dim f + dim g − 2 dim(f ∩ g), any path f0 → G → f1 costs at least d(f0, f1), +with excess + +- **target** (0 → q^⊥): d(0, G) + d(G, q^⊥) − d(0, q^⊥) = 2(dim G − dim(G ∩ q^⊥)) ∈ {0, 2}, which is 0 iff G ⊆ q^⊥; +- **source** (⟨q⟩ → L): 2(1 − dim(⟨q⟩ ∩ G)) ∈ {0, 2}, which is 0 iff q ∈ G. + +(dim G − dim(G ∩ q^⊥) ≤ 1 because q^⊥ is a hyperplane.) + +The route T_{fY}·T_{fX}^{−1} equals F modulo monomials *only if* dim fX + dim fY = n and fX ∩ fY = 0. The source's +saving and the target's saving are therefore tied: un-labelling one side alone leaves a rank-1 mismatch on the pair. + +**Consequence.** "y avoids u_t" is the geodesic condition of the endpoint frames, not an artifact of where the +factor is paid. Moving the rank-1 factor to the parent costs at least d(0, L) − d(0, q^⊥) = 1 per family. Leaving +the interval costs exactly 2. + +**Checks (exact Clifford).** + +- The F2 rank of B = Σqqᵀ equals the tableau child rank on 240 random C-products (n = 4..7). +- Detour excess is 0 on the geodesic set and exactly 2 otherwise: + + | n | geodesic | off-geodesic | + |---|---|---| + | 3 | 20 | 44 | + | 4 | 128 | 408 | + | 5 | 1072 | 4912 | + | 6 | 3740 | 24510 | + + The source and target families give the same counts. +- The rigid pairs at n = 3, 4 are a subset of the complementary pairs. The converse fails: complementary pairs need + not be rigid. +- The gauge descent rank − 1 holds in 9/9 controls. + +**Not reproduced here.** A run on the 112 retained ports of the #523 controller found rank(C_q Z) = rank Z + 1 on +2016/2016 idle children and 2016/2016 stage climbs (no parent object absorbs the gauge). It needs the controller's +generated data-phase files, which this package does not ship, so it is reported, not checked. + +### C.3 Lemma R: complement sinks are legal but pinned + +**Legal (gate 0, `c3_complement_gate0.py`, checked).** For an odd w with w·u = 1, the route T_{w^⊥}·T_{⟨u⟩}^{−1} has +Clifford rank n: + +- for every complement w at n = 3..6, and on 40 seeded samples at n = 9; +- it equals C^{⊗n} after monomial wrappers of the same class as the standard sink, on the tableau and on every basis + column (n ≤ 6); +- non-complements (w·u = 0) give rank n − 2. + +The port price is unchanged: Y: 0 → w^⊥ and X: ⟨u⟩ → F both cost n − 1. The geodesic interval is G ⊆ w^⊥, with +excess exactly 2 outside it. A corrector that the standard sink forbids is exact and correctly priced. So the sink +stays a plain label with a new projection, and the port gate stays a gauge (C_w instead of C_u). + +**Lemma R.** If the sources whose content reaches target t drop-free span u_t^⊥, the only admissible complement sink +of t is w_t = u_t. + +*Proof.* By #446 Theorem A the sink V_t = w_t^⊥ contains u_t^⊥, and V_t is a hyperplane. + +**Pinned (`c3_complement_taint.py`, checked).** The checks run on four complex words: main's #531 word, the width-7 +and four-cold provider words of #569, and the combined-eight-local word of #571. The closure starts every helper at frame 0, the most permissive choice, +so the result holds for every frame assignment of the same scalar word; the words' own entrance frames are not +needed (on the three vendored words the closure with them gives the same result). + +- The most permissive lower closure (helpers enter at 0; every centre may drop to 0 at the cut) has dimension 8 on + 112/112 targets, so w_t = u_t is forced on 112/112. +- The pure drop-free source taint of every target is exactly its Gram-orthogonal neighbourhood: 52 sources, span + u_t^⊥. Phase A contributes nothing to any target. +- Any w ≠ u_t breaks at least 20 of t's 52 lossless corrections (112/112 targets). + +A positive control removes the 4 correction gates of one target. The closure then reports dimension 7 and 2 +admissible sinks, so the instrument sees freedom when it exists. + +On these four words the obstruction is the decoder's lossless pattern, not the endpoint rule. A decoder whose pairing is not symmetric +would be needed, and C.6 shows the E8 pattern admits none at window ≤ 9. + +### C.4 Lemma Q: a degenerate unit is dominated by its quotient (`c4_quotient.py`) + +**Setting.** The ports span W (dim d), with radical rad = W ∩ W^⊥ (dim ρ) and Gram rank r = d − ρ. Write +π: W → W/rad. + +**Lemma Q.** + +- A copy of total j read at a common cut g (g lies in every target sink, so WLOG g ⊆ rad) costs + d(f_j, g) ≥ dim π(f_j). +- Summed over j, this is the quotient unit's reads-at-0 cost, which is ≥ Σ_j rank G[S_j, R_j] (#446 Theorem C at + Gram level). +- Every stage window contains W and is nondegenerate, so h ≥ r + 2ρ. + +Since X is non-increasing in a and in cst (§A.2), X_deg(s) ≤ X(s, r/k, x_quot) ≤ X(s, r/k, x_ThmC) for every s. +Star scope is Gram-level (an in-cap clique inside S_j has a nonsingular diagonal Gram block in every realisation), so +degenerate spans are not outside the ceiling's scope and add no (w, x) points. + +**Checks (exact ranks).** + +- **The paired-cube p = 3 toy:** d 4, ρ 2; copy cost 18 (reads at 0), 16 (optimum over all flags of rad), 12 + (quotient = Theorem C bound); window 6 vs quotient 2. +- **Paired cubes p = 3..12:** only the complex p = 3 cube is degenerate. +- **E8 + an extra vector (bit):** 81 → 72 = quotient 72, window 10 vs 8. +- **E8 + weight-2 isotropic decorations (complex), ρ = 1, 2, 3:** 80 / 88 / 96 → 72 = quotient, windows 11 / 13 / 15 + vs 9. +- **Random radicals:** 0 violations of "cut cost ≥ quotient cost" on 737 seeded instances. +- **Certified X:** each realisation sits below its quotient. + + | unit | quotient | realisation(s) | + |---|---|---| + | bit | 5.1598e-3 | 4.0462e-3 | + | complex (ρ = 1 / 2 / 3) | 4.5356e-3 | 3.6522e-3 / 3.0570e-3 / 2.6286e-3 | + +**Out of scope.** Repeated-label (vector-linear) decoders are a Gram-level class that Lemma Q does not close. + +### C.5 Lemma λ: a phase-frame butterfly needs √−1 (argued; instances checked by `c5_lambda.py`) + +**Lemma λ.** Let K be a directional kernel defined by its direction alone. If P_N(K ⊗ I)P_N^{−1} = K ⊗ I for the +e₁-fixing N, then K = aI + bX. If moreover H_0 = [[1, 1], [1, −1]] satisfies u·H_0 = D₁(aI + bX)D₂ with D₁, D₂ +invertible diagonal and u a unit, then (b/a)² = −1, i.e. the Walsh eigenvalue ratio λ = (a − b)/(a + b) = ±i. + +*Proof.* The first part is a 2 × 2 symbolic computation (T5). For the second, write D₁ = diag(d, d′) and +D₂ = diag(e, e′). Entrywise, d·a·e = u, d·b·e′ = u, d′·b·e = u and d′·a·e′ = −u. Multiplying the first and last +equations gives dd′ee′·a² = −u², and multiplying the middle two gives dd′ee′·b² = u². Hence a² = −b², so a and b are +units and (b/a)² = −1. With b = ±i·a, λ = (1 ∓ i)/(1 ± i) = ∓i. Writing λ needs a + b = a(1 ± i) invertible, and +(1 + i)(1 − i) = 2, so the ring must also make 2 invertible (H_0 itself has determinant −2). ∎ + +**Consequences.** + +- A payload ring in which −1 is not a square (Z[1/2]; Z/M with a prime factor ≡ 3 mod 4) or in which 2 is not + invertible (F2; even M) carries no phase-frame butterfly supplier. +- In a ring with √−1, such as the Fermat ring Z/(2^N + 1) where i = 2^{N/2} is a shift, the ring hosts the identical + C-network with the same paid Fourier-rank histogram and the same b. +- The odd-weight residuals that the phase calculus needs (U/03-motifs.tex:600) force an odd-form unit. For E8 this + means F2 rank 9 and h = 9, which is the structural part of b < c. +- Bit networks have signed-permutation endpoints per role for any payload alphabet. Each two-point butterfly level at + most doubles row support, so a length-8 transform needs ≥ 3 butterfly levels, with the same Fourier-rank mass as the + complex DFT₈. +- The outer already uses shift twiddles (B.3, item 6). + +**Checks (exact, sympy / modular).** + +- **T1–T3:** the product of three H_0 factors and three monomial twiddles equals the bit-reversed DFT₈. Over Z/17 it is + the length-8 NTT with root 2. Row support 8 needs 3 levels. +- **T4:** brute force over Z/M for the 16 odd moduli M ∈ {3, 5, 7, 9, 11, 13, 15, 17, 21, 25, 29, 33, 37, 41, 45, 65}: + solutions exist iff −1 is a square mod M, and λ² = −1 in every solution. +- **T5:** the commutation forces K = aI + bX. +- **T6:** C² = X and H_0 = b·S·C·S in Z/17 with i = 4. +- **T7:** there is no real solution. +- **T8:** weight-2-mod-4 residuals act as translations. + +### C.6 Asymmetric pairing uniqueness at the E8 pattern (`c6_asym.py`) + +**Setting.** A unit is (N over Q, B = W·Uᵀ over F2): + +- window = rank B (the pairing version of Lemma Q); +- a correction N_TS is lossless iff B_TS = 0 (#446 Theorem A, directed); +- β_j = rank B[R_j, A_j] (Theorem C); +- exactness is N∘B = diag. + +The gauge (U, W) ↦ (UP, WP^{−T}) fixes B, so "W ≠ U" means nothing by itself. A symmetric unit-diagonal F2 matrix of +rank r is congruent to I_r. + +**Result (SAT).** At the E8-linear decoder pattern (B_TS = 0 where G_TS ≠ 0, B_TT = 1), gauge-fixed on 8 +pairwise non-orthogonal lines (where the pattern forces B[K, K] = I, so U_K = W_K = [I_8 | 0]): + +- P112 at c = 9: "B ≠ Bᵀ" and "B ≠ B0 = (J + G) mod 2" are UNSAT with U and W both free; with U fixed to the E8 + labels and W free, "B ≠ Bᵀ" is UNSAT too (the "B ≠ B0" question was not run with U fixed); +- P120 at c = 9: the same two questions are UNSAT; +- c = 8: UNSAT, symmetric and non-symmetric (P120), and non-symmetric on P112; +- calibration: c = 9 without the extra constraint is SAT, with B = B0. + +So at window ≤ 9 the pairing is unique and every W ≠ U is a gauge. The UNSAT answers come from CaDiCaL (through +python-sat) without proof logs; the SAT calibration runs show that each encoding is satisfiable where it should be. + +**Off the E8 pattern.** An exact asymmetric P112 unit exists at copy cost 65 (+1) and window 9: N′∘B = diag on all +112 × 112 entries. Two of its targets take sinks w ≠ u and need 28 corrections instead of 52. In this verified unit one extra copy-rank +unit (65 instead of 64) frees exactly two sinks; no lower bound on the price of a freed sink is claimed. A directed +3-cycle toy (B non-symmetric, rank 2, +exact on 343 inputs) shows that the asymmetric class is larger in general. + +### C.7 Per-call descent pricing (`c7_descent_toy.py`, `c7_descent_price.py`) + +**Statement.** A descent of rank r followed by its re-climb costs exactly 2r rank units in the local word. It +therefore costs 2r units of data mass in every call, which is 2r copy-rank units by the deficit identity. There is no +fixed cost to share between uses. + +**Checks.** + +- **Exact toy (n = 5).** One reader reads three cheap terms at point stations ⟨u_a⟩, ⟨u_b⟩, ⟨u_c⟩, and each term's + readers span u_j^⊥. + - Four networks (standard, clones, direct descents, descents through 0) are exact on 224/224 basis columns. + - Every child, including the rank-2 non-comparable ones, has Clifford rank d(A, B). + - Each rank-1 descent costs +2, whether direct or through 0, and a reader at k point stations pays 2(k − 1). +- **Prices on the published profiles** (certified root, hosting held fixed): one rank-1 descent per local word costs + **−5.630% c on #555** (288 stage-replicas) and **−5.646% b on #568** (72 calls); two cost −11.26% / −11.29%. + +**Dominance within the price class (argued).** In the known designs (the complex factory, face and M-copy ledger and +the bit pair-term and star units; this list is a census of those designs, not a theorem), each use of a descent buys at +most one of the following: + +- one target removed from one last-read antichain (≤ |T_t| ≤ 7 private copies); +- two monotone arms for a copy register; +- two fixed pair-split conflicts; +- one supplied retired row. + +That is at most about 7 helpers' work. One rank-1 descent costs −5.65% b on #568, about 40 width-9 complex helpers +at 0.14% b each (§E.1). So within the class where every non-comparable step is one child of rank d(f, g) +paid in every call, a schedule with ≥ 1 paid descent is dominated by the best schedule without one. + +This is price-class dominance, not an impossibility. It does not cover a descent paid once per word. + +### C.8 Split residuals across hosting streams (argued) + +Split a helper residual of width w = a + b over two streams. #451 (chafreaky) shows that the identity +trace(D_{a+b} + I) − trace(D_a + D_b) = q^{2m−a−b}(q^a − 1)(q^b − 1) ≠ 0 is invariant under every invertible linear +change of storage; there is a complex analogue. So no relabelling makes an uncharged split exact. An exact split +needs one of: + +- a cross-term repair (≥ min(a, b) doubly paid coordinates); +- one helper per piece; +- a new hub primitive that prices split routing. + +The "one further route factor per helper selector" of #448 (higherbeing) is the last kind. + +Even uncharged, the gain is small on the current complex frontier. #569 hosts all residual supply and pays the idle +remainder {3: 1200, 7: 48, 48: 1808} (90,720 coordinates; checked in `e2`). #588 uses the same hosting regime, but +its remainder differs and is not reproduced here. φ(r) = r((m/r)^q − 1) is concave, so with free +splitting the best case puts the whole remainder in rank-48 children: 1890·φ(48) = 60.98 against 78.06 today, a +saving of 17.08 D-units. That is **at most +0.67% b**, and it ignores windows and timing. + +Status: argued (concavity bound on #569's reproduced hosting profile; the profile itself is checked in `e2`). + +## D. Design-free helper bounds (`d1_cover_numbers.py`, `d2_coupled_count.py`, `d3_carrier_ledger.py`) + +**Model.** Registers are monotone frame chains: + +- helpers 0 → F; +- sources ⟨u_s⟩ → F; +- targets 0 → u_t^⊥. + +Gates act at a common frame. The only drops are the decoder copies: 9 totals at p^⊥ (bit), 8 rank-8 centres +(complex). The demand is the drop-free source → terminal map. + +**Crossing lemma (argued; #446 Thm A plus the sandwich).** Fix a level d. Every drop-free path s → q crosses level d +exactly once, inside one register's climb a → b, so N = Σ_e α_e β_eᵀ over the level-d crossing events, with +supp β_e ⊆ S(a_e) and supp α_e ⊆ Q(b_e^⊥). Each register crosses each level at most once. Only the extreme levels +bind: at the middle levels the rectangle areas are below the free data crossings. + +**Cover numbers (exact).** + +| side | per-source cover | per-terminal cover | evidence | +|---|---|---|---| +| complex P112 (F2^9) | 2 | 2 | two proper hyperplane sections cover every source's 52 readers (112/112; max section 32; 26 with port-spanned frames only, still 2 sections) | +| bit #555 (Q^8, E7 = the 63 lines ⊥ a source) | 3 | 3 | exhaustive census of the 8821 hyperplane flats of E7: two cover at most 52 of 63 (≥ 11 left), three D6 flats (30 lines each) cover all; on the terminal side at least 6 live sources stay uncovered by any two flats (all 120 terminals) | + +**Floors.** + +| side | sink-only targets | strict (y → y mixing allowed) | shipped | +|---|---|---|---| +| bit | 2·111 − ⌊111/11⌋ = **212** | max(3·111 − 222, 3·120 − 222) = **138** | 439 | +| complex | 112 − ⌊112/20⌋ = **107** (108 with port-spanned frames) | 2·112 − 224 = **0** | 496 (+ 8 centres) | + +**Coupling adds 0 (checked).** The coupled cover model (hop areas through all levels, exact unit rectangle caps +32/32/32/36/32/32/32 for complex d = 2..8, exhaustive for d = 2..5 and by the symmetry d ↔ 10 − d above; end +patterns; bit flat sizes 1, 3, 6, 12, 20, 36, 63 per rank, enumerated in E7, with maximality in E8 from the +root-subsystem chain A1 ⊂ A2 ⊂ A3 ⊂ D4 ⊂ D5 ⊂ E6 ⊂ E7) has integer count optima 212 / 138 / 107 / 0 (HiGHS, zero gap), +identical to the single-cut bounds. The shipped words are feasible in it. With the shipped data ladders held fixed the +floors rise to 222 (bit) and 146 / 123 (complex). + +**Corrections.** + +- **The census of E7's hyperplane flats.** An earlier sampled census found 2258 flats; the exhaustive census has 8821 + (5040 / 2016 / 1008 / 666 / 63 / 28 of sizes 10 / 13 / 16 / 21 / 30 / 36). The sampled set is reproduced (seed 1) and + undercounts the small types; the cover number 3 is unchanged. +- **The "224 carriers = 2 per source" complex floor is a design choice.** #531 gives every source exactly 3 level-2 + crossings (X_s + 2 helpers) into port-spanned 2-dim frames whose section is 20 (3 × 20 = 60 ≥ 52), while two + sections already cover every source. The 224 is a property of the section type, not of the format. +- **Carriers are register-neutral in the calibrated ledger (checked).** The register ledger rebuilt from #531's real + tile objects (168 block-local planes, 168 keys, mate matching 2) reproduces 224 scratch + 168 face copies + 112 M + copies = 504, with B = N2 + K + R − 112 + waste. The carrier stage and the face stage together cost 2·N2 − 112 + + waste for any edge cover. The cover axis therefore only enters through wasted single-variant butterflies: + - rebuilding the same planes from cross-tetrad edges costs +168 (12 per block, exact); + - tetrad edges give waste 0 (CP-SAT over all three splits). + +**What the floors certify.** At most 48% (bit, sink-only, 212/439) / 22% (complex, 107/496 helpers without the 8 +centres) of the shipped helper count is design-free necessary. No single-cut or coupled cover argument closes the helper gap that §A.5 identifies as the whole headroom. + +## E. Complex helper prices and the moment-cost census (`e1_run_census.py`, `e2_helper_prices.py`) + +### E.1 Price per helper by class and width on #569 + +The b gain per deleted helper is measured as follows: + +- the helper is removed in all 72 calls; +- its width returns to the idle remainders; +- hosting is re-solved (the LP relaxation of the whole-owner model; integer CP-SAT spot checks at k = 1, not + reproduced here, agreed with it to < 0.002% b). + +The control reproduces #569's hosting (remainder {3: 1200, 7: 48, 48: 1808}, b = 1.602631811·10⁻³). + +| cell (count) | width | % b per helper, k = 1 (checked) | k = 8 / 14 / whole cell (recorded) | +|---|---|---|---| +| factory scratch (216) | 9 | 0.140 | 0.142 / 0.143 / 0.179 | +| face copy (64) | 9 | 0.134 | 0.140 / 0.141 / 0.151 | +| face-copy entrant (72) | 8 | 0.105 | 0.102 / 0.101 / 0.081 | +| face-copy provider (32) | 7 | 0.075 | 0.069 / 0.062 / 0.050 | +| M-copy entrant (56) | 8 | 0.111 | 0.111 / 0.109 / 0.098 | +| rank-4 pivot (48) | 5 | 0.039 | 0.039 / 0.036 / 0.032 | +| rank-5 pivot (8) | 4 | 0.042 | 0.041 / – / – | + +**Width law.** Price = local fee saved − hosting offset, where the offset is the increase of the hosting LP objective. +The offset depends on width only: cells of equal width have identical LP objective increases (checked). Its share of +the local fee at k = 1 (checked) is: + +| width | 9 | 8 | 7 | 5 | 4 | +|---|---|---|---|---|---| +| offset share, k = 1 | 6.3–6.6% | 17.0–17.9% | 31.5% | 57.4% | 45.4% | + +The share is not monotone in width (w4 sits between w7 and w5). At larger k the w7 share rises to 55% and the w5 share +to 65% (recorded in `data/prices/helper-price-table.json`). One conversion constant links all cells: fee saved minus offset is 25.64–25.66 moment units per 1% b. + +A count-based "0.11% per helper" is therefore about right for the width-8 entrants (0.105–0.111), overprices the +width-7 providers by about 1.5× (0.075) and the rank-4/5 pivots by 2.6–2.8× (0.039–0.042), and underprices the +width-9 scratch and face copies by about 25% (0.134–0.140). Summed k = 1 marginals give: + +| class | share of the marginal helper cost | % b | +|---|---|---| +| factory scratch | 53% | 30.2 | +| face copies | 32% | 18.5 | +| M copies | 15% | 8.4 | + +Full table, including the mixed-class runs: `data/prices/helper-price-table.json` (k > 1 rows recorded). + +### E.2 Moment-cost census by class (checked) + +The F-share of a class is its share of Σφ = D at the word's own root. The all-single-run ceiling is the supplier value +if each register of the class climbed in one child, with hosting proportional. + +**#555** (R = 439; 288 stage-replicas): + +| class | n | runs | mean run | stops/register | F-share | all-single-run ceiling | +|---|---|---|---|---|---|---| +| line-born carriers (0,1,2,…) | 205 | 1120 | 1.46 | 4.46 | 29.5% | +14.75% c | +| cell-born (0,2,…) | 153 | 686 | 1.78 | 3.48 | 21.2% | +9.60% | +| line → quad/D6 keepers and totals | 80 | 349 | 1.83 | 3.36 | 10.7% | +4.35% | +| quad-born | 1 | 4 | 2.00 | 3.00 | 0.1% | +0.05% | +| data x / data y | 111 / 111 | 539 / 213 | 1.44 / 3.65 | – | 14.1% / 10.4% | – | + +Copies take 0.7% and the idle remainder 13.4%. + +**#569** (R = 504; width-7 provider word for all 72 calls): + +| class | n | runs | mean run | stops/register | F-share | all-single-run ceiling | +|---|---|---|---|---|---|---| +| factory scratch | 216 | 1304 | 1.49 | 5.04 | 32.5% | +16.4% b | +| face copies | 168 | 696 | 1.98 | 3.14 | 21.9% | +9.1% | +| M copies | 112 | 504 | 1.43 | 3.50 | 12.4% | +4.9% | + +Data take 28.3%, centres 1.8% and the idle remainder 3.0%. The published global profile is reproduced exactly from +63 width-7 calls, 9 four-cold calls and the remainder. + +## F. What the results imply + +**Cost structure (result).** Under S2 the ceiling is set by the copy charge and the B_K idle structure (A.7); on the +real words the headroom is helper cost, 87–93% of the log-gap (A.5). A change inside the local word is paid in every +call: the local word runs 288 times (stage-replicas) in #555's bit pipeline and 72 times in #568's complex pipeline, +and by the deficit identity each rank unit added per local word lowers D by one per call. On the published profiles one +rank unit per local word costs 2.82% of c (#555) and 2.82% of b (#568): half the checked price of a rank-1 descent +(C.7), and the same size as one copy-rank unit per stage (+2.8% of X at s = 9, A.3). What such a change unlocks (a +shared station, a freed sink, a removed copy, a supplied row) is a gain fixed per word. + +**Break-even.** A change that costs Δ rank units in every local word pays only if its per-word gain exceeds about +2.8·Δ % of the supplier value. On the complex side that is about 20·Δ width-9 helpers (0.14% b each, E.1). The +per-call prices of C.1, C.2, C.6 and C.7 are all of this form: +2 per relaxed target per call, at least 1 per +un-gauged family per call, one copy-rank unit for the two sinks freed in the verified asymmetric unit, and 2r per +rank-r descent per call. + +**Open problems.** + +1. **Per-word enablers.** A mechanism charged once per word or per outer level instead of per call, such as a descent, + gauge change or station hoisted out of the local word. At 1/72 of its per-call price a rank-1 descent would cost + about 0.08% b, roughly half a width-9 helper. The current interface has no such primitive (B.2 rows 1, 3, 24). +2. **A non-star decoder.** The copy charge is the largest scope term (×6.8 at the best s, ×2.8 at s = 9; A.7). On the + E8 pattern the pairing is unique at window ≤ 9 (C.6), and on the four complex words checked the lossless pattern + pins every sink (C.3). Lowering x therefore needs a different unit or decoder; for scale, x = 54/102 (bit) and + 56/104 (complex) would give X* = 8.25·10⁻³ and 6.80·10⁻³ (A.6). +3. **The schedule/ρ freedom.** Any permutation ρ is spec-legal, and one bank pair per invocation is a convention (B.2 + rows 5, 12, 13). The B_K idle terms are worth ×1.15 to ×2.15 (A.7). +4. **New skeletons.** The design-free floors certify at most 48% (bit, 212/439) and 22% (complex, 107/496) of today's + helper counts (D). The other 52% and 78% of the helpers are not shown necessary by any argument here. + +## Files + +- `scripts/`: one check per claim group, plus shared code. + - Shared: `report.py` (PASS/FAIL, paths), `cert.py` (rational-interval ln/expm1, certified roots), `skel.py` + (skeleton slots, variants), `e8units.py` and `minrank_sat.py` (E8 geometry, SAT encodings), `d_geometry.py`, + `e_hosting.py` (the hosting LP and the moment root). + - Driver and step 0: `run_all.py`, `provenance.py`. +- `data/vendor/`: inputs copied from open PRs (`SOURCES.json` gives PR, author, commit, path, git blob id). +- `data/ceiling/`, `data/census/`, `data/toys/`, `data/prices/`: small inputs (#568's recorded idle remainder, the + census anchors, the p = 3 paired-cube instance, #569's call dispatch with its source blob id, the deleted-helper + specs and the recorded price table). +- `DEPENDS.json`: files of main read by the checks, by sha256. +- `MANIFEST.sha256`: every file of the package. + +## Credits + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0. See `NOTICE.md` for the +PRs whose words, pipelines and results are used. diff --git a/research/five-port-quadratic-decoder/sources/pr231-README.md b/research/five-port-quadratic-decoder/sources/pr231-README.md new file mode 100644 index 0000000000..3a13dfd89b --- /dev/null +++ b/research/five-port-quadratic-decoder/sources/pr231-README.md @@ -0,0 +1,56 @@ +# Why the paired-cube decoder does not extend to 4-dimensional (hyper)cubes (no new κ) + +A scoping note on the port dimension of the paired-cube bit word. **No κ is claimed, and nothing existing changes.** + +## The identity being generalized + +The paired-cube bit word (`research/paired-cube-bit/LEMMA.md`) computes the mod-2 decoder identity + + x_T = sum_{c in T} star(c) + sum_{|S cap T| = 1} x_S (mod 2), + +over **ports**: triples taking one coordinate from each of three distinct coordinate pairs. +- `star(c)` is the sum of `x_S` over all ports containing coordinate `c`. These are the shared center sums. +- The overlap-1 sums are what the cube's local circuits, modules and partner pairs compute. + +A natural question is whether moving to k-dimensional cubes, with ports taking one coordinate from each of k pairs, gives a larger deficit. The source count grows like 2^k·C(p,k), while the center loss grows like p². + +## Result + +Consider the star family of decoders for k-ports: + + x_T = sum_{0 order[j] for i in range(n) for j in range(i + 1, n)) + term = (-1)**inversions + for i, j in enumerate(order): + term *= matrix[i][j] + value += term + return value + + +class ProofRelevantControls(unittest.TestCase): + def test_two_eliminations_against_definition(self): + matrices = [[[a, b], [c, d]] for a, b, c, d in product(range(-1, 2), repeat=4)] + rng = random.Random(40) + matrices += [[[rng.randrange(-4, 5) for _ in range(4)] for _ in range(4)] for _ in range(40)] + matrices += [[[0, 1, 0], [0, 0, 1], [1, 0, 0]], [[0, 0], [1, 1]]] + for matrix in matrices: + exact = permutation_determinant(matrix) + self.assertEqual(primary.determinant_mod(matrix), exact % primary.PRIME) + self.assertEqual(second.bareiss(matrix), exact) + self.assertEqual(second.bareiss(matrix, second.MODULUS), exact % second.MODULUS) + + def test_all_named_controls(self): + witness = json.loads((HERE / 'WITNESSES.json').read_text())['witnesses'] + self.assertEqual(len(primary.negative_controls(witness)), 9) + + def test_distinct_valid_labels_can_make_a_singular_minor(self): + # Different ports can have identical pairings on a restricted column + # set. Exercise elimination, not just duplicate-label rejection. + ports = [sum(1 << (2*i+b) for i, b in enumerate(bits)) for bits in product((0, 1), repeat=5)] + found = False + for a, b in zip(ports, ports[1:]): + matrix = [[primary.gram(x, y) for y in ports[:2]] for x in (a, b)] + if permutation_determinant(matrix) == 0: + self.assertEqual(primary.determinant_mod(matrix), 0) + found = True + break + self.assertTrue(found) + + def test_missing_obligation_rejected(self): + with tempfile.TemporaryDirectory(prefix='five port omission ') as tmp: + shutil.copytree(HERE, Path(tmp) / 'package') + root = Path(tmp) / 'package' + data = json.loads((root / 'WITNESSES.json').read_text()) + data['witnesses'] = data['witnesses'][:-1] + (root / 'WITNESSES.json').write_text(json.dumps(data)) + with patch.object(primary, 'HERE', root): + with self.assertRaisesRegex(ValueError, '17 obligations'): + primary.verify() + + def test_changed_source_rejected(self): + with tempfile.TemporaryDirectory(prefix='five port source ') as tmp: + shutil.copytree(HERE, Path(tmp) / 'package') + root = Path(tmp) / 'package' + source = root / 'sources/pr446-PROOF.md' + source.write_bytes(source.read_bytes() + b'\nchanged source\n') + with patch.object(primary, 'HERE', root): + with self.assertRaisesRegex(ValueError, 'immutable source hash'): + primary.check_sources() + + def test_valid_scalar_geometry_failure_is_visible(self): + # An overlap-three correction is present in the true XOR identity, + # but the predecessor's affine overlap kernel j-1 cannot route it. + left = frozenset((0, 2, 4, 6, 8)) + right = frozenset((0, 2, 4, 7, 9)) + common = len(left & right) + self.assertEqual((common + int(common in (1, 3))) % 2, 0) + self.assertEqual(second.feature_entry(left, right), 0) + self.assertNotEqual(common - 1, 0) + + +if __name__ == '__main__': + unittest.main(verbosity=2) diff --git a/research/five-port-quadratic-decoder/verify.py b/research/five-port-quadratic-decoder/verify.py new file mode 100644 index 0000000000..4c1f044fdb --- /dev/null +++ b/research/five-port-quadratic-decoder/verify.py @@ -0,0 +1,250 @@ +#!/usr/bin/env python3 +"""Check literal rational-rank witnesses and the optimistic format ceiling. + +Integer minors modulo a checked prime certify rational rank LOWER bounds. +No floating-point calculation, optimizer or discovery code is used. +Copyright 2026 Ross Richardson. Apache-2.0. Substantial OpenAI Codex assistance. +""" +from fractions import Fraction as Q +from itertools import combinations, product +from math import comb, isqrt +from pathlib import Path +import argparse +import copy +import hashlib +import json + +HERE = Path(__file__).resolve().parent +BASE = '47481c89fd30a43f8f882eb4b391e89c29273fd0' +PRIME = 65521 +LOG_LOWER = Q(549, 500) +CEILING = Q(125, 76433) +SELECTED = Q(1661957774647029, 10**18) +CORRECTOR = dict(zip(range(5, 14), (15, 50, 83, 111, 143, 179, 219, 263, 311))) +STAR = dict(zip(range(5, 13), (11, 35, 60, 84, 112, 144, 170, 210))) +SOURCE_NAMES = {'sources/pr231-README.md', 'sources/format-axioms-README.md', + 'sources/selected-result-base.json', 'sources/pr446-PROOF.md'} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def gram(a, b): + common = (a & b).bit_count() + return 2 * (common - 1) * (common - 3) + + +def determinant_mod(matrix, prime=PRIME): + """Ordinary row elimination; the committed residue must be nonzero.""" + n = len(matrix) + require(n > 0 and all(len(row) == n for row in matrix), 'square nonempty minor') + rows = [[x % prime for x in row] for row in matrix] + determinant = 1 + for col in range(n): + pivot = next((i for i in range(col, n) if rows[i][col]), None) + if pivot is None: + return 0 + if pivot != col: + rows[pivot], rows[col] = rows[col], rows[pivot] + determinant = -determinant + entry = rows[col][col] + determinant = determinant * entry % prime + inverse = pow(entry, -1, prime) + for i in range(col + 1, n): + multiplier = rows[i][col] * inverse % prime + if multiplier: + rows[i][col] = 0 + for j in range(col + 1, n): + rows[i][j] = (rows[i][j] - multiplier * rows[col][j]) % prime + return determinant % prime + + +def valid_port(mask, p): + return (type(mask) is int and 0 <= mask < (1 << (2 * p)) and mask.bit_count() == 5 + and all(((mask >> (2 * i)) & 3) != 3 for i in range(p))) + + +def check_witness(w): + require(type(w.get('p')) is int, 'integer pair count') + p, kind = w['p'], w.get('kind') + require(kind in ('corrector', 'star'), 'known witness kind') + expected = CORRECTOR if kind == 'corrector' else STAR + require(p in expected and w.get('rank_lower') == expected[p], 'rank obligation') + n = expected[p] + canonical_target = sum(1 << (2 * i) for i in range(5)) + require(w.get('target') == (canonical_target if kind == 'corrector' else 1), 'target binding') + for side in ('rows', 'columns'): + labels = w.get(side, []) + require(len(labels) == n and len(set(labels)) == n, 'distinct minor labels') + for mask in labels: + require(valid_port(mask, p), 'signed five-port domain') + if kind == 'corrector': + require((mask & canonical_target).bit_count() in (1, 3), 'corrector support') + else: + require(bool(mask & 1), 'coordinate-star support') + matrix = [[gram(a, b) for b in w['columns']] for a in w['rows']] + determinant = determinant_mod(matrix) + require(determinant != 0, 'nonsingular rational-rank witness') + require(determinant == w.get('determinant_mod_prime'), 'determinant receipt') + return dict(p=p, kind=kind, rank_lower=n, determinant_mod_prime=determinant) + + +def check_sources(): + manifest = json.loads((HERE / 'SOURCES.json').read_text()) + require(manifest['base_commit'] == BASE, 'base pin') + require(len(manifest['files']) == 4, 'source count') + require({r['path'] for r in manifest['files']} == SOURCE_NAMES, 'source inventory') + hashes = {} + for row in manifest['files']: + raw = (HERE / row['path']).read_bytes() + digest = hashlib.sha256(raw).hexdigest() + blob = hashlib.sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() + require(digest == row['sha256'] and blob == row['git_blob_sha1'], 'immutable source hash') + require(row['commit'] == ('309482849b6ddf34db998f53612d34c19f6e3233' + if row['path'] == 'sources/pr446-PROOF.md' else BASE), 'source commit') + hashes[row['path']] = digest + selected = json.loads((HERE / 'sources/selected-result-base.json').read_text()) + require(Q(selected['kappa']) == SELECTED, 'frozen selected value') + return hashes + + +def algebra_checks(): + # The XOR decoder coefficient, checked on all overlap types and on every + # pair of literal ports for p=5,6. It is not a full supplier replay. + for j in range(6): + require((j + int(j in (1, 3))) % 2 == int(j == 5), 'XOR decoder identity') + require(6 - 6 * j + 4 * comb(j, 2) == 2 * (j - 1) * (j - 3), 'feature pairing') + pairs = 0 + for p in (5, 6): + ports = [sum(1 << (2 * i + bit) for i, bit in zip(indices, bits)) + for indices in combinations(range(p), 5) + for bits in product(range(2), repeat=5)] + for a in ports: + for b in ports: + j = (a & b).bit_count() + require((j + int(j in (1, 3))) % 2 == int(a == b), 'literal decoder') + if j in (1, 3): + require(gram(a, b) == 0, 'lossless correction') + pairs += 1 + even = [bits for bits in product(range(2), repeat=5) if sum(bits) % 2 == 0] + labels = [sum(1 << (2 * i + b) for i, b in enumerate(bits)) for bits in even] + require(len(labels) == 16 and 16 > 6, 'linear-label dimension obstruction') + for i, a in enumerate(labels): + for j, b in enumerate(labels): + require(gram(a, b) == (16 if i == j else 0), 'parity clique') + # ln(3) = 2 atanh(1/2). Every omitted summand is strictly positive. + partial = check_log_lower(LOG_LOWER) + return dict(literal_decoder_pairs=pairs, parity_clique_size=16, + affine_label_span_upper=6, logarithm_partial_sum=str(partial), + logarithm_lower=str(LOG_LOWER)) + + +def check_log_lower(proposed): + partial = sum((Q(2, (2 * i + 1) * 2**(2 * i + 1)) for i in range(6)), Q()) + require(partial > proposed > 0, 'certified logarithm lower bound') + return partial + + +def price(p, a, star_rank): + require(p in STAR and a == CORRECTOR[p] and star_rank == STAR[p], 'price rank bindings') + v = 32 * comb(p, 5) + c = 2 * p * star_rank + if c >= v: + return dict(p=p, ports=v, active_rank_lower=a, star_rank_lower=star_rank, + copy_charge_lower=c, positive_deficit_possible=False) + upper = (1 - Q(c, v)) / (2 * a * LOG_LOWER) + require(upper <= CEILING, 'finite supplier ceiling') + return dict(p=p, ports=v, active_rank_lower=a, star_rank_lower=star_rank, + copy_charge_lower=c, positive_deficit_possible=True, saving_upper=str(upper)) + + +def expect_rejection(fn, description): + try: + fn() + except (ValueError, KeyError, TypeError): + return description + raise ValueError('negative control was accepted: ' + description) + + +def negative_controls(witnesses): + original = next(w for w in witnesses if w['p'] == 5 and w['kind'] == 'corrector') + controls = [] + bad = copy.deepcopy(original) + bad['rows'][1] = bad['rows'][0] + controls.append(expect_rejection(lambda: check_witness(bad), 'duplicate minor row')) + bad = copy.deepcopy(original) + bad['rows'][0] = bad['target'] + controls.append(expect_rejection(lambda: check_witness(bad), 'self substituted for corrector')) + bad = copy.deepcopy(original) + bad['determinant_mod_prime'] = 0 + controls.append(expect_rejection(lambda: check_witness(bad), 'false determinant residue')) + bad = copy.deepcopy(original) + bad['rows'][0] = 31 # contains both coordinates of a pair + controls.append(expect_rejection(lambda: check_witness(bad), 'invalid paired-port label')) + star = copy.deepcopy(next(w for w in witnesses if w['p'] == 5 and w['kind'] == 'star')) + star['rows'][0] ^= 3 # move coordinate 0 to its mate + controls.append(expect_rejection(lambda: check_witness(star), 'reader outside copied star')) + controls.append(expect_rejection(lambda: price(10, 179, 143), 'invoice rank differs from witness')) + controls.append(expect_rejection(lambda: check_log_lower(Q(1099, 1000)), + 'unproved logarithm bound')) + # A true scalar identity need not have valid geometry: the old affine + # kernel j-1 fails on a required overlap-three correction. + require(3 - 1 != 0, 'linear-kernel geometric failure control') + controls.append('linear kernel rejected at overlap three') + # A singular matrix reaches the actual elimination failure, independently + # of the label uniqueness checks above. + require(determinant_mod([[16, 16], [16, 16]]) == 0, 'singular minor detection') + controls.append('singular matrix detected by elimination') + return controls + + +def verify(): + require(PRIME > 2 and all(PRIME % d for d in range(2, isqrt(PRIME) + 1)), 'prime modulus') + sources = check_sources() + raw = (HERE / 'WITNESSES.json').read_bytes() + data = json.loads(raw) + require(data['schema'] == 'five-port-quadratic-rank-witnesses-v1', 'witness schema') + require(data['seed'] == 40 and data['prime'] == PRIME, 'seed and prime') + require(data['kernel_coefficients'] == [6, -8, 2], 'kernel coefficients') + expected = {(p, 'corrector') for p in CORRECTOR} | {(p, 'star') for p in STAR} + require(len(data['witnesses']) == len(expected), 'all 17 obligations present') + require({(w['p'], w['kind']) for w in data['witnesses']} == expected, 'obligation inventory') + ranks = [check_witness(w) for w in data['witnesses']] + algebra = algebra_checks() + bounds = [price(p, CORRECTOR[p], STAR[p]) for p in STAR] + # Every target at p>=13 contains an isometric copy of the p=13 witness. + # Grant copy and all other costs zero in the tail. + tail = 1 / (2 * CORRECTOR[13] * LOG_LOWER) + require(tail < CEILING < SELECTED, 'all-p tail and frozen selected comparison') + require(max(Q(r['saving_upper']) for r in bounds if r['positive_deficit_possible']) == CEILING, + 'maximum of the stated coarse bounds') + controls = negative_controls(data['witnesses']) + return dict(schema='five-port-quadratic-certificate-v1', base_commit=BASE, + witness_sha256=hashlib.sha256(raw).hexdigest(), source_sha256=sources, + prime=PRIME, ranks=ranks, algebra=algebra, finite_bounds=bounds, + all_p_ge_13_tail_upper=str(tail), supplier_saving_strict_upper=str(CEILING), + selected_kappa_at_base=str(SELECTED), strict_gap=str(SELECTED - CEILING), + stage_scope='every integer s >= 3 under PROOF.md accounting premises', + negative_controls=controls, new_kappa_claim=False) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-certificate', type=Path, + help='write a new receipt with exclusive creation; do not compare committed receipt') + args = parser.parse_args() + result = verify() + encoded = json.dumps(result, indent=2) + '\n' + if args.write_certificate: + with args.write_certificate.open('x') as handle: + handle.write(encoded) + else: + require(json.loads((HERE / 'CERTIFICATE.json').read_text()) == result, 'certificate equality') + print('PASS_FIVE_PORT_QUADRATIC_DECODER witnesses=17 ' + 'ceiling=125/76433 tail=250/170739 controls=9 no_new_kappa') + + +if __name__ == '__main__': + main()