From 09022f8e47bf6b635ca09b31e9749be38645f25a Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 15 Oct 2026 00:06:10 +0100 Subject: [PATCH 1/2] test(research): audit anti-Fano rank-three completions --- .../CONFIGURATION.json | 1 + .../antifano-subspace-audit/EXPECTED.json | 167 +++++++++++ research/antifano-subspace-audit/LICENSE | 201 +++++++++++++ research/antifano-subspace-audit/README.md | 184 ++++++++++++ research/antifano-subspace-audit/SOURCES.json | 55 ++++ research/antifano-subspace-audit/TASK.json | 100 +++++++ .../UPSTREAM-NOTICE.md | 23 ++ research/antifano-subspace-audit/VERIFY.json | 29 ++ research/antifano-subspace-audit/ruff.toml | 12 + .../antifano-subspace-audit/test_verify.py | 135 +++++++++ research/antifano-subspace-audit/verify.py | 267 ++++++++++++++++++ 11 files changed, 1174 insertions(+) create mode 100644 research/antifano-subspace-audit/CONFIGURATION.json create mode 100644 research/antifano-subspace-audit/EXPECTED.json create mode 100644 research/antifano-subspace-audit/LICENSE create mode 100644 research/antifano-subspace-audit/README.md create mode 100644 research/antifano-subspace-audit/SOURCES.json create mode 100644 research/antifano-subspace-audit/TASK.json create mode 100644 research/antifano-subspace-audit/UPSTREAM-NOTICE.md create mode 100644 research/antifano-subspace-audit/VERIFY.json create mode 100644 research/antifano-subspace-audit/ruff.toml create mode 100644 research/antifano-subspace-audit/test_verify.py create mode 100644 research/antifano-subspace-audit/verify.py diff --git a/research/antifano-subspace-audit/CONFIGURATION.json b/research/antifano-subspace-audit/CONFIGURATION.json new file mode 100644 index 0000000000..ae11f01fab --- /dev/null +++ b/research/antifano-subspace-audit/CONFIGURATION.json @@ -0,0 +1 @@ +[[[1, -1, -1], [0, 1, 1]], [[1, -1, -1], [1, -1, 0]], [[1, -1, -1], [1, 0, -1]], [[1, -1, 1], [0, 1, -1]], [[1, -1, 1], [1, -1, 0]], [[1, -1, 1], [1, 0, 1]], [[1, 1, -1], [0, 1, -1]], [[1, 1, -1], [1, 0, -1]], [[1, 1, -1], [1, 1, 0]], [[1, 1, 1], [0, 1, 1]], [[1, 1, 1], [1, 0, 1]], [[1, 1, 1], [1, 1, 0]]] \ No newline at end of file diff --git a/research/antifano-subspace-audit/EXPECTED.json b/research/antifano-subspace-audit/EXPECTED.json new file mode 100644 index 0000000000..e34fc40daa --- /dev/null +++ b/research/antifano-subspace-audit/EXPECTED.json @@ -0,0 +1,167 @@ +{ + "lines": 12, + "incidences": 72, + "blocks": [ + { + "coordinate": 0, + "columns": [ + 1, + 2, + 4, + 5, + 7, + 8, + 10, + 11 + ], + "triangular_minor": [ + 1, + 4, + 2 + ], + "column_trials": 262144, + "row_trials": 4096, + "completions": 1, + "unique_columns": [ + 1410, + 2100, + 3216, + 294, + 3216, + 294, + 1410, + 2100 + ], + "class_space_ranks": [ + 3, + 3 + ], + "zero_rows": [ + 0, + 3, + 6, + 9 + ], + "projection_identity_minor": [ + 0, + 9 + ] + }, + { + "coordinate": 1, + "columns": [ + 0, + 1, + 3, + 4, + 6, + 8, + 9, + 11 + ], + "triangular_minor": [ + 0, + 9, + 1 + ], + "column_trials": 262144, + "row_trials": 4096, + "completions": 1, + "unique_columns": [ + 281, + 2626, + 2059, + 848, + 2626, + 281, + 848, + 2059 + ], + "class_space_ranks": [ + 3, + 3 + ], + "zero_rows": [ + 2, + 5, + 7, + 10 + ], + "projection_identity_minor": [ + 2, + 7 + ] + }, + { + "coordinate": 2, + "columns": [ + 0, + 2, + 3, + 5, + 6, + 7, + 9, + 10 + ], + "triangular_minor": [ + 0, + 9, + 2 + ], + "column_trials": 262144, + "row_trials": 4096, + "completions": 1, + "unique_columns": [ + 225, + 1548, + 1548, + 225, + 1093, + 680, + 680, + 1093 + ], + "class_space_ranks": [ + 3, + 3 + ], + "zero_rows": [ + 1, + 4, + 8, + 11 + ], + "projection_identity_minor": [ + 1, + 4 + ] + } + ], + "lower_bound": 12, + "rank_three_case_floor": 13, + "upper_rows": [ + 9, + 258, + 36, + 9, + 2064, + 36, + 576, + 1152, + 258, + 576, + 1152, + 2064 + ], + "upper_ranks": [ + 4, + 4, + 4 + ], + "full_pattern_ranks": [ + 8, + 8, + 8 + ] +} diff --git a/research/antifano-subspace-audit/LICENSE b/research/antifano-subspace-audit/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/antifano-subspace-audit/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/antifano-subspace-audit/README.md b/research/antifano-subspace-audit/README.md new file mode 100644 index 0000000000..06fd7c29a0 --- /dev/null +++ b/research/antifano-subspace-audit/README.md @@ -0,0 +1,184 @@ +# Independent subspace audit of the anti-Fano decoder bound + +The minimum raw pairing cost of the pinned 12-line configuration is **12**. +This independently corroborates DreamingOfClouds' PR2111, Theorem T, and PR2162, +Theorem T'. It does not supply a new decoder, supplier or multiplication bound. + +The new check replaces PR2111's SAT-based uniqueness step with two complete +binary-subspace censuses. It imports no predecessor code and uses no external solver, +finite-field extension, floating point or jet certificate. The exchange argument +below is credited to PR2111, not claimed as new. + +## Model and result + +For the twelve point/line pairs `(p(t), q(t))` in +[CONFIGURATION.json](CONFIGURATION.json), an admissible binary matrix `B` has +unit diagonal. An off-diagonal entry can be one only if `p(t) dot q(s) = 0`. +There are 72 independently optional entries, hence `2^72` admissible matrices. +All points have full coordinate support. Let `C_j` contain the four columns +whose `q` has coordinate `j` equal to zero, and let `A_j` be its eight-column +complement. The raw cost is + +`rank_F2 B[:, A_0] + rank_F2 B[:, A_1] + rank_F2 B[:, A_2]`. + +For each block the audit establishes: + +| Missing coordinate | Universal triangular minor | Column-basis assignments | Row-basis assignments | Rank-3 completions | +| --- | --- | ---: | ---: | ---: | +| 0 | 1, 4, 2 | 262,144 | 4,096 | 1 | +| 1 | 0, 9, 1 | 262,144 | 4,096 | 1 | +| 2 | 0, 9, 2 | 262,144 | 4,096 | 1 | + +Indices start at zero and retain the predecessor's ordering. Both orientations +recover exactly the same unique completion. Its two constituent class column +spaces each have dimension three, their union has dimension three, and every +row in `C_j` vanishes. [EXPECTED.json](EXPECTED.json) records each completion +as twelve-bit column vectors, together with the minors and the upper witness. + +**The bound is a minimum over B, not equality for every B.** The full incidence +matrix has block ranks `(8,8,8)` and cost 24. A recorded admissible matrix has +ranks `(4,4,4)` and attains 12. + +## Why the census is complete + +Each displayed principal minor is unit upper triangular for every admissible +matrix. The verifier checks that all entries below its diagonal are forbidden. +Its three columns and three rows are therefore independent, so every block has +rank at least three. + +Fix one block. Each column has six optional bits and its mandatory diagonal +bit. There are exactly `64^3` assignments to the three displayed basis columns. +For a block of rank at most three, every other column must lie in their +eight-element span. The column census intersects that span with each remaining +column's allowed affine set. The product of the intersection sizes counts all +completions. Different basis assignments give different matrices, and the +remaining columns have independent entry constraints. Thus no rank-three +completion is omitted or counted twice. + +The separate transpose implementation reconstructs the entry constraints directly +from the rational configuration, without calling the column-option builder. +Each selected row has four optional bits, giving `16^3` basis assignments. +It constructs row spans by set doubling and intersects them with independently +enumerated eight-bit row alphabets. It again counts all completions and agrees +entrywise with the column result. + +## The credited exchange argument + +Write `S_k` for the span of the columns in `C_k`. If no block has rank three, +all three have rank at least four and the cost is at least twelve. + +Otherwise, suppose block `j` has rank three. The unique completion gives +`S_k = S_l = U` of dimension three for the other two classes, and `U` vanishes +on the four rows `C_j`. The projection of `S_j` onto those rows has dimension +at least two. The verifier supplies a universal two-by-two principal identity +minor in `B[C_j,C_j]`, respectively `(0,9)`, `(2,7)` and `(1,4)`. + +Because projection kills `U`, +`dim(S_j + U) >= dim U + dim projection(S_j) >= 3 + 2 = 5`. +Both other blocks have column space `S_j + U`. Their ranks are at least five, +so this case costs at least `3 + 5 + 5 = 13`. In either case the cost is at +least twelve. The explicit cost-twelve matrix proves sharpness. + +This is a finite computer-assisted proof of the pinned configuration's minimum. +It replaces one computational step of an existing proof, not its mathematical +claim or its broader open three-total conjecture. + +## Reproduce + +Standard library only, from the repository root: + +```sh +python3.12 scripts/research_package.py --package research/antifano-subspace-audit +python3.12 -I -O -B research/antifano-subspace-audit/verify.py +python3.12 -O -B -m unittest discover -s research/antifano-subspace-audit -p 'test_*.py' +``` + +Expected verifier line: + +```text +PASS_ANTIFANO_SUBSPACE_AUDIT minimum=12 blocks=3 column_trials=786432 row_trials=12288 unique_rank3=1,1,1 no_new_kappa +``` + +The ten test groups include all 4,096 three-by-four binary matrices against a +separate dense elimination oracle, a 64-completion census fixture, an impossible +completion fixture, and controls for a missing diagonal, forbidden entry, +incorrect cost witness, wrong source bytes, dependent basis, false uniqueness, +truncated census count, corrupted completion, false lower bound and capacity +exhaustion. Checks remain active under `-O`. + +The direct verifier also works from a source export without Git or network. +The registered metadata checker uses Git for historical provenance. Exact heads, +source hashes, scope change, overlap coverage and environment are in +[TASK.json](TASK.json) and [SOURCES.json](SOURCES.json). + +Ruff 0.17.0 also passes with all diagnostics enabled under the package's scoped +configuration. Its exclusions retain standard-library unittest, standalone +scripts, literal mathematical dimensions and the documented CLI output: + +```sh +ruff check --config research/antifano-subspace-audit/ruff.toml research/antifano-subspace-audit/ +``` + +## Implementation bounds + +All mathematical loops have fixed finite bounds. The largest is `64^3` basis +assignments per block, each testing at most five columns against eight vectors. +The transpose uses `16^3` assignments, each testing at most twelve rows. +No search state accumulates across assignments. Configuration and receipt reads +are capped at 4,096 and 16,384 bytes. Every function is shorter than 40 lines. + +Python necessarily allocates integers and collections during the census. This +is a managed-runtime deviation from allocation-free steady operation, confined +to this fixed instance. Column alphabets contain at most `8*64` integers; row +alphabets at most `12*16`; each span contains eight. CPython 3.12 tracemalloc +measured a 240,520-byte peak during one audit after configuration parsing. This +is an observation, not a universal process-memory bound. Any variable-size +extension must derive new input, loop and memory caps before reuse. + +The unittest runner uses framework dispatch to ten named test methods. This is +the only test-framework indirect-call deviation; no user-supplied code or solver +is loaded. Discovery is confined to this package. A future plugin or broader +discovery mechanism would need a new review. The single `FBT001` suppression +marks an assertion predicate, not a mode-selection flag; all acceptance checks +remain ordinary exceptions under `-O`. + +## Limits + +This does not enumerate the 217 optimal matrices, prove the general `T=3` +conjecture, reproduce either predecessor's entire suite, or formalize the +exchange argument in Lean. No physical decoder, hosting, precision, all-size +compiler, outer assembly or selected cold replay is checked. The selected +conditional exponent remains unchanged. + +## Open next questions + +- Can the unique rank-three completion be derived without enumeration? Start + with the displayed triangular minors and the eight-element spans, then + eliminate the remaining affine constraints by hand. This would remove the + computational step, but a short symbolic argument is not established here. +- Can the projection/exchange certificate extend to other three-total + configurations? First inspect the rank-three blocks of a second explicit + configuration. The present zero-row and equal-class-space properties are + verified only for this anti-Fano object and must not be assumed generally. + +The structured questions and their blockers are in TASK.json. + +## Credit and scope selection + +DreamingOfClouds supplied the configuration, the exchange proof and the SAT +uniqueness result in [PR2111](https://github.com/CrocSwap/integer-mult-bounds/pull/2111), +and the separate jet proof in +[PR2162](https://github.com/CrocSwap/integer-mult-bounds/pull/2162). +This responds to item 1 of the +[independent-check handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18934590). +The model and prior rank arguments retain the PR446/595/1590 lineage. +CONFIGURATION.json is an unchanged copy of PR2162's `data/tied_min.json`, also +byte-identical in PR2111. LICENSE and UPSTREAM-NOTICE.md retain its Apache-2.0 +terms and source notice. No predecessor implementation is imported. + +The original draw was `bit-helper-contract`, priority revision 4. Its basic +H2/K replacement was already covered by PR1194/1782/1805 and related packages; +the proposed full-profile recount was already covered by PR1421. This is an +explicitly changed scope to an independent decoder-floor audit, not progress on +the helper contract. The binary pairing-cost check addresses a live verification +request on the binding complex side. Nick Petalas prepared this audit. diff --git a/research/antifano-subspace-audit/SOURCES.json b/research/antifano-subspace-audit/SOURCES.json new file mode 100644 index 0000000000..9db946ed6e --- /dev/null +++ b/research/antifano-subspace-audit/SOURCES.json @@ -0,0 +1,55 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "predecessors": [ + { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/2111", + "head": "98da76c2839ba38538b510420dec54546ccabf0b", + "author": "DreamingOfClouds", + "scope": "Configuration, Theorem T and credited exchange argument. The SAT uniqueness implementation is not imported." + }, + { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/2162", + "head": "113a718265c62aec301c5695f4bfb9c421bef7ab", + "author": "DreamingOfClouds", + "scope": "Source of the unchanged vendored configuration, license and notice; Theorem T prime is an alternate proof, not replayed here." + } + ], + "vendored_files": [ + { + "path": "CONFIGURATION.json", + "source_commit": "113a718265c62aec301c5695f4bfb9c421bef7ab", + "source_path": "research/char2-jets/data/tied_min.json", + "git_blob": "ae11f01fab8b32b07a782ec968186a0af98c8f32", + "sha256": "670ed90924b601ade22f0d4adaff46d1667e5449326a0f7ba7b88dd8f5906f93", + "also_identical_at": "98da76c2839ba38538b510420dec54546ccabf0b:research/three-total-decoders/data/tied_min.json", + "verification": "verify.py checks the SHA256 before parsing." + }, + { + "path": "LICENSE", + "source_commit": "113a718265c62aec301c5695f4bfb9c421bef7ab", + "source_path": "research/char2-jets/LICENSE", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "path": "UPSTREAM-NOTICE.md", + "source_commit": "113a718265c62aec301c5695f4bfb9c421bef7ab", + "source_path": "research/char2-jets/NOTICE.md", + "sha256": "2eeab89221c6ebc3e228d55aa279992b028ce19bfa7732ff808a601f81dd146a" + } + ], + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + } + ] +} diff --git a/research/antifano-subspace-audit/TASK.json b/research/antifano-subspace-audit/TASK.json new file mode 100644 index 0000000000..1137e957e4 --- /dev/null +++ b/research/antifano-subspace-audit/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "Independently certify the unique rank-three block completions and the sharp minimum raw pairing cost twelve of PR2111/2162's pinned anti-Fano configuration, using binary row/column subspace enumeration instead of SAT or jets.", + "scope_change_reason": "The drawn H2/K question is already covered by PR1194/1782/1805 and related work. A possible selected-bit profile recount was also already covered by PR1421. Take the explicit unreserved independent-check request in Discussion1166 comment18934590, item1, without another task draw. This is a side result relative to the helper-contract card, not a replacement interface.", + "bottleneck_link": "A source-bound independent audit of an existing three-total decoder floor checks one proposed low-rank route on the binding complex side. It changes no supplier, paid profile or selected exponent.", + "budget_minutes": 60, + "stop_rule": "Stop after this one twelve-line configuration. A census disagreement falsifies the proposed corroboration and must be reported rather than weakening uniqueness. Do not enumerate all 2^72 matrices or claim the general T=3 conjecture.", + "outcome": "completed", + "evidence": "EXPECTED.json; verify.py reconstructs all three unique completions in two orientations and validates an admissible (4,4,4) witness. test_verify.py supplies dense rank, multiple-completion, impossible-completion and corruption controls. README gives completeness and the credited projection/exchange proof.", + "author": "Nick Petalas", + "ai_assistance": "Substantial AI assistance with implementation and checking. Author-checked evidence, not independent human review.", + "selection": { + "seed": "d10ac7d67313ef461e1833b43220df53", + "track": "bit-mechanisms", + "scope_key": "bfb61f829a81535adeae", + "refined_scope_key": "antifano-tied-min-dual-subspace-audit", + "first_working_example": "python3 -B research/r439-bsection-stars-seed01/verify.py", + "first_working_result": "PASS_R439_BSECTION_STARS blocks=10 gates=388->254 ADDs=11783->11515->11500 guard_rejections=24->0 columns=661 controls=8 no_new_kappa" + }, + "coordination": { + "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18934590", + "claim_posted": false, + "reason": "The invoked engineering-mode skill forbids human-directed external messages. Read-only overlap and board checks were performed; communication text remains a local draft. No retrospective reservation is claimed." + }, + "freshness": { + "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "checked_at_utc": "2026-10-14T23:02:26Z", + "overlap": "Final find_overlap.py refresh for anti-Fano, tied_min and subspace audit; complete pagination over 435 open PRs and 876 discussion records, fetched 23:01:00Z and 23:02:25Z. Only source PR2111, source PR2162, the independent-check request and this local package matched. No code diffs or arbitrary nested files were searched; this is not proof of novelty. Canonical main and both predecessor heads were unchanged.", + "predecessor_heads_rechecked": true + }, + "environment": { + "python": "CPython 3.12.15; additional direct checks with CPython 3.13.5", + "platform": "Linux 6.6.87.2-microsoft-standard-WSL2 x86_64", + "dependencies": "Python standard library only" + }, + "verification": { + "registered_python312": "PASS_REGISTERED_RESEARCH_PACKAGE research/antifano-subspace-audit outcome=completed", + "tests": "10 package behavior groups pass normally and with -O; 65 test_research_*.py workflow tests pass.", + "diagnostics": "Ruff 0.17.0 ALL checks pass under ruff.toml. Python 3.12 validation ran with -X dev -W error. No Lean build or static type checker was run.", + "source_export": "Standalone -I -O replay passes outside Git. CLI rejects a changed configuration and a false lower-bound receipt.", + "counting_mutation": "In a temporary copy, replacing the product of completion counts with one per feasible basis leaves this unique-completion baseline unchanged but is rejected by the 64-completion test fixture.", + "memory_observation": "CPython 3.12 tracemalloc peak 240520 bytes during audit after configuration parsing; not a universal RSS bound.", + "review": "Local source and mathematical review only. No independent human review, predecessor full replay or selected cold replay is claimed." + }, + "open_questions": [ + { + "question": "Can the unique rank-three completion be proved without enumeration?", + "why_it_matters": "This would remove the computer-assisted uniqueness step from the credited exchange argument.", + "first_step": "Use the listed triangular minors as pivots and simplify the affine membership constraints on each eight-element span.", + "blocked_by": "No short symbolic derivation is supplied; the present proof uses two complete finite censuses." + }, + { + "question": "Does another three-total configuration admit the same zero-row projection/exchange certificate?", + "why_it_matters": "A second instance could identify hypotheses for a reusable decoder-floor lemma instead of a configuration-specific proof.", + "first_step": "Choose a second explicit configuration and inspect its rank-three block completions for equal class spaces and vanishing omitted-class rows.", + "blocked_by": "Those properties have only been established for this pinned anti-Fano configuration; no universal implication is claimed." + } + ] +} diff --git a/research/antifano-subspace-audit/UPSTREAM-NOTICE.md b/research/antifano-subspace-audit/UPSTREAM-NOTICE.md new file mode 100644 index 0000000000..6991d8ac18 --- /dev/null +++ b/research/antifano-subspace-audit/UPSTREAM-NOTICE.md @@ -0,0 +1,23 @@ +# Notice + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0 (`LICENSE`, copied from the repository root). + +## Credits (prior work this package stands on) + +- **#446** (Theorem C; closed, not merged): the cost formula and exactness model, carried by the merged **#595** (FL C.6): the pairing model and the window table. +- **#717**: the provenance / manifest pattern (`checks/provenance.py` follows it) and the complex E8 decoders. +- **#1590** (`research/root-unit-decoder-lemmas`, merged): Lemma A (T ≤ 2), the lift identity Lemma B, ERR1. The Lean file formalises the rank argument behind Lemma B; the step-0 manifest check and the PASS/FAIL style of `verify.sh` follow that package. +- **#2111** (pending): the three-total model and lemmas, the sharp example `tied_min`, the configurations in `data/` (copies), `lib/kit.py`, `lib/satlib.py`, `c/enumall.c`. This package asks and answers a different question about the same objects and is self-contained; it does not depend on #2111 being merged. +- **#2031** (pending): the DRAT certificate of the D5 CNF of #1590, cited as context, not duplicated. +- **#2125** (pending): the T² threshold for root-unit decoders, the context for why characteristic 2 matters. +- Our own swarm working cards of 2026-10-14 (the `KPR4-T3` struct card: tracks on CR2, the map φ, jets, the jetfail search, and the Lean project), shipped verbatim in `evidence/PROOF-working-notes.md`. + +## New in this package + +`README.md`, `verify.sh`, `requirements.txt`, `MANIFEST.sha256`, `checks/*.py` (written for this package; they re-implement the checks of the working scripts in exact arithmetic with fixed seeds), `data/tied_min_B.json`, `data/cr2_realisations.json`, `scripts/make_data.py`, and `lean/`. + +## Adapted from our earlier work + +- `lib/kit.py`, `lib/satlib.py`, `c/enumall.c`, `data/*.json` (configurations): unchanged copies from #2111 (themselves from the working cards). +- `lib/cr2.py`, `gr.py`, `phi.py`, `gen.py`, `tangent.py`, `jet2.py`, `col.py` and `scripts/t*.py`, `tied_min_jet_cert.py`, `verify_cr2.py`: the working scripts of the struct card; only the import / data paths were changed (and `t4.py`, `t18.py`, `t22.py` write their output to the current directory). +- `data/jf0..2.json`, `data/tm_noncr2.json`: outputs of those scripts. diff --git a/research/antifano-subspace-audit/VERIFY.json b/research/antifano-subspace-audit/VERIFY.json new file mode 100644 index 0000000000..755910d72a --- /dev/null +++ b/research/antifano-subspace-audit/VERIFY.json @@ -0,0 +1,29 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-X", "dev", "-W", "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Source-bound complete row/column subspace censuses, unique completions, exchange premises and sharp cost-twelve witness." + }, + { + "argv": ["{python}", "-X", "dev", "-W", "error", "-B", "-m", "unittest", "discover", "-s", "{package}", "-p", "test_*.py"], + "timeout_seconds": 60, + "checks": "Ten behavior groups, independent dense rank oracle, multiple/zero-completion fixtures, semantic corruptions and capacity controls." + }, + { + "argv": ["{python}", "-I", "-O", "-X", "dev", "-W", "error", "-B", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "Optimized standalone replay retains all acceptance checks." + } + ] +} diff --git a/research/antifano-subspace-audit/ruff.toml b/research/antifano-subspace-audit/ruff.toml new file mode 100644 index 0000000000..700b054e2e --- /dev/null +++ b/research/antifano-subspace-audit/ruff.toml @@ -0,0 +1,12 @@ +target-version = "py312" +line-length = 100 + +[lint] +select = ["ALL"] +ignore = [ + "D203", "D213", # Mutually exclusive with the selected D211/D212 docstring rules. + "INP001", # Standalone scripts discovered by unittest, not an importable package. + "PLR2004", # Literal dimensions and ranks name the fixed mathematical instance. + "PT009", "PT027", # Keep standard-library unittest and its -O-safe assertions. + "T201", # The CLI's single PASS line is its documented observable output. +] diff --git a/research/antifano-subspace-audit/test_verify.py b/research/antifano-subspace-audit/test_verify.py new file mode 100644 index 0000000000..7c0f085add --- /dev/null +++ b/research/antifano-subspace-audit/test_verify.py @@ -0,0 +1,135 @@ +"""Behavior checks and deliberate corruptions for the independent anti-Fano audit.""" +# Copyright 2026 Nick Petalas +import copy +import hashlib +import itertools +import json +import unittest + +import verify + + +class SubspaceAuditTests(unittest.TestCase): + """Exercise exact results, independent oracles and meaningful failure paths.""" + + @classmethod + def setUpClass(cls) -> None: + """Compute the complete fixed audit once for these read-only tests.""" + cls.config = verify.load_configuration((verify.PACKAGE / "CONFIGURATION.json").read_bytes()) + cls.report = verify.audit(cls.config) + + def test_exact_full_receipt(self) -> None: + """Match the full receipt and every vendored source digest.""" + expected = json.loads((verify.PACKAGE / "EXPECTED.json").read_bytes()) + verify.compare_report(self.report, expected) + self.assertEqual(self.report["upper_ranks"], [4, 4, 4]) + self.assertEqual([b["completions"] for b in self.report["blocks"]], [1, 1, 1]) + sources = json.loads((verify.PACKAGE / "SOURCES.json").read_bytes()) + for source in sources["vendored_files"]: + payload = (verify.PACKAGE / source["path"]).read_bytes() + self.assertEqual(hashlib.sha256(payload).hexdigest(), source["sha256"]) + + def test_rank_against_dense_exhaustive_oracle(self) -> None: + """Match dense elimination on every three-by-four binary matrix.""" + # Every 3x4 binary matrix, using a separate dense Gauss-Jordan oracle. + for encoded in range(4096): + rows = [(encoded >> (4 * i)) & 15 for i in range(3)] + matrix = [[(row >> j) & 1 for j in range(4)] for row in rows] + rank = 0 + for column in range(4): + pivot = next((i for i in range(rank, 3) if matrix[i][column]), None) + if pivot is None: + continue + matrix[rank], matrix[pivot] = matrix[pivot], matrix[rank] + for i in range(3): + if i != rank and matrix[i][column]: + matrix[i] = [x ^ y for x, y in zip(matrix[i], matrix[rank], strict=True)] + rank += 1 + self.assertEqual(verify.binary_rank(rows), rank) + + def test_census_counts_multiple_and_zero_completions(self) -> None: + """Compare completion counts with brute force on small affine alphabets.""" + # First three columns have a variable upper-triangular 3x3 minor. + options = ((15, 1, (1,)), (14, 2, (2, 3)), (12, 4, (4, 5, 6, 7)), + (8, 0, tuple(range(8)))) + trials, count, _ = verify.column_census(options, (0, 1, 2)) + brute = sum(verify.binary_rank(list(columns)) == 3 + for columns in itertools.product(*(o[2] for o in options))) + self.assertEqual((trials, count, brute), (8, 64, 64)) + impossible = (*options[:3], (15, 8, (8,))) + self.assertEqual(verify.column_census(impossible, (0, 1, 2)), (8, 0, None)) + + def test_invalid_upper_witnesses_reject(self) -> None: + """Reject wrong diagonals, forbidden entries and a cost-twenty-four witness.""" + good = self.report["upper_rows"] + missing = good.copy() + missing[0] ^= 1 + forbidden = good.copy() + forbidden[0] |= 1 << 1 + for bad in (missing, forbidden, [1 << t for t in range(12)]): + with self.subTest(rows=bad), self.assertRaises(ValueError): + verify.validate_upper(self.config, bad) + + def test_receipt_corruptions_reject(self) -> None: + """Reject truncated counts, false uniqueness and false mathematical claims.""" + mutations = [] + for key, value in (("column_trials", 262143), ("completions", 0)): + bad = copy.deepcopy(self.report) + bad["blocks"][0][key] = value + mutations.append(bad) + bad = copy.deepcopy(self.report) + bad["blocks"][1]["unique_columns"][0] ^= 1 + mutations.append(bad) + bad = copy.deepcopy(self.report) + bad["lower_bound"] = 13 + mutations.append(bad) + for bad in mutations: + with self.subTest(receipt=bad), self.assertRaisesRegex(ValueError, "receipt mismatch"): + verify.compare_report(self.report, bad) + + def test_full_pattern_is_not_a_cost_twelve_claim(self) -> None: + """Confirm that some admissible matrices cost twenty-four, not twelve.""" + allowed = verify.incidence(self.config) + rows = [(1 << t) | sum(1 << s for s in range(12) if allowed[t][s]) + for t in range(12)] + self.assertEqual(verify.block_ranks(self.config, rows), [8, 8, 8]) + + def test_capacity_failures(self) -> None: + """Reject rank, configuration and census requests outside fixed capacities.""" + for vectors in ([4096], [0] * 13): + with self.subTest(vectors=vectors), self.assertRaisesRegex(ValueError, "rank capacity"): + verify.binary_rank(vectors) + with self.assertRaisesRegex(ValueError, "configuration capacity"): + verify.load_configuration(b" " * 4097) + with self.assertRaisesRegex(ValueError, "census shape"): + verify.column_census((), (0, 1, 2)) + options = ((15, 1, (1,)), (15, 2, (2,)), (15, 4, (4,))) + with self.assertRaisesRegex(ValueError, "census shape"): + verify.column_census(options, (0, 1, 2, 2)) + with self.assertRaisesRegex(ValueError, "row census shape"): + verify.row_census(self.config, tuple(range(8)), (0, 1, 2, 2)) + + def test_configuration_pin_rejects_semantic_mutation(self) -> None: + """Reject a changed source vector before the audit runs.""" + bad = copy.deepcopy(self.config) + bad[0][1][0] = 1 + with self.assertRaisesRegex(ValueError, "configuration pin"): + verify.load_configuration(json.dumps(bad).encode()) + + def test_exchange_rejects_wrong_class_space(self) -> None: + """Reject a proposed completion that violates the projection premises.""" + block = self.report["blocks"][0] + values = block["unique_columns"].copy() + values[0] ^= 1 << block["zero_rows"][0] + with self.assertRaises(ValueError): + verify.exchange_properties(self.config, 0, block["columns"], values) + + def test_dependent_census_basis_rejects(self) -> None: + """Reject dependent basis choices instead of counting a smaller space twice.""" + options = ((15, 1, (1,)), (15, 1, (1,)), (15, 4, (4,))) + with self.assertRaisesRegex(ValueError, "basis is not independent"): + verify.column_census(options, (0, 1, 2)) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/antifano-subspace-audit/verify.py b/research/antifano-subspace-audit/verify.py new file mode 100644 index 0000000000..05f072b1d3 --- /dev/null +++ b/research/antifano-subspace-audit/verify.py @@ -0,0 +1,267 @@ +#!/usr/bin/env python3 +"""Exact subspace audit of PR2111's anti-Fano exchange proof. Apache-2.0.""" +# Copyright 2026 Nick Petalas +import hashlib +import itertools +import json +import math +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +CONFIG_SHA256 = "670ed90924b601ade22f0d4adaff46d1667e5449326a0f7ba7b88dd8f5906f93" + +type Config = list[list[list[int]]] +type Incidence = tuple[tuple[bool, ...], ...] +type ColumnOption = tuple[int, int, tuple[int, ...]] +type Census = tuple[int, int, list[int] | None] + + +# The boolean is an assertion predicate, not a behavior-selection flag. +def require(condition: bool | int, message: str) -> None: # noqa: FBT001 + """Reject a failed boundary check or mathematical obligation, including under -O.""" + if not condition: + raise ValueError(message) + + +def load_configuration(payload: bytes) -> Config: + """Parse only the pinned, capacity-bounded twelve-line configuration.""" + require(len(payload) <= 4096, "configuration capacity") + require(hashlib.sha256(payload).hexdigest() == CONFIG_SHA256, "configuration pin") + config = json.loads(payload) + require(len(config) == 12, "twelve lines required") + for pair in config: + require(len(pair) == 2 and all(len(v) == 3 for v in pair), "vector shape") + p, q = pair + require(all(type(x) is int and abs(x) == 1 for x in p), "point support") + require(all(type(x) is int and x in (-1, 0, 1) for x in q), "line entries") + require(sum(x != 0 for x in q) == 2 and dot(p, q) != 0, "line support/diagonal") + return config + + +def dot(a: list[int], b: list[int]) -> int: + """Compute an exact integer inner product with equal-length operands.""" + return sum(x * y for x, y in zip(a, b, strict=True)) + + +def binary_rank(vectors: list[int]) -> int: + """Eliminate at most twelve vectors of at most twelve bits, without recursion.""" + require(len(vectors) <= 12 and all(0 <= x < 4096 for x in vectors), "rank capacity") + pivots = [0] * 12 + for original in vectors: + vector = original + for bit in range(11, -1, -1): + if not (vector >> bit) & 1: + continue + if pivots[bit]: + vector ^= pivots[bit] + else: + pivots[bit] = vector + break + return sum(x != 0 for x in pivots) + + +def incidence(config: Config) -> Incidence: + """Derive all optional off-diagonal entries directly from rational orthogonality.""" + return tuple(tuple(t != s and dot(config[t][0], config[s][1]) == 0 + for s in range(12)) for t in range(12)) + + +def block_columns(config: Config, j: int) -> tuple[int, ...]: + """Return the column support of coordinate j.""" + return tuple(s for s in range(12) if config[s][1][j] != 0) + + +def triangular_pivot(allowed: Incidence, columns: tuple[int, ...]) -> tuple[int, ...]: + """Find a principal unit upper-triangular minor valid for every admissible B.""" + for pivot in itertools.permutations(columns, 3): + if all(not allowed[t][s] for i, t in enumerate(pivot) for s in pivot[:i]): + return pivot + message = "no universal rank-three minor" + raise ValueError(message) + + +def column_options(allowed: Incidence, s: int) -> ColumnOption: + """List one column's complete alphabet and mandatory-bit constraint.""" + free = tuple(t for t in range(12) if allowed[t][s]) + require(len(free) <= 6, "column alphabet exceeds 64") + values = tuple((1 << s) | sum(((mask >> i) & 1) << t for i, t in enumerate(free)) + for mask in range(1 << len(free))) + fixed = 4095 ^ sum(1 << t for t in free) + return fixed, 1 << s, values + + +def column_census(options: tuple[ColumnOption, ...], basis_indices: tuple[int, ...]) -> Census: + """Count all rank-three completions, retaining only the first as a witness. + + The caller supplies three columns with a universal nonsingular minor. + Each matrix therefore has exactly one tuple of those three basis columns. + """ + require(3 <= len(options) <= 8 and len(basis_indices) == 3 + and len(set(basis_indices)) == 3, "census shape") + require(all(0 <= i < len(options) for i in basis_indices), "basis indices") + require(all(1 <= len(o[2]) <= 64 for o in options), "census alphabet") + rest = tuple(i for i in range(len(options)) if i not in basis_indices) + trials = completions = 0 + witness = None + for basis in itertools.product(*(options[i][2] for i in basis_indices)): + trials += 1 + a, b, c = basis + space = (0, a, b, c, a ^ b, a ^ c, b ^ c, a ^ b ^ c) + require(len(set(space)) == 8, "basis is not independent") + choices = [] + for i in rest: + fixed, diagonal, _ = options[i] + matches = tuple(x for x in space if x & fixed == diagonal) + if not matches: + break + choices.append(matches) + if len(choices) != len(rest): + continue + completions += math.prod(len(values) for values in choices) + if witness is None: + by_index = dict(zip(basis_indices, basis, strict=True)) + by_index.update((i, values[0]) for i, values in zip(rest, choices, strict=True)) + witness = [by_index[i] for i in range(len(options))] + require(trials == math.prod(len(options[i][2]) for i in basis_indices), + "column census coverage") + return trials, completions, witness + + +def row_census(config: Config, columns: tuple[int, ...], pivot: tuple[int, ...]) -> Census: + """Run the transpose census using eight-bit rows, sets and row-span doubling.""" + require(len(columns) == 8 and len(pivot) == 3 and len(set(pivot)) == 3, + "row census shape") + choices = [] + for t in range(12): + diagonal = sum(1 << i for i, s in enumerate(columns) if t == s) + forbidden = sum(1 << i for i, s in enumerate(columns) + if t != s and dot(config[t][0], config[s][1]) != 0) + choices.append(frozenset(x for x in range(256) + if x & forbidden == 0 and x & diagonal == diagonal)) + require(all(len(values) == 16 for values in choices), "row alphabet") + trials = completions = 0 + first = None + for rows in itertools.product(*(choices[t] for t in pivot)): + trials += 1 + space = {0} + for row in rows: + space |= {x ^ row for x in tuple(space)} + require(len(space) == 8, "row basis is not independent") + matches = [] + for t in range(12): + possible = {rows[pivot.index(t)]} if t in pivot else space & choices[t] + if not possible: + break + matches.append(possible) + if len(matches) != 12: + continue + completions += math.prod(len(values) for values in matches) + if first is None: + first = [min(values) for values in matches] + require(trials == 4096, "row census coverage") + return trials, completions, first + + +def as_rows(columns: list[int]) -> list[int]: + """Transpose the packed column witness for entrywise oracle comparison.""" + return [sum(((value >> t) & 1) << i for i, value in enumerate(columns)) + for t in range(12)] + + +def exchange_properties( + config: Config, j: int, columns: tuple[int, ...], values: list[int], +) -> dict[str, list[int]]: + """Check every finite premise used by the credited projection argument.""" + require(binary_rank(values) == 3, "rank-three witness") + missing = tuple(t for t in range(12) if config[t][1][j] == 0) + require(all(all(not ((value >> t) & 1) for t in missing) for value in values), + "missing-class rows must vanish") + ranks = [] + for k in range(3): + if k != j: + group = [value for s, value in zip(columns, values, strict=True) + if config[s][1][k] == 0] + ranks.append(binary_rank(group)) + require(ranks == [3, 3], "two class spaces must both equal the rank-three union") + pair = next(((a, b) for a, b in itertools.combinations(missing, 2) + if dot(config[a][0], config[b][1]) != 0 + and dot(config[b][0], config[a][1]) != 0), None) + require(pair is not None, "missing-class universal identity minor") + return {"class_space_ranks": ranks, "zero_rows": list(missing), + "projection_identity_minor": list(pair)} + + +def block_ranks(config: Config, rows: list[int]) -> list[int]: + """Compute all three raw coordinate-block ranks of a packed matrix.""" + return [binary_rank([sum(((row >> s) & 1) << i + for i, s in enumerate(block_columns(config, j))) + for row in rows]) for j in range(3)] + + +def validate_upper(config: Config, rows: list[int]) -> list[int]: + """Reject inadmissible or non-cost-twelve upper-bound witnesses.""" + allowed = incidence(config) + require(len(rows) == 12 and all(type(x) is int and 0 <= x < 4096 for x in rows), + "upper witness shape") + for t in range(12): + require((rows[t] >> t) & 1, "upper witness diagonal") + require(all(not ((rows[t] >> s) & 1) or t == s or allowed[t][s] + for s in range(12)), "upper witness forbidden entry") + ranks = block_ranks(config, rows) + require(ranks == [4, 4, 4], "upper witness must have cost twelve") + return ranks + + +def audit(config: Config) -> dict[str, object]: + """Reconstruct both censuses, the exchange premises and a sharp upper bound.""" + allowed = incidence(config) + require(sum(map(sum, allowed)) == 72, "incidence count") + blocks = [] + for j in range(3): + columns = block_columns(config, j) + require(len(columns) == 8, "eight columns per block") + pivot = triangular_pivot(allowed, columns) + options = tuple(column_options(allowed, s) for s in columns) + indices = tuple(columns.index(s) for s in pivot) + trials, count, values = column_census(options, indices) + rtrials, rcount, rows = row_census(config, columns, pivot) + require((trials, count, rtrials, rcount) == (262144, 1, 4096, 1), "uniqueness census") + if values is None or rows is None: + message = "missing census witness" + raise ValueError(message) + require(as_rows(values) == rows, "row/column census disagreement") + properties = exchange_properties(config, j, columns, values) + blocks.append({"coordinate": j, "columns": list(columns), "triangular_minor": list(pivot), + "column_trials": trials, "row_trials": rtrials, "completions": count, + "unique_columns": values, **properties}) + upper = [9, 258, 36, 9, 2064, 36, 576, 1152, 258, 576, 1152, 2064] + ranks = validate_upper(config, upper) + full_rows = [(1 << t) | sum(1 << s for s in range(12) if allowed[t][s]) + for t in range(12)] + return {"lines": 12, "incidences": 72, "blocks": blocks, + "lower_bound": min(3 * 4, 3 + 2 * (3 + 2)), + "rank_three_case_floor": 3 + 2 * (3 + 2), + "upper_rows": upper, "upper_ranks": ranks, + "full_pattern_ranks": block_ranks(config, full_rows)} + + +def compare_report(actual: object, expected: object) -> None: + """Reject any difference between reconstructed evidence and the stored receipt.""" + require(actual == expected, "receipt mismatch") + + +def main() -> None: + """Run the bounded standalone audit without writing artifacts.""" + config_path = PACKAGE / "CONFIGURATION.json" + expected_path = PACKAGE / "EXPECTED.json" + require(config_path.stat().st_size <= 4096, "configuration capacity") + require(expected_path.stat().st_size <= 16384, "receipt capacity") + config = load_configuration(config_path.read_bytes()) + report = audit(config) + compare_report(report, json.loads(expected_path.read_bytes())) + print("PASS_ANTIFANO_SUBSPACE_AUDIT minimum=12 blocks=3 " + "column_trials=786432 row_trials=12288 unique_rank3=1,1,1 no_new_kappa") + + +if __name__ == "__main__": + main() From 296badeafb15e98d3cdfacee43f90e2b3648816b Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 15 Oct 2026 00:11:46 +0100 Subject: [PATCH 2/2] docs(research): refresh anti-Fano submission status --- research/antifano-subspace-audit/TASK.json | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/research/antifano-subspace-audit/TASK.json b/research/antifano-subspace-audit/TASK.json index 1137e957e4..97e48fcdb8 100644 --- a/research/antifano-subspace-audit/TASK.json +++ b/research/antifano-subspace-audit/TASK.json @@ -60,13 +60,13 @@ "coordination": { "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18934590", "claim_posted": false, - "reason": "The invoked engineering-mode skill forbids human-directed external messages. Read-only overlap and board checks were performed; communication text remains a local draft. No retrospective reservation is claimed." + "reason": "No advance claim was posted. This package answers the unreserved independent-check handoff. The donor explicitly requested upstream PR publication in a follow-up; publication reports the completed evidence without a retrospective reservation." }, "freshness": { "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", "priority_revision": 4, - "checked_at_utc": "2026-10-14T23:02:26Z", - "overlap": "Final find_overlap.py refresh for anti-Fano, tied_min and subspace audit; complete pagination over 435 open PRs and 876 discussion records, fetched 23:01:00Z and 23:02:25Z. Only source PR2111, source PR2162, the independent-check request and this local package matched. No code diffs or arbitrary nested files were searched; this is not proof of novelty. Canonical main and both predecessor heads were unchanged.", + "checked_at_utc": "2026-10-14T23:11:12Z", + "overlap": "Pre-PR find_overlap.py refresh for anti-Fano, tied_min and subspace audit; complete pagination over 436 open PRs and 877 discussion records, fetched 23:09:46Z and 23:11:11Z. Only source PR2111, source PR2162, the independent-check request and this local package matched. No code diffs or arbitrary nested files were searched; this is not proof of novelty. Canonical main and both predecessor heads were unchanged.", "predecessor_heads_rechecked": true }, "environment": {