From 518351a389e32e2ccdf0a1ca55580e9c60d65492 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Fri, 6 Nov 2026 09:05:13 -0800 Subject: [PATCH] Attain six formal query targets with two clean helpers (no kappa) --- research/clean-two-helper-query/CREDITS.md | 12 + research/clean-two-helper-query/LICENSE | 201 +++++++++ research/clean-two-helper-query/NOTICE | 415 ++++++++++++++++++ research/clean-two-helper-query/PROOF.md | 176 ++++++++ research/clean-two-helper-query/README.md | 47 ++ .../clean-two-helper-query/SOURCE-PINS.json | 25 ++ research/clean-two-helper-query/SOURCES.json | 18 + research/clean-two-helper-query/TASK.json | 89 ++++ research/clean-two-helper-query/VERIFY.json | 30 ++ .../vendor/PR6800-PROOF.md | 171 ++++++++ .../vendor/PR6800-README.md | 131 ++++++ research/clean-two-helper-query/verify.py | 361 +++++++++++++++ 12 files changed, 1676 insertions(+) create mode 100644 research/clean-two-helper-query/CREDITS.md create mode 100644 research/clean-two-helper-query/LICENSE create mode 100644 research/clean-two-helper-query/NOTICE create mode 100644 research/clean-two-helper-query/PROOF.md create mode 100644 research/clean-two-helper-query/README.md create mode 100644 research/clean-two-helper-query/SOURCE-PINS.json create mode 100644 research/clean-two-helper-query/SOURCES.json create mode 100644 research/clean-two-helper-query/TASK.json create mode 100644 research/clean-two-helper-query/VERIFY.json create mode 100644 research/clean-two-helper-query/vendor/PR6800-PROOF.md create mode 100644 research/clean-two-helper-query/vendor/PR6800-README.md create mode 100644 research/clean-two-helper-query/verify.py diff --git a/research/clean-two-helper-query/CREDITS.md b/research/clean-two-helper-query/CREDITS.md new file mode 100644 index 0000000000..701a261869 --- /dev/null +++ b/research/clean-two-helper-query/CREDITS.md @@ -0,0 +1,12 @@ +# Attribution and scope + +Prepared for ToikY with substantial source-aware OpenAI Codex assistance through proposal, implementation, mathematical challenge, overlap/credit and metadata roles. The provisional block recipe was written during prior-session verification before fresh selection; it was unexecuted and unaccepted then. Current source/proposal/future exposure is disclosed, and no blind, independent-human, proof-kernel or independent-end-to-end claim is made. + +- Nick Petalas, PR6800, head c94197e40c9e8a25f643d776160659871e5ce9ac: restored-dirty-workspace theorem, odd clean control and explicit even-clean question. Its floor is a cited theorem, not a predecessor replay or new result here. +- Josie Elliston, PR6138, head6c3562e62f43b8490fa327d745b877d9f8d9911b: workspace-free all-call capacity, attainment and independent6122audit. +- Nick Petalas, PR6122, heade4fb5699c1c390ada0e6ac738d48548c462448b1: four-call Gram capacity theorem. +- Ali Romman5617: coupled Gram/block-simplex framework; Cinna Davis: simplex/controller lineage; Matarener6114: higher-rank query question. Block matrices, trace/rank arguments and dual-number algebra are classical. +- JoyboyBrian5007and Petalas5857: prior clean coupling/compiler and primitive stream in a different idempotent-reflection alphabet. Their clean-resource and call-count results are not rediscovered here. +- Josie Elliston1974/Hanson Sun's GL3model and Gareth Davidson2027/UT4mixed-root lineage supply the required card comparison, not a theorem or tariff transferred to this changed model. Retain all their predecessor credits, source headers, root NOTICE and Apache-2.0 license. + +The written exact-version proof challenge found no blocker. A source-aware implementation role wrote an unexecuted verifier; root strengthened rejection controls before the first run, and a separate static code role checked that revision. Root then performed the first1.364-second finite replay, retaining its initial code/receipt/package hashes. Later delivery replay is reported separately. All roles share source/proposal context. The word's specified total paid rank8 is not a total-rank optimum. Native conversion, clean resource/basis prices, actual caller integration, full supplier bill and all five selected assumptions remain open. diff --git a/research/clean-two-helper-query/LICENSE b/research/clean-two-helper-query/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/clean-two-helper-query/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/clean-two-helper-query/NOTICE b/research/clean-two-helper-query/NOTICE new file mode 100644 index 0000000000..59d8e0cf31 --- /dev/null +++ b/research/clean-two-helper-query/NOTICE @@ -0,0 +1,415 @@ +A sharper exponent for integer multiplication +Copyright 2026 Douglas Colkitt + +This project includes unmodified source files from OpenAI's manuscript +"Integer multiplication below n log n" and its accompanying repository: +https://github.com/openai/math +Commit: adc7f1241b42e322a6451854ab7e4b4c146bf78a + +The original manuscript identifies OpenAI as its author. Its Apache-2.0 +license is retained at upstream/LICENSE. The exact source URLs and hashes +are recorded in upstream/manifest.json. Proposed modifications are supplied +as separate files under patches/; upstream source files remain unchanged. + +The original local research note, scripts, certificates, patches, and +documentation were prepared by Douglas Colkitt with assistance from OpenAI +Codex. The community release incorporates work by the contributors identified +in the notices below; it is not solely Douglas Colkitt's work. +This project is not an official OpenAI release or an OpenAI endorsement. + +Related contributions (not imported in this checkpoint): +Zhihao Chen (jacklightChen), PR #7, supplied an earlier ternary five-subset +motif, finite-alphabet transfer and a different compressed producer: +https://github.com/CrocSwap/integer-mult-bounds/pull/7 +The present checkpoint claims no priority for that motif. Related compressed +complex-network work was submitted by eumemic in PR #3: +https://github.com/CrocSwap/integer-mult-bounds/pull/3 +The pending contributions and their stronger bounds require their own review; +this notice does not represent adoption or verification of their claims. + +Additional community work, including parallel and superseded submissions, is +acknowledged in CONTRIBUTORS.md, with pinned submission metadata in +docs/research/contribution-snapshot.json. These acknowledgements do not imply +joint authorship of the checkpoint, incorporation of pending code, or verification +of submitted mathematical claims. Original source-specific notices remain in force. + +Community release (accepted by conditional maintainer audit): +The following original contributor notices apply to the imported PR #39 chain. +The preceding non-import statements describe the preserved 2^-30 checkpoint. + +Ternary five-subset construction and common-four-point resynthesis +Copyright 2026 Zhihao Chen (jacklightChen) + +This is Zhihao Chen's first submission of this specific construction to this +repository. Research, proof development, code and verification were prepared +with substantial assistance from GPT-6 Astra (OpenAI Codex), as identified by +the contributor. This is not independent review or an OpenAI endorsement. +Future research building on this contribution should explicitly acknowledge +Zhihao Chen (jacklightChen), cite the accompanying note and pull request, and +retain the preceding contributors' attribution. This notice records research +provenance; the repository's Apache-2.0 license remains unchanged. + +Dependencies retained from eumemic's Claude-assisted PRs #3 and #5: +https://github.com/CrocSwap/integer-mult-bounds/pull/3 +https://github.com/CrocSwap/integer-mult-bounds/pull/5 +PR #5 commit: d3d370c34937503bd3fa63c83d505a05e8e50893 +These include complex_circuit.py, complex_network.py, fast_gaussian.py, +their generators, construction notes and certificates. The Gaussian input +scaling proof is corrected in this derivative; see the modification notice below. +Aligned pairing also appears in Bortlesboat's PR #2. Retained totals and bank +sharing appear in dleen's PR #4 and cheaper retained centers in eumemic's PR #6. +Their results and ideas are credited separately from this new construction. + +Bulk recursion and controlled tensor basis, 8 October 2026 +Copyright 2026 icekylinx + +The new projector batching, controlled simultaneous basis, mixed-width tape +recursions, whole-residual complex recursion, and dependency-path precision +guard in the batched-23 proof package are contributed by icekylinx, developed +with substantial OpenAI GPT-6 Astra assistance. Review corrections and +repository integration were prepared with OpenAI Codex assistance. They build on the retained +PR #7 finite producers and the preceding contributions credited above. +The new package retains the repository's Apache-2.0 license and the original +authors' attribution. It is not an official OpenAI release or endorsement. + +Modification notice, 8 October 2026 (icekylinx): the retained fast Gaussian +proof now bounds shifted approximation error by F=2^ceil(1.14 alpha^2). +The P=34p precision budget and asymptotic exponent are unchanged. New batching +checks are integrated into make verify. Existing attribution and licenses +are retained. + +Partial-swap extension, 8 October 2026 +Copyright 2026 icekylinx + +The partial-swap framing, binary retained-total triple construction, +dependency-preserving positive labels and carrier reuse, unequal (25,23,57) +common basis, improved complex batching, and exact assembly are contributed +by icekylinx with substantial OpenAI GPT-6 Astra and Codex assistance. +This extension directly inherits PR #10, commit +62691e395a0458ce089a1c7b5d89e74291e95e29. The portable producer adapters +modify the retained paired-exclusion and shared-point implementations credited +above. The original licenses, attribution, and Gaussian correction are retained. + +Endpoint-gauge extension, 8 October 2026 +Copyright 2026 icekylinx + +The complementary auxiliary endpoint gauges, (32,30,40) controlled basis, +general nondegenerate binary phase residuals, retained-center complex producer, +updated path guard and exact assembly are contributed by icekylinx with +substantial OpenAI GPT-6 Astra and Codex assistance. This extension inherits +f2ab41aebad47861caf6316282c1793e5513845e and its PR #10 ancestry. New portable +adapters retain the paired-exclusion and shared-point contributions credited +above. Original licenses, notices and the Gaussian correction are retained. + +Structured-basis and semantic-bulk extension, 8 October 2026 +Copyright 2026 icekylinx + +The selected (32,30,36) bit construction, A1/A5 block refinements, fixed +middle-axis I+J profiles with bounded-minor CRT certificates, mixed dyadic +complex centers, complete data-front batching and circuit-specific assembly +are contributed by icekylinx with substantial OpenAI GPT-6 Astra and Codex +assistance. The immediate parent is ed90fd940279c336ebc45968631bdebfb087b505. + +The semantic/bulk compatibility argument, literal scalar charge, product row +stock and parameterization adapt Zhihao Chen (jacklightChen)'s PR #23, +commit 661ebabc1076c9f525d7ce4967c876b203fa9827. Translated complex endpoints +are adopted from the same contributor's PR #21, +commit 5ba6cf0bfb68f2be8d15610e7972207c50254d6a, following eumemic's source-frame +work and the earlier nested-basis contributions. + +Completed-child semantic precision, arbitrary-coordinate routing, phase-cell +Gaussian inversion and bulk tape transfer are credited to the RaD project +(hipotures), commit 45d9b60355872041f9275f77c057514def0d45bc, exposed through +PR #20 at 4f8d6c8272b5ff307a0da51df545ec3cd96a8b6e. Their selected proof +sources retain their separate CC0 license and original NOTICE under +references/semantic-bulk/rad20. The PR #23 source retains its recorded OpenAI +Codex assistance; RaD retains its recorded Codex and GPT-6.1-Sol Ultra +assistance. These are source attributions, not claims about this session's +runtime model. Related contributions by Rohan Arun and Aurel Prosz remain +acknowledged in the imported notices. No exclusive priority or additional +license condition is asserted. + +Copied retained-center extension, 8 October 2026 +Copyright 2026 icekylinx + +The copied retained-center schedule in both orientations, its complex-phase +transfer, the Wm-N+L rank budget, and the selected (25,23)/(28,28) composition +are contributed by icekylinx with substantial OpenAI GPT-6 Astra and Codex +assistance. This extension inherits PR #32 at +0ef3aeb61f55cc0b321ce6a0ef00acee25cefe52 and the preceding PR #10/#18/#24 work. + +The two-stage topology and paid copied-stream endpoint correction are due +to Aurel Prosz (Paureel), c82d09eb4781b68435e3fa3eb6beea72fa900fab, +through Zhihao Chen (jacklightChen)'s PR #29 unequal-axis composition, +9d963275075fa98f1da821e27757b238dafd6b3c. That source also credits Swapnil +Jain's two-stage development at ae405eb474d1486b2d8aef90139869f927f4836a. + +The contiguous corner method, incidence factorization and exact partition +certificates are due to Rohan Arun (PR #31), method commit +02f68f95369c39955c5ffcfddbd75cd83e26b305. The selected (25,23) certificate +specializes Dominik Scholz's parameterization (PR #33), +a499a345c040aa15b68e984a0904eadc485c7a7e. Their source notices and proof +snapshots are preserved in references/copied-centers. Historical OpenAI +Codex, GPT-6 Astra and Anthropic Claude Opus 5.5 assistance is credited to +the respective imported sources. Existing PR #21/#23 and RaD attribution, +licenses and the Gaussian correction remain in force. + +Copied centers with reversed (23,25) data corners, 2026-10-08 +Rohan Arun with substantial OpenAI Codex assistance supplies the composition, +exact dimension23 controls and cost/assembly integration. James Chang's PR34 +supplies the reversed boundary family; icekylinx's PR36 supplies copied retained +centers and the selected complex graph. The balanced assembly remains attributed +to RaD/hipotures and its PR34 specialization. Retain Dominik Scholz PR33, Rohan +Arun PR31, Zhihao Chen PR29/21/23, Paureel/Aurel Prosz, Swapnil Jain, icekylinx, +eumemic, Douglas Colkitt, OpenAI and all earlier notices and hypotheses. +This is not a claim of formal verification, new foundational rank identities, +global optimality or measured runtime speedup. + +Fixed middle basis with copied reversed corners (2026-10-08): +Rohan Arun, with substantial OpenAI Codex assistance. Composition and +simultaneous-basis proof retain icekylinx PR32/36, James Chang PR34, +Dominik Scholz PR35/38, Zhihao Chen, Paureel, Swapnil Jain, RaD/hipotures, +eumemic and all preceding attribution and licenses. See research/copied-fixed-reversed. + +Changed-graph composition with copied centers and fixed bases, 8 October 2026 +Prepared with OpenAI Codex assistance. +The new composition uses icekylinx PR36 copied centers and PR32 fixed-I+J +projectors/profiler, Dominik Scholz PR35 two fixed factors and CRT argument, +Zhihao Chen (jacklightChen) PR29/23 interfaces, Aurel Prosz (Paureel) and +Swapnil Jain's two-stage development, Rohan Arun PR25/31 corner methods, +Dominik Scholz PR33/38 dimension/composition work; James Chang (jamesyc) +PR34 reversed geometry and balanced transfer; Rohan Arun PR37/39/40 +reversed integration, modular data tests and both-fixed baseline; +RaD (hipotures) PR41 changed scalar DAGs, alternating point order and +independent role compiler; RaD balanced routing/bulk interfaces, and all +retained predecessors. +Complete attribution and the conditional proof boundary are recorded in +research/copied-fixed/PROOF.md; imported originals and source pins are retained. +Original Apache-2.0 and CC0 notices remain applicable. + +Community follow-up integration (PRs #49, #45 and #26), 8 October 2026: +Rohan Arun contributes weighted carrier matching and climbed summand/leave-one-out +orders (PRs #44/#47/#49), with Anthropic Claude assistance. The final construction +composes Chafik Boukhalfa's changed-graph checks, exact rational data recovery and +reordered exclusion sums (PRs #43/#46/#48, OpenAI Codex assistance) with RaD / +hipotures's alternating pair order and independent physical role compiler (#41). +All predecessor attribution and conditional proof interfaces remain in force. + +Alejandro Zarzuelo Urdiales contributes Gaussian parity and canonical arithmetic +proofs, finite tensor execution, profile precision accounting and mixed-center +reference checks (#45), with substantial OpenAI Codex assistance. See +research/gaussian-parity-synthesis/PROVENANCE.md for his full attribution. +Ryan S / princezuda contributes historical Lean certificate arithmetic, algebraic +frame/movement/guard lemmas and independent paired-circuit checks (#26). Original +source notices and historical snapshots are preserved. Neither formal package +claims a full formal proof of the multiplication algorithm or a new kappa. + +Joint frame compilation of skip-prefix strips + +The local compiler and exact finite witnesses were prepared by eumemic with +substantial OpenAI Codex assistance. Avi Eisenberg / ikeboy with Anthropic +Claude assistance supplied the unmodified PR #53 skip-prefix producer. +The pinned PR #48 pipeline is Chafik Boukhalfa's contribution, incorporating +Rohan Arun, RaD / hipotures, icekylinx, Dominik Scholz, James Chang, +Zhihao Chen, Aurel Prosz / Paureel, Swapnil Jain, eumemic, Douglas Colkitt, +OpenAI, David Harvey, Joris van der Hoeven and the earlier contributors +credited in the retained sources. See references/frame-compiler/pr48/NOTICE +and references/frame-compiler/pr53/NOTICE for their original attribution. +No authorship or review by those predecessors is claimed for this compiler. + +Joint dual-skip/frame-compiler composition (2026-10-08) +--------------------------------------------------- +Rohan Gupta / gupt1156 with Anthropic Claude assistance: PR55 dual-skip +scalar graph; original LICENSE and NOTICE are retained under +references/frame-compiler/pr55. eumemic with substantial OpenAI Codex +assistance: PR57 joint reversible frame compiler, serialized physical-word +replay and profile reconstruction. Chafik Boukhalfa with OpenAI Codex +assistance: this composition, independent integration and exact certificate. +Avi Eisenberg / ikeboy, Rohan Arun, RaD / hipotures, icekylinx, and all +predecessor authors retain the notices above and in pinned source files. +No original copyright or Apache-2.0 notice is removed. + +Ranked reclamation after the PR58 joint-dual composition (2026-10-08) +---------------------------------------------------------------- +Chafik Boukhalfa with OpenAI Codex assistance: prioritize retired physical +slots by descending current frame rank, retaining slot ID as the tie-breaker; +complete replay, exact profiles, comparison and adversarial controls. +The dedicated joint_dual_reclaim_compiler.py is derived from eumemic's PR57 +compiler. Its original shared compiler remains byte-identical. The PR55 +producer and all preceding attribution remain unchanged. The complete PR58 +comparison certificate and its original source/proof provenance are retained +under references/frame-compiler/pr58. + +Skip-prefix strip producer, 8 October 2026 +By Avi Eisenberg (ikeboy), with Anthropic Claude (Claude Opus 5.5) +assistance. The skip-prefix leave-one-out strip layout in +research/skip-strips/skip_graph.py is new. Everything else reuses Chafik +Boukhalfa's PR #43/#46/#48 research/copied-fixed pipeline, its verification +code, exact data recovery and support-order sorting, together with: +- Rohan Arun's PR #44 weighted carrier matching optimizer; +- RaD (hipotures) PR #41 alternating point order; +- every predecessor credited above. +Complete attribution and the conditional proof boundary are recorded in +research/skip-strips/PROOF.md. Original Apache-2.0 and CC0 notices remain +applicable. + +Local split-pair skip-prefix research continuation (2026-10-08) +Prepared with substantial OpenAI Codex assistance at the user's request. +New contribution: singleton/pair recursive partition refinement, finite summand +order and moment search, and verified composition with inherited paid clones. +Avi Eisenberg/ikeboy with Anthropic Claude assistance: PR53 skip-prefix strips. +Chafik Boukhalfa with OpenAI Codex assistance: PR54 original-envelope clone +specialization and PR43/46/48 checking interfaces. RaD/hipotures: PR51 +whole-chain/source-partition cloning and earlier producer/interfaces. +Rohan Arun: PR44 weighted matching and earlier fixed/reversed work, with all +stated historical AI assistance. All predecessor notices remain applicable. + +Original-envelope whole-chain clones on skip-prefix strips (research/skip-clones): +Chafik Boukhalfa, prepared with OpenAI Codex assistance. The complete-chain +source-partition clone operation is adapted from RaD / hipotures, PR #51, +with original envelopes retained here. The scalar base is Avi Eisenberg's +PR #53 skip-prefix layout, prepared with Anthropic Claude assistance. +All credited PR #43/#46/#48, PR #44 and earlier code/proof notices remain +in force. This extension is provided under the repository's Apache-2.0 terms. + +Community review checkpoint #50–#61, 8 October 2026 +Maintainer integration and independent arithmetic: Douglas Colkitt, with OpenAI Codex. +Avi Eisenberg / ikeboy: skip-prefix strip framework (#53), with Anthropic Claude. +Rohan Gupta / gupt1156: parallel order search (#50, stated Antigravity assistance) +and dual-suffix strips (#55, Anthropic Claude assistance). +Eumemic: equal-frame joint compilation and paid signal reclamation (#57), with Codex. +Chafik Boukhalfa: original-envelope paid clones (#54), composition (#58) and ranked +reclamation (#60), with Codex. Rohan Arun: order search (#52) and positive-frame +composition (#56), with Anthropic Claude and stated Codex validation assistance. +RaD / hipotures: enlarged frames, source partitions and paid whole-chain clones +(#51), with Codex. Rohan Garg / rohangar1: singleton/pair recursion and paid-clone +composition (#59), with Codex. Alejandro Zarzuelo Urdiales: exact parameter +refinement, scoped Lean arithmetic, matrix/parity and search tools (#61), with +his disclosed multi-tool and Codex assistance. +Parallel #50/#52 records are reviewed and credited without replacing the earlier +climbed-48 implementation; their exact commit history is retained. The separate +#51 witness is retained as research; its source-graph/negative-basis data proof +has not received the same full replay as #56's consumed compiler machinery. +See docs/research/community-round2-review.md for precise validation boundaries. +All earlier licenses, contributions and notices remain applicable. + +Interval strips and core-aware pair assembly + +The interval leave-one-out strips and the core-aware group-pair assembly in +research/pair-assembly were prepared by Avi Eisenberg / ikeboy with Anthropic +Claude assistance. They build on PR #53's skip-prefix pipeline and its +inherited PR #48 sources. The stacked witness in research/pair-assembly/frame +uses eumemic's PR #57 joint frame compiler unchanged; its driver and verifier +are adaptations of PR #57's skip_frame_compiler.py, skip_frame_compose.py and +verify_skip_frame.py. Original notices are retained. + +Stopped product-ring extension, 9 October 2026 +Copyright 2026 icekylinx + +The opposite-bank generic projector factorization, componentwise atom-ring +adapters, stopped recurrence and outer ordinary-interchange conversion, +aligned pair-star producer with rational centers, exact denominator-21 +grid and selected (23,23)/(24,24) composition are contributed by icekylinx +with substantial OpenAI GPT-6 Astra and Codex assistance. This extension +builds on merged PR #36, 11817ccacb564bb7f98789c20dc11d3fece207e3, and is +integrated on upstream main 56b66d58297deca1d7dd130247d720e960f77a37. + +The retained ordinary leaf uses the preceding projector, corner and +copied-center proofs. The selected two-stage topology retains Aurel Prosz +(Paureel), Swapnil Jain and Zhihao Chen's credits; the semantic assembly +retains PR #21/#23 and RaD's attribution. Paired producers, carrier matching, +original source notices and each imported license remain unchanged. + +Partial-gauge extension, 9 October 2026 +Copyright 2026 icekylinx + +The pair-first cube assembly, compatible backward frame enlargement, +partial source-gauge schedule and stopped whole-projector composition are +contributed by icekylinx with substantial OpenAI GPT-6 Astra and Codex +assistance, extending PR #104 at 948ce1510df750f4c18b96bdaef436a86f8bf834. + +The physical deferred bit word, reflected event accounting, fan-order +clarification and signed two-stage endpoint are adopted from Zhihao Chen +(jacklightChen), PR #97, e15350b66e4bf796153a68c240a6cc1b788abe3e, with +Codex assistance. Its deferred readouts, V leaves, lifted frames and frozen +witness originate in Swapnil Jain's 741e7aa078392553815df7926ee17ac5e25a8c38, +with the original Claude disclosure retained. Cyclic interval and core-aware +pair primitives build on Avi Eisenberg (ikeboy), PR #62, +ad0f25ff7b23cff7f08ad237c2254e6ecf74257e, with Anthropic Claude assistance. +Prior two-stage, copied-center, ordinary-leaf, semantic/bulk, routing and +precision credits remain in force. Imported source notices and licenses +are preserved under references/partial-gauge/; see SOURCES.json. + +Three-stage cover extension, 9 October 2026 +Copyright 2026 icekylinx + +The arbitrary-subspace Clifford frame theorem, three-stage Cayley geometry, +weighted q-adic GL cover, unit-lower weighted compiler, charged local-ring +fallback, uniform batching, internal row borrowing and exact composition +are contributed by icekylinx with substantial OpenAI GPT-6 Astra assistance. This +repository integration uses Codex assistance and extends +PR #115, cf60442983c153a3a0f5272ea4713f99eba13c86. + +The selected local complex DAG and support/label replay are adopted from +Copyright 2026 eumemic, PR #117, cbb05ce504d571546d9b7794c186a613c659c3bf, +with its original Apache-2.0 terms and Claude assistance disclosure. +The unchanged bit physical word retains Zhihao Chen (jacklightChen), +PR #97, and Swapnil Jain's underlying witness and assistance notices. +The prior opposite-bank, stopped ordinary-leaf, copied-center, topology, +semantic/bulk, precision and analytic credits remain applicable. +Original source notices and license bytes are preserved in +references/three-stage-cover/pr117/ and references/partial-gauge/. + +Paired-cube and shared-core extension, 9 October 2026 +Copyright 2026 icekylinx + +The paired-coordinate triple-cube identity, signed overlap channels, +original-source involution, coordinate-star centers, concrete frame/carrier +compiler, chronological source gauges, PR97 gauge-subset selection, +orthogonal cross-stage routing and exact supplier/assembly integration +are contributed by icekylinx with substantial OpenAI GPT-6 Astra assistance. +Repository integration uses Codex assistance and extends PR #130 at +6a9970a530119174507904e23592fd59ede19a5d. + +The substantial completed-core workspace-sharing principle is credited to +an664, PR #128, 530588a019b4a74f09180680c9e3961bf649ec89, with its reported +OpenAI Codex assistance. No source code, partition or serialized witness +from that PR is imported. The new routing and paired-motif integration +are described separately and claim no exclusive priority for broad sharing, +paired-coordinate, Fourier or carrier-matching ideas. + +Selected coarse queries restrict the retained eumemic PR #117 positive DAG; +its original Apache-2.0 and Claude assistance notices remain unchanged. +The bit word and original frames retain Zhihao Chen's PR #97 and Swapnil +Jain's frozen witness, notices and historical assistance disclosures. +Earlier generalized Clifford, three-stage, uniform weighted recursion, +ordinary-leaf, semantic/bulk, precision and analytic credits remain in force. +Source-specific license bytes are preserved under references/. + +October 9 recycled-bit integration: +DaysSky (#150), William Porter/hpst3r (#147), Thomas Marchand/Th0rgal (#146), +Rohan Gupta/gupt1156 (#148), James Chang/jamesyc (#124), SovereignSteak (#122). +The original notices and assistance disclosures are retained under research/, +including research/recycled-bit-integration/NOTICE. Andrew Barnes/Bortlesboat +(#101) repairs shared verifiers using rfu08's #64 counterexample. rfu08's +scoped finite and formal-transfer packages are included separately; they do +not establish the full multiplication theorem. Earlier and parallel credits +remain applicable. Douglas Colkitt integrated these with OpenAI Codex assistance. + +SovereignSteak PR151 independently supplies the matching gauge/recycling +composition and the selected 473/10^6 atom refinement; its original package +and assistance disclosure are retained under research/gauge-recycling/. + +October 9 coordinated-frame and completed-entrance-bank integration: +Dugongue PR186, 166a34d75e853e933855f0f7e940fe77c4bb6b8d, builds on +Chafik Boukhalfa/chafreaky's PR181, 7fb2194801e3a10f54772c7f0d5505035a4fc0ad, +and eumemic's PR168 v4, 4a3c769e5c5430e7114c4d3e099ff34664677f17. +The frozen package and prerequisite archive preserve all author, source-license +and assistance notices, including PR175's compiler optimization. DaysSky's +carrier closure, James Chang's terminal substitution and balanced assembly, +geckods' stopping refinements and all preceding framework credits remain. +Rohan Arun's PR185 bootstrap and chafreaky's PR182 bit refinement are reviewed +parallel contributions; their gains are not added to the selected witness. +Douglas Colkitt integrated the package and supplied the bank scheduling +supplement with OpenAI Codex assistance, under Apache-2.0. The all-size +interfaces remain conditional; finite verification is not full formalization. diff --git a/research/clean-two-helper-query/PROOF.md b/research/clean-two-helper-query/PROOF.md new file mode 100644 index 0000000000..e6b8c65406 --- /dev/null +++ b/research/clean-two-helper-query/PROOF.md @@ -0,0 +1,176 @@ +# Two clean helpers suffice, and are necessary, for the six-target case + +Prepared for ToikY with substantial source-aware OpenAI Codex assistance. +Apache-2.0. The dirty-capacity theorem, normalization and Gram lineage of +Nick Petalas6800 and its credited predecessors retain attribution below. + +## 1. Exact statement and changed promise + +Let K be any field of characteristic two and R=K[Q]/(Q²−1), with Q a +formal central involution. Constant invertible matrices over K are free. +A paid gate is I+QN, where N is constant, N²=0 and rank(N)≤2. +There are six public coordinates, h helpers and at most four paid gates. +Require precisely + + W(x,0)=(Qx,0) for every x in R^6. + +Helpers start at zero and return to zero; arbitrary old helper values need +not return. Under this promise the least possible h is exactly two. +The construction uses four rank-two paid gates, total paid rank eight. +We do NOT assert eight is the least total paid rank with clean helpers. + +Nick Petalas6800 proves that restored arbitrary DIRTY helpers cannot lower +the corresponding total-rank floor nine. Its even-clean question is open +in the pinned source. The new result answers this fixed six-target case, +including its minimum helper count. It changes the entrance promise and +does not contradict or reprice the dirty theorem. All dimensions, ranks +and costs here belong to the stated abstract linear query model. + +## 2. Four square-zero summands + +Use four blocks K², for a total of eight scalar coordinates. Let J be the +4-by-4 block matrix every block of which is I₂, and put P=I₈+J. +Since four is zero in K, J²=0 and P²=I₈. The diagonal blocks of P vanish; +its off-diagonal blocks equal I₂. + +For i=1,2,3,4, let U_i:K²→K⁸ embed into block i and let V_i:K⁸→K² be +block row i of P. Set R_i=U_i V_i. Then V_i U_i=0, so R_i²=0. +V_i is surjective (any one of its other three blocks is I₂), and U_i is +injective, so rank(R_i)=2 over every K. Summing block rows gives + + R_1+R_2+R_3+R_4=P. + +This is a block all-ones/rank-factorization construction, using classical +linear algebra and the credited simplex/Gram viewpoint, not a new query +alphabet or an uncharged physical gate implementation. + +## 3. Literal query word and its complete operator + +Set ε=1+Q. Then ε²=0 in R. Since R_i²=0, + + (I+R_i)(I+Q R_i)=I+ε R_i. + +Each such factor uses one allowed constant free gate and one paid gate. +The free gate is invertible with inverse itself. The paid gate is likewise +its own inverse. Products of two ε terms vanish, hence in any order + + product_i (I+R_i)(I+Q R_i)=I+εP. + +For public blocks x₁,x₂,x₃ in K² and a helper block h in K², define the +constant free basis + + C(x₁,x₂,x₃,h)=(x₁,x₂,x₃,x₁+x₂+x₃+h). + +C²=I. The block sum of C(x,h) is h, so J C(x,h)=(h,h,h,h). +It follows directly, on ALL inputs, that + + C⁻¹ P C(x₁,x₂,x₃,h)=(x₁+h,x₂+h,x₃+h,h). + +Let L be the 6-by-2 matrix obtained by stacking three copies of I₂. +The literal word applies C, the four free/paid pairs, then C⁻¹. Its full +R-linear matrix is + + W=C⁻¹(I+εP)C = [ Q I₆ εL ] + [ 0 Q I₂ ]. + +Thus W(x,0)=(Qx,0), as required, for every formal-ring x. All six public +columns and both unspecified helper columns have been stated, not just +tested on a chosen set of numerical inputs. W²=I because ε²=0 and the +characteristic is two, so the inverse restriction is identical. The +reversed literal word also supplies the inverse using allowed gates. + +There are exactly four paid gates of rank two and six free basis gates: +four I+R_i factors plus C and C⁻¹. No physical tariff is assigned to those +free bases or to preparation/ownership of the zero helpers. + +## 4. Why arbitrary dirty restoration fails + +For x=0 and h=(1,0), the output helper is (Q,0), rather than (1,0), and +each public block acquires (ε,0). Both differences are nonzero in the +formal ring. In particular the complete matrix is not diag(QI₆,I₂). +Numerically substituting Q=1 would erase exactly this distinction and is +not a test of the formal endpoint. The derivative coefficient +C⁻¹PC=[I₆,L;0,I₂] is an involution, but is not a projection: its square +is I₈ and L≠0. Applying the source's projection bound to it would discard +the clean/dirty boundary. + +## 5. No word with zero or one helper can satisfy the clean promise + +Consider ANY permitted word with h≤1, including arbitrary constant free +gates and at most four square-zero paid terms of rank at most two. +The following normalization is the one credited in source6800; here its +constant endpoint need only fix the public subspace pointwise. + +Evaluate ε=0 (equivalently Q=1) and call the constant word A. A is +invertible, and the clean promise implies A(x,0)=(x,0). Its free inverse +also fixes that subspace. Therefore replacing W by A⁻¹W preserves the +clean promise and uses no additional paid gate. + +Move all constant factors to one side, using +I+QN=(I+N)(I+εN). Conjugation by constants preserves rank and square-zero. +The normalized full matrix is I+εD, where + + D=sum_i T_i, T_i²=0, rank(T_i)≤2, + +with at most four terms. Every square-zero matrix has trace zero, hence +trace(D)=0. The clean public-column identity gives D(x,0)=(x,0). + +If h=0, D=I₆ and the full endpoint is QI₆. If h=1, for some column b +and scalar d in K the FULL coefficient is + + D=[I₆ b] + [ 0 d]. + +Since six is zero in K, trace(D)=d=0. Consequently D²=D and rank(D)=6. +The constant public-fixing shear S=[I₆,b;0,1], with S²=I, conjugates D +to diag(I₆,0). After this allowed free conjugation the normalized word +has full arbitrary-input endpoint diag(QI₆,1): it is a restored DIRTY +word with the same at-most-four paid gates and the same rank cap. + +Source6800's credited dirty-capacity necessity applies. For k=4 its +m_k=2 and six public coordinates require + + total paid rank ≥ 6+ceil(6/2)=9. + +The candidate word has total paid rank at most 4·2=8, a contradiction. +The same source theorem excludes h=0. Zero-rank padding covers words +using fewer than four gates. This proves h≥2; Section3 attains h=2. + +The new lower-bound step is the one-helper trace/projection reduction. +The dirty floor and its projection-complement proof are source6800's +work, cited rather than a new census or an independent re-certification. +The displayed reduction checks its exact hypotheses; it does not assume +that an arbitrary clean endpoint with two or more helpers is a projection. + +## 6. Evidence and limits + +This is an all-field written proof, not a proof-kernel certificate. +The new verifier is finite corroboration of the explicit word, complete +formal endpoint, inverse and premise-removal controls. Its exact executed +domains/counts are reported by generated receipts and the README after +observation. It imports and executes no predecessor scientific program. +Finite checks alone do not prove all-field feasibility or the universal +minimum-helper claim; the argument above supplies those implications. + +Initialized helper preparation, ownership, basis implementation, native +alignment, actual caller chronology, retention/restoration costs and the +complete signed supplier invoice remain separate obligations. This is no +physical saving, supplier admission, κ improvement or selected-frontier +change. All five selected assumptions remain. No general clean-capacity +classification, total-paid-rank optimum, human acceptance or formal-kernel +verification is asserted. The original native-conversion task gate is +unmet; the catalogue scope is explicitly changed and its outcome partial. + +## 7. Predecessor credit + +Nick Petalas6800 supplies the dirty theorem, projection-complement +normalization, clean-versus-dirty distinction and explicit even-clean +question. Josie Elliston6138 supplies its earlier workspace-free theorem +and workspace question; Nick6122, Cinna Davis's simplex/controller line, +Ali Romman5617's coupled Gram/block simplex and Matarener6114 retain credit. +Rank factorization, dual-number linearization, block all-ones matrices, +trace and constant shear conjugation are classical. Exact retained source +texts and their immutable foreign commit/blob/SHA pins accompany this note. +Substantial OpenAI Codex proposal, implementation, source-aware challenge, +overlap and metadata roles share source context; they are not blind or +independent human/proof-kernel acceptance. diff --git a/research/clean-two-helper-query/README.md b/research/clean-two-helper-query/README.md new file mode 100644 index 0000000000..4da5299228 --- /dev/null +++ b/research/clean-two-helper-query/README.md @@ -0,0 +1,47 @@ +# Two clean helpers for six formal query targets + +**Scoped written proof with exact finite corroboration; no new kappa.** This answers the fixed six-target initialized-clean question released by Nick Petalas [PR6800](https://github.com/CrocSwap/integer-mult-bounds/pull/6800): four rank-two square-zero calls suffice with two initialized helpers returned to zero, and two is the least helper count under those fixed call/rank caps. The minimum-helper argument uses the credited dirty theorem and a new one-helper trace/projection reduction. + +Over any characteristic-two field K, use the formal ring R=K[Q]/(Q²−1), constant free bases in GL8(K), and at most four paid gates I+Q N with N²=0 and whole-matrix rank(N)≤2. Six data coordinates are arbitrary; two helpers begin at zero and must return zero. The complete operator is + +```text +W = [[Q I6, (1+Q)L], [0, Q I2]], L = [I2; I2; I2]. +``` + +Thus W(x,0)=(Qx,0). The helper columns are part of the stated full operator: arbitrary dirty restoration fails (for example, the constant helper(1,0)). Requiring diag(QI6,I2) instead would silently return to6800's excluded dirty model. Q is a formal nontrivial central symbol, not an identity substitution. + +The word uses four rank-two calls, total paid rank8. **No total paid-rank optimality is claimed.** The helper lower bound is only for n6, at most four calls and rank cap2: zero or one clean helper is reduced by a trace/projection argument to the credited6800 dirty floor9. This needs the written argument, not a failed finite search. See [PROOF.md](PROOF.md). + +## Evidence and runtime boundary + +The first new-verifier replay passed on CPython3.12.14 in1.364seconds with20.97MiB peak resident memory, empty stderr and unchanged package hashes. These measurements check the stated budget, not a speedup against a predecessor. The new standard-library verifier uses no runtime Git, network, subprocess or predecessor-code import. Registered normal/optimized caps are120seconds each. + +- Ordered pair-polynomial matrix multiplication checks every paid whole-matrix rank/square-zero condition, all ten literal paid/free gates, the complete operator and reversed inverse word. +- A separate component-gate interpreter checks all65,536vectors of (F2[Q]/(Q²−1))^8, including all4,096zero-helper entrances:65,536forward,65,536reverse and131,072round-trip compositions. The exhaustive loop executes262,144literal words; prechecks and controls are additional executions. Its profile SHA256 is `aca44f95b5664b09d8baaf741721d05d8fca6bd4807b2edf837514514b4e3290`. +- All64binary one-helper columns pass the projection/shear reduction and scalar-trace controls. This corroborates the written reduction, not an all-word exclusion or an all-field enumeration. +- Eight controls enforce their intended rejection reason; six retain actual unequal endpoint witnesses. They distinguish invalid paid terms, missing bases/cleanup/calls, wrong endpoints, collapsing formalQ to1 and falsely extending to dirty restoration. + +The all-field construction and universal helper-minimum claim rest on the written proof and credited6800floor9, not finite testing alone. Source-aware proof and code challenges are not blind, human or proof-kernel acceptance. Final normal/optimized registered, committed-byte/export/publication and hosted-CI checks are separate delivery observations recorded in the PR/handoff when completed. Every replay emits generated receipts binding all package hashes. + +```sh +python3.12 -I -B research/clean-two-helper-query/verify.py +python3.12 -I -O -B research/clean-two-helper-query/verify.py +python3.12 -B scripts/research_package.py --package research/clean-two-helper-query +``` + +The complete original card and CHANGED/partial scope are in [TASK.json](TASK.json). [SOURCES.json](SOURCES.json) pins canonical catalogue/selected provenance only. Exact6800PROOF/README bytes in [SOURCE-PINS.json](SOURCE-PINS.json) are retained mathematical provenance, not executable predecessors. Runtime vendor inputs are package-local, so external VERIFY.inputs is empty. No selected construction or historical scientific replay is requested. + +## Distinct source contracts and credit + +6800proves that arbitrary restored dirty helpers do not improve capacity and explicitly leaves initialized-clean EVEN targets open; its existing odd n1example is not new here. Josie Elliston6138 supplies workspace-free capacity/attainment and the first n6four-rank2exclusion; Nick Petalas6122 supplies the earlier four-call Gram bound. Their results are credited inputs, not rerun. + +JoyboyBrian5007and Petalas5857already supply clean square-zero COUPLING compilation and primitive lowering, using rank-one IDEMPOTENT reflections. Their alphabet/target differs from I+Q N with square-zero N and target QI6. The card's1974GL3census and2027UT4mixed-root tariffs were compared as distinct noncentral/multilabel rank-one and restored-dirty models; no count or tariff is transferred. [CREDITS.md](CREDITS.md), [NOTICE](NOTICE) and [LICENSE](LICENSE) retain attribution. + +## Limits + +This is an abstract clean-return model, with free bases and initialized helper roles explicitly counted. It supplies no clean preparation/reservation price, physical basis implementation, native conversion, actual caller, complete invoice or full supplier. It does not justify another family expansion/search. All five selected assumptions remain; no kappa, frontier, merge, human or proof-kernel acceptance is claimed. Source-aware future/proposal exposure and substantial OpenAI Codex assistance are disclosed; this is not blind discovery or independent-end-to-end verification. + +## Open next questions + +1. **Bind one native caller and full bill.** Specify the central operator, each paid rank-two map, both basis conversions, clean preparation/return and every movement/precision/storage cost. Native contracts and a complete invoice are missing. +2. **Separate total-rank optimality from helper minimality.** Fix the same alphabet and complete allowed helper-column contract before deriving any paid-rank optimum. This one rank8word is not such a lower bound; no broader search is reserved. diff --git a/research/clean-two-helper-query/SOURCE-PINS.json b/research/clean-two-helper-query/SOURCE-PINS.json new file mode 100644 index 0000000000..dad5557ee6 --- /dev/null +++ b/research/clean-two-helper-query/SOURCE-PINS.json @@ -0,0 +1,25 @@ +{ + "schema_version": 1, + "files": [ + { + "local_path": "vendor/PR6800-PROOF.md", + "source_repository": "petalas/integer-mult-bounds", + "source_commit": "c94197e40c9e8a25f643d776160659871e5ce9ac", + "source_path": "research/restored-dirty-query-capacity/PROOF.md", + "mode": "100644", + "bytes": 6061, + "sha256": "e82afe4b80b34dcdd69b59c2104f88cf9242c8b93554442e30c35de305deff98", + "git_blob": "c5f42331896c9bfcbe348c9ecd1a5c9431503fdb" + }, + { + "local_path": "vendor/PR6800-README.md", + "source_repository": "petalas/integer-mult-bounds", + "source_commit": "c94197e40c9e8a25f643d776160659871e5ce9ac", + "source_path": "research/restored-dirty-query-capacity/README.md", + "mode": "100644", + "bytes": 7386, + "sha256": "bec1134b11d08664897821f28888dda6f88946d7ca9a405be3f95802aae26387", + "git_blob": "8df37528f5d2f9f5e818f71d30c7106c7ae43082" + } + ] +} diff --git a/research/clean-two-helper-query/SOURCES.json b/research/clean-two-helper-query/SOURCES.json new file mode 100644 index 0000000000..75ea7c3d55 --- /dev/null +++ b/research/clean-two-helper-query/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + } + ] +} diff --git a/research/clean-two-helper-query/TASK.json b/research/clean-two-helper-query/TASK.json new file mode 100644 index 0000000000..5b8cee9655 --- /dev/null +++ b/research/clean-two-helper-query/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "A scoped characteristic-two formal query result: six arbitrary data coordinates can be twisted using four rank-two square-zero paid calls and two initialized helpers returned to zero; two helpers are minimal by the written proof under these fixed call/rank caps.", + "scope_change_reason": "Take PR6800's explicitly released even-target initialized-clean boundary. This changes its restored-arbitrary-dirty premise and the original card's source alphabet; native conversion and the complete physical bill remain unprovided.", + "scope_key": "central-q-clean-n6-four-rank2-h2", + "seed": "13ec8d34f9090bc89af72876397d2d2c", + "started_at": "2026-11-06T16:34:38.195108+00:00", + "time_budget_minutes": 120, + "minimum_verification_minutes": 30, + "question": "Can two initialized clean helper coordinates attain the n=6, at-most-four, rank-at-most-two square-zero central-Q target while one or no clean helper cannot?", + "success_rule": "Provide a written all-characteristic-two-field identity, the exact full eight-coordinate operator and valid whole-matrix rank/square-zero checks; prove helper minimality using an exact reduction to the credited dirty theorem, with independent challenge and bounded verification. No total paid-rank optimality or native price is required or claimed.", + "stop_rule": "Stop at this fixed eight-coordinate construction and helper-count bound, or retain a precise failure. Do not expand a word/family search. Science cutoff 2026-11-06T18:04:38.195108+00:00; reserve the final30minutes through 2026-11-06T18:34:38.195108+00:00 for verification/handoff.", + "method": "Source-aware root proposal, separately assigned static mathematical challenge, new stdlib exact verifier and metadata/source reviews. The provisional block recipe was written during prior-session verification before fresh S3 selection; it was unexecuted and unaccepted then. No blind, independent-human, proof-kernel or independent-end-to-end claim.", + "bottleneck_link": "An exact changed clean-return contract can distinguish initialized clean workspace from the already excluded arbitrary restored-dirty query model; a finite-address identity alone still does not deliver a BIT supplier.", + "family_decision": "Only the released even-clean alternative is taken. No extension of the closed dirty model or broader family search is authorized; native conversion/full invoice gate remains unmet.", + "outcome": "partial", + "scientific_status": "SCOPED_WRITTEN_PROOF_WITH_FINITE_CORROBORATION", + "author": "ToikY", + "ai_assistance": "Substantial OpenAI Codex assistance through source-aware proposal, implementation, static challenge, overlap/credit and metadata roles. Current source6800proof/README and prior future-recipe exposure are disclosed; no blind/human/kernel acceptance.", + "credit": "Nick Petalas6800 dirty theorem and explicit even-clean question; Josie Elliston6138 workspace-free capacity/attainment and audit; Nick Petalas6122 four-call Gram theorem; Ali Romman5617, Cinna Davis simplex/controller lineage and Matarener6114 question. JoyboyBrian5007/Petalas5857 clean-coupling work and1974/2027 distinct-model predecessors remain credited context; block and dual-number algebra are classical.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19444824", + "overlap": "Root refreshed canonical7c49/revision8 and757open bodies plus live hub/index and bounded all-state searches. The role compared exact5007/5857/6138/6122 and card first examples1974/2027. Source6800OpenQ1 is explicit; hidden/unindexed work is unknown. Prior109 results plus B14S1/S2 remain excluded.", + "evidence": "Written all-field full operator W=[[Q I6,(1+Q)L],[0,Q I2]], with h2 minimal under fixedn6/k\u22644/r\u22642 by trace/projection reduction and credited6800dirtyfloor9. First actual new verifier:1.363680s/20.96875MiB,exit0,empty stderr,all12package hashes unchanged. Exhaustive65536formalF2[Q]8vectors/4096clean entrances,65536forward+65536reverse checks/131072roundtrip compositions/262144literal executions in exhaustive loop (extra prechecks/controls separate);64one-helper binary columns/8intended-reason rejecting controls with6actual endpoint witnesses. ProfileSHA aca44f95b5664b09d8baaf741721d05d8fca6bd4807b2edf837514514b4e3290. Static exact-version proof/code reviews are source-aware. Final registered/export/publication/CI are distinct delivery observations recorded separately. No predecessor checker/census ran; totalpaidrank8optimality and actual native/fullbill gates remain unmet.", + "remaining_obligations": [ + "The proposed minimum is helper count for n6,k<=4,rank<=2, not total paid-rank or physical memory optimality.", + "The helper columns of W are intentionally unspecified by clean return and are not a full dirty identity endpoint.", + "Native conversion, charged constant bases, clean resource preparation/return, actual caller and full physical bill remain missing.", + "All five selected assumptions remain; no supplier admission, multiplier, kappa or frontier change follows.", + "Source6800theorem is credited input, not independently replayed or formally verified; finite checks cannot establish universal field quantifiers alone." + ], + "open_questions": [ + { + "question": "Can this fixed four-call clean-return identity be converted to one legal native primitive with a complete paid bill?", + "why_it_matters": "Free constant bases and initialized helper roles are model assumptions, not delivered physical resources or a supplier saving.", + "first_step": "Specify the actual central involution, every rank-two paid map, both basis conversions, clean reservation/preparation/return and all movement/precision/storage work at one actual caller boundary.", + "blocked_by": "No native conversion, actual caller integration or complete physical invoice is supplied by this abstract result." + }, + { + "question": "What is the minimum total paid rank in the initialized-clean model, separately from the fixed word and minimum helper count?", + "why_it_matters": "The proposed word has four rank-two calls, but helper minimality does not prove total paid-rank optimality.", + "first_step": "Fix the same formal alphabet, call cap and complete allowed helper-column contract before deriving a lower bound; do not infer an optimum from this one witness or a failed search.", + "blocked_by": "No total paid-rank optimum is claimed or established in this contribution." + } + ] +} diff --git a/research/clean-two-helper-query/VERIFY.json b/research/clean-two-helper-query/VERIFY.json new file mode 100644 index 0000000000..93c30454f6 --- /dev/null +++ b/research/clean-two-helper-query/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact full eight-coordinate formal word, paid rank/square-zero and inverse, exhaustive65536F2[Q] vectors including4096clean entrances,64one-helper reduction cases and8intended-reason semantic controls. Finite corroboration of written all-field proof; no predecessor program replay." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat complete finite corroboration under optimized Python with explicit guards and source authentication. No runtime Git/network/subprocess; all-field/minimum-helper proof and physical obligations remain separate." + } + ] +} diff --git a/research/clean-two-helper-query/vendor/PR6800-PROOF.md b/research/clean-two-helper-query/vendor/PR6800-PROOF.md new file mode 100644 index 0000000000..c5f4233189 --- /dev/null +++ b/research/clean-two-helper-query/vendor/PR6800-PROOF.md @@ -0,0 +1,171 @@ +# Restored dirty helpers do not increase square-zero query capacity + +This contribution was produced by Nick Petalas. Apache-2.0. + +## 1. Statement and credited premise + +Let K be any field of characteristic two and let +R = K[Q]/(Q^2-1). The symbol Q is a formal central involution. +Fix n>0 target coordinates, h>=0 arbitrary dirty helper coordinates, +k>=3 available paid calls, and a nonnegative integer rank cap r. +Free gates are arbitrary constant matrices in GL_(n+h)(K). +A paid gate is I+Q N, where N is constant, N^2=0, and rank(N)<=r. +The complete required endpoint on every input is + +```text +diag(Q I_n, I_h). +``` + +Thus every original helper value must return unchanged, without a promise +on its value or correlations with the target inputs. +Put m_k=2 floor((k-1)/2). The endpoint is possible with at most k calls iff + +```text +n is even and n + ceil(n/m_k) <= k r. +``` + +Whenever feasible, its least total paid rank with at most k calls is +n+ceil(n/m_k). +Neither statement depends on h. Zero-rank calls may pad a shorter word. + +The new part is necessity for arbitrary h. Josie Elliston's +[PR #6138](https://github.com/CrocSwap/integer-mult-bounds/pull/6138), +`research/four-block-query-capacity-audit/README.md`, finding 5, supplies +the workspace-free attaining construction. We use that theorem as a cited +premise and extend its words by the identity on h helpers. We do not replay +its computations or claim its construction. Its four-call theorem credits +Nick Petalas #6122, its simplex credits Cinna Davis, its Gram framework +credits Ali Romman #5617, and its source question credits Matarener #6114. + +## 2. Normalize to a projection, keeping every helper + +Set epsilon=Q+1, so epsilon^2=0 and R=K[epsilon]/(epsilon^2). +For square-zero N, + +```text +I+Q N = (I+N)(I+epsilon N). +``` + +Move the constant factors and free gates to one side, conjugating the N's +by constant invertible matrices. Rank and square-zero are preserved. +The constant part of the required endpoint is I, so the complete endpoint +is equivalent to + +```text +sum_(i=1)^k R_i = P, +R_i^2=0, +P=diag(I_n,0_h). +``` + +All products involving two epsilon terms vanish. Conversely, such a sum +implements I+epsilon P by preceding each paid I+Q R_i with the free I+R_i. +This equivalence keeps the whole arbitrary-input matrix, including both +off-diagonal helper blocks. It does not discard helper information. + +Let r_i=rank(R_i) and S=sum r_i. Since a square-zero matrix has trace zero, +trace(P)=n times 1_K=0, so n must be even. + +## 3. The projection Gram complement + +Factor R_i=U_i V_i with U_i injective and V_i surjective through K^(r_i). +Then V_i U_i=0, since U_i(V_i U_i)V_i=R_i^2=0. +Concatenate the U_i horizontally into U and the V_i vertically into V. +Thus UV=P. Let + +```text +X=VU on K^S, Y=I_S+X, d=S-n. +``` + +The call-diagonal blocks of X vanish, so Y_ii=I_(r_i). +Although P is a projection, X need not be one. Instead, + +```text +X^3=V P^2 U=V P U=X^2, +Y^3=Y. +``` + +The fixed space of X has dimension n. Indeed, U and V restrict to inverse +maps between ker(I_S+X) and im(P). For Xv=v, P(Uv)=Uv and VUv=v. +For Pw=w, XVw=Vw and UVw=w. Therefore rank(Y)=S-n=d. + +Take a full-rank factorization Y=A B through K^d. Since Y^3=Y, +injectivity of A and surjectivity of B give + +```text +C=BA, C^2=I_d. +``` + +In particular C is invertible. Partition A into call row blocks A_i +and B into matching column blocks B_i. The call-diagonal equations give + +```text +A_i B_i=I_(r_i), +E_i=B_i A_i, E_i^2=E_i, rank(E_i)=r_i, +sum E_i=C. +``` + +Consequently r_i<=d. When h=0, the old argument can take C=I_d. +With dirty helpers, C can be a nonidentity involution I_d+Z with Z^2=0. +Invertibility, rather than identity, is the property needed below. + +## 4. The rank bound for every call count + +If k is odd, sum r_i<=k d immediately gives + +```text +(k-1) S >= k n, +S >= n + ceil(n/(k-1)). +``` + +If k is even, characteristic two gives sum(I_d+E_i)=C. +Each I_d+E_i has rank d-r_i, while C has rank d. Rank subadditivity yields + +```text +d <= sum(d-r_i) = k d-S, +(k-2) S >= (k-1) n, +S >= n + ceil(n/(k-2)). +``` + +Together these say S>=n+ceil(n/m_k). Since S<=k r, the stated uniform-cap +condition is necessary. The credited workspace-free construction proves +sufficiency and equality for total rank. This finishes the scoped theorem. + +For example, four rank-two paid calls cannot twist six independent +coordinates even when any number of arbitrary dirty helpers may be mixed +into every call and must eventually return unchanged. The new conclusion +is the independence from the helper count, not the predecessor's +workspace-free numerical bound. + +## 5. A genuine nilpotent defect and the clean-helper boundary + +Write binary matrices as integer-coded rows, with the least significant +bit the first column. The four three-by-three matrices + +```text +(0,6,6), (6,6,6), (0,5,0), (7,7,0) +``` + +are square-zero rank-one matrices with sum diag(1,1,0). Their stacked +X=VU is not idempotent, and the complement factor has C!=I but C^2=I. +The verifier reconstructs these facts without treating the coded rows as +a receipt. Thus replacing the predecessor's identity by a projection +requires the new argument in section 3. + +Initialized clean helpers have a different contract. The two-by-two terms + +```text +(2,0), (0,1), (3,3) +``` + +sum to I_2 and yield endpoint Q I_2. On (x,0) this twists one target and +returns the zero helper, despite n=1 being odd. On (x,y) it also twists y. +It therefore fails dirty restoration. The theorem does not cover a +zero-initialized helper promise, discarded outputs, nonlinear controls, +Q-dependent free gates, non-square-zero paid gates or approximate equality. + +This is an abstract query-capacity obstruction. Native implementation, +physical basis-change costs, independent stage multipliers, storage, +precision, a complete supplier invoice and the five selected framework +assumptions remain outside the claim. No new kappa or complete +multiplication theorem follows. The all-field proof is written mathematics; +finite binary checks do not provide formal proof-kernel acceptance. diff --git a/research/clean-two-helper-query/vendor/PR6800-README.md b/research/clean-two-helper-query/vendor/PR6800-README.md new file mode 100644 index 0000000000..8df37528f5 --- /dev/null +++ b/research/clean-two-helper-query/vendor/PR6800-README.md @@ -0,0 +1,131 @@ +# Exact query capacity with restored dirty helpers + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped proof with exact finite corroboration; no new kappa.** An arbitrary +finite bank of restored dirty helpers cannot lower the square-zero query +capacity in characteristic two. This answers the dirty-workspace part of +Josie Elliston's [PR #6138](https://github.com/CrocSwap/integer-mult-bounds/pull/6138), +second Open next question. Its workspace-free attaining theorem is a cited +premise, not a replay target. + +Over any characteristic-two field K, let Q be a formal central involution. +Free gates are constant invertible matrices. Each paid gate is I+Q N with +N^2=0 and rank(N)<=r. There are n>0 independent targets and any h>=0 +independent dirty helpers. The full endpoint must be diag(Q I_n,I_h). +For k>=3 available calls and m_k=2 floor((k-1)/2), feasibility is exactly + +```text +n is even and n + ceil(n/m_k) <= k r. +``` + +Whenever feasible, the least total paid rank is n+ceil(n/m_k), independently of h. +For example, adding restored dirty helpers cannot make four rank-two calls +twist six independent targets. The same capacity without helpers was +already proved by #6138; the new result is its invariance under arbitrary +finite dirty workspace. + +[PROOF.md](PROOF.md) gives the all-field argument. Normalization replaces +an identity endpoint by a projection P. The call Gram matrix X then only +satisfies X^3=X^2. Factoring Y=I+X yields an invertible complement core C +with C^2=I, rather than C=I. Its diagonal blocks still give idempotents. +Rank subadditivity recovers the same even-call bound; a separate dimension +count gives the odd-call bound. A nonidentity core occurs in the finite +fixtures, so the identity-only predecessor argument cannot be reused +without this step. + +## Evidence and reproduction + +From the repository root, with the interpreter used locally: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/restored-dirty-query-capacity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/restored-dirty-query-capacity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/restored-dirty-query-capacity +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/restored-dirty-query-capacity --check-source-history +``` + +Elsewhere substitute a CPython 3.12 path. Only the standard library is +needed. The direct verifier emits `PASS_RESTORED_DIRTY_QUERY_CAPACITY` +in a generated JSON receipt bound to the six package files' SHA256 hashes. +It writes no files and imports no predecessor program. + +- A complete three-coordinate, four-call binary fixture uses two target + coordinates and one arbitrary restored dirty helper. Pair joins and a + separate direct scan of all 234,256 ordered four-tuples both find exactly + 648 valid words. The new complement identities hold for each, including + all 288 nonidentity cores. Literal quotient-ring execution checks all + eight dirty inputs of each word, for 5,184 executions. +- Padded dirty-helper fixtures exercise each call count from three through + eight, covering both parity branches of the new rank argument. +- A separate complete two-pair minimization on four coordinates, two targets + and two dirty helpers, gives minimum total rank three for caps one and + two. It includes respectively 11,236 and 99,856 ordered pairs and retains + every pair-sum cost. It does not enumerate all ordered four-tuples in this + larger domain. +- Four rejecting controls cover a non-square-zero summand with unchanged + total, the wrong complete endpoint, a nonprojection, and the enumeration + dimension limit. A literal clean-helper example shows why a zero-input + promise does not imply dirty restoration. + +The written proof, not these small fixtures, establishes arbitrary field, +helper count and dimension. No predecessor counts were replayed as the +contribution. [SOURCES.json](SOURCES.json) pins the source question and +attainment theorem as historical provenance at canonical main +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8. + +## Limits and expansion decision + +This theorem requires exact formal equality, constant free controls, +square-zero paid terms, and restoration of every arbitrary helper input. +Initialized clean helpers, discarded helper outputs, non-square-zero paid +operations, nonlinear controls and approximation remain outside its scope. +The clean-helper example in the proof can twist one target using three +rank-one calls and a clean zero helper, while its full dirty endpoint fails. + +There is no physical multi-bank query, native alignment, charged basis +implementation, stage chronology, complete signed invoice, compiler or +precision/tape construction. The five selected framework assumptions are +unchanged. No selected cold replay, Lean or Docker run, independent human +review or formal proof-kernel acceptance is claimed. + +This closes the restored-dirty-workspace route in this model. Further +construction work needs a changed hypothesis and a complete favorable +physical bill. A larger search inside the same dirty model is unnecessary. +The non-square-zero and initialized-clean alternatives remain open and +are not assigned by this package. + +Power of Ten rule 3 has a managed-runtime deviation. Python allocates +integers, tuples and dictionaries during verification. Scientific loops +have fixed bounds: dimension at most four, at most 65,536 candidate +matrices per census, 234,256 streamed raw four-tuples, and at most 65,536 +pair-sum keys. Gram fixtures use at most eight calls and matrices of width +at most eight. There is no recursion, network operation, subprocess or +dynamic code in the verifier. Every function is below 60 physical lines. +Warning-strict normal and optimized commands are registered. The deviation +is confined to this terminating verifier; any larger search must introduce +new capacity bounds before expanding it. + +## Open next questions + +- Can initialized clean helpers reduce the paid-rank floor for even target + dimensions? This would separate clean from restored dirty capacity beyond + the odd-dimension example. First classify the permitted unspecified + helper-column blocks in a normalized endpoint. The complete endpoint and + clean-return contract need to be fixed before claiming a capacity. +- Which invertible non-square-zero paid alphabet can improve a real caller? + This is the remaining distinct branch of #6138's second question. First + specify a native gate, its complete arbitrary-input response and paid + rank. No such physical gate or profitable invoice is supplied here. + +## Credit + +Josie Elliston's #6138 supplies the question, all-call workspace-free +attainment theorem and its stated unresolved workspace boundary. Credit +Nick Petalas #6122 for the earlier four-call theorem, Cinna Davis for the +rank-one simplex and controller lineage, Ali Romman #5617 for the coupled +Gram framework and block simplex, and Matarener #6114 for the higher-rank +query question. Rank factorization, kernel correspondence and rank +subadditivity are standard linear algebra. The new contribution is the +projection-complement involution argument and the resulting sharp +restored-dirty-workspace exclusion. No predecessor credit line is changed. diff --git a/research/clean-two-helper-query/verify.py b/research/clean-two-helper-query/verify.py new file mode 100644 index 0000000000..3771691199 --- /dev/null +++ b/research/clean-two-helper-query/verify.py @@ -0,0 +1,361 @@ +#!/usr/bin/env python3 +"""Finite formal-ring corroboration for one clean-helper word; no source imports. + +Prepared for ToikY with substantial OpenAI Codex assistance. Apache-2.0. +Credit Nick Petalas PR6800, Josie Elliston PR6138, Nick Petalas PR6122, +Cinna Davis, Ali Romman PR5617 and Matarener PR6114. Rank/Gram methods are +classical. Source dirty-capacity theorem is cited, not replayed here. +""" +import hashlib +import json +from pathlib import Path +import sys + +P = Path(__file__).resolve().parent +SOURCE_HEAD = 'c94197e40c9e8a25f643d776160659871e5ce9ac' +EXPECTED_SOURCES = { + 'vendor/PR6800-PROOF.md': ('research/restored-dirty-query-capacity/PROOF.md', + 6061, 'e82afe4b80b34dcdd69b59c2104f88cf9242c8b93554442e30c35de305deff98', + 'c5f42331896c9bfcbe348c9ecd1a5c9431503fdb'), + 'vendor/PR6800-README.md': ('research/restored-dirty-query-capacity/README.md', + 7386, 'bec1134b11d08664897821f28888dda6f88946d7ca9a405be3f95802aae26387', + '8df37528f5d2f9f5e818f71d30c7106c7ae43082'), +} +OTHER = ((2, 4, 6), (0, 4, 6), (0, 2, 6), (0, 2, 4)) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def sha(raw): + return hashlib.sha256(raw).hexdigest() + + +def blob(raw): + return hashlib.sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() + + +def unique(pairs): + result = {} + for key, value in pairs: + need(key not in result, 'duplicate source metadata key: ' + key) + result[key] = value + return result + + +def bad_number(value): + raise ValueError('non-integer source metadata number: ' + value) + + +def authenticate(): + raw = (P / 'SOURCE-PINS.json').read_bytes() + pins = json.loads(raw, object_pairs_hook=unique, parse_float=bad_number, + parse_constant=bad_number) + need(type(pins.get('schema_version')) is int and pins['schema_version'] == 1, + 'source schema') + rows = pins.get('files') + need(type(rows) is list and len(rows) == 2 and + {r.get('local_path') for r in rows} == set(EXPECTED_SOURCES), 'source inventory') + observed = {} + for row in rows: + name = row['local_path'] + path, size, digest, git_blob = EXPECTED_SOURCES[name] + need(row.get('source_repository') == 'petalas/integer-mult-bounds' and + row.get('source_commit') == SOURCE_HEAD and row.get('source_path') == path + and row.get('mode') == '100644', 'source identity: ' + name) + need(type(row.get('bytes')) is int and row['bytes'] == size and + row.get('sha256') == digest and row.get('git_blob') == git_blob, + 'source pin: ' + name) + data = (P / name).read_bytes() + need(len(data) == size and sha(data) == digest and blob(data) == git_blob, + 'source bytes: ' + name) + observed[name] = digest + return sha(raw), observed + + +def identity(n): + return tuple(1 << i for i in range(n)) + + +def zero(n): + return (0,) * n + + +def add(a, b): + return tuple(x ^ y for x, y in zip(a, b)) + + +def multiply(a, b): + result = [] + for row in a: + value = 0 + while row: + low = row & -row + value ^= b[low.bit_length() - 1] + row ^= low + result.append(value) + return tuple(result) + + +def rank(matrix): + pivots = {} + for row in matrix: + while row: + p = row.bit_length() - 1 + if p not in pivots: + pivots[p] = row + break + row ^= pivots[p] + return len(pivots) + + +def trace(matrix): + result = 0 + for i, row in enumerate(matrix): + result ^= (row >> i) & 1 + return result + + +def pair_multiply(a, b): + """(A0+Q A1)(B0+Q B1), retaining both coefficients and their order.""" + return (add(multiply(a[0], b[0]), multiply(a[1], b[1])), + add(multiply(a[0], b[1]), multiply(a[1], b[0]))) + + +def product(chronological): + value = (identity(8), zero(8)) + for gate in chronological: + value = pair_multiply(gate, value) + return value + + +def check_paid(matrix): + need(len(matrix) == 8 and all(type(x) is int and 0 <= x < 256 for x in matrix), + 'paid matrix format') + need(multiply(matrix, matrix) == zero(8), 'paid square-zero') + need(rank(matrix) <= 2, 'paid rank cap') + + +def construction(): + unit = identity(8) + full = tuple(sum(1 << j for j in range(8) + if j % 2 == i % 2 and j // 2 != i // 2) for i in range(8)) + terms = tuple(tuple(full[i] if i // 2 == block else 0 for i in range(8)) + for block in range(4)) + for term in terms: + check_paid(term) + need(rank(term) == 2, 'constructed paid rank') + basis = (*unit[:6], 1 | 4 | 16 | 64, 2 | 8 | 32 | 128) + need(multiply(basis, basis) == unit and rank(basis) == 8, 'common basis inverse') + gates = [(basis, zero(8))] + for term in terms: + free, paid = (add(unit, term), zero(8)), (unit, term) + need(pair_multiply(free, free) == (unit, zero(8)), 'free inverse') + need(pair_multiply(paid, paid) == (unit, zero(8)), 'paid inverse') + gates.extend([free, paid]) + gates.append((basis, zero(8))) + helper = tuple((1 << (6 + i % 2)) if i < 6 else 0 for i in range(8)) + expected = (helper, add(unit, helper)) + forward, backward = product(gates), product(reversed(gates)) + need(forward == backward == expected, 'complete formal operator') + need(pair_multiply(forward, backward) == (unit, zero(8)), 'formal inverse') + return terms, basis, expected + + +def apply_binary(matrix, vector): + result = 0 + for i, row in enumerate(matrix): + result |= ((row & vector).bit_count() & 1) << i + return result + + +def pair_action(operator, vector): + lo = sum((x & 1) << i for i, x in enumerate(vector)) + hi = sum((x >> 1) << i for i, x in enumerate(vector)) + a = apply_binary(operator[0], lo) ^ apply_binary(operator[1], hi) + b = apply_binary(operator[0], hi) ^ apply_binary(operator[1], lo) + return tuple(((a >> i) & 1) | (((b >> i) & 1) << 1) for i in range(8)) + + +def q(value): + """Literal two-coefficient scalar multiplication by Q, Q squared equals1.""" + return ((value & 1) << 1) | (value >> 1) + + +def literal_gate(value, block, paid, q_is_one): + a, b, c = OTHER[block] + first = value[a] ^ value[b] ^ value[c] + second = value[a + 1] ^ value[b + 1] ^ value[c + 1] + if paid and not q_is_one: + first, second = q(first), q(second) + value[2 * block] ^= first + value[2 * block + 1] ^= second + + +def literal(vector, inverse=False, omit_paid=-1, omit_free=-1, + without_basis=False, q_is_one=False): + """Execute explicit component gates, without using any binary matrix routine.""" + value = list(vector) + if not without_basis: + value[6] ^= value[0] ^ value[2] ^ value[4] + value[7] ^= value[1] ^ value[3] ^ value[5] + for block in (range(3, -1, -1) if inverse else range(4)): + order = (True, False) if inverse else (False, True) + for paid in order: + if not ((paid and block == omit_paid) or + (not paid and block == omit_free)): + literal_gate(value, block, paid, q_is_one) + if not without_basis: + value[6] ^= value[0] ^ value[2] ^ value[4] + value[7] ^= value[1] ^ value[3] ^ value[5] + return tuple(value) + + +def endpoint(vector): + return tuple(q(x) ^ ((vector[6 + i % 2] ^ q(vector[6 + i % 2])) + if i < 6 else 0) for i, x in enumerate(vector)) + + +def exhaustive(operator): + digest = hashlib.sha256() + clean = 0 + for number in range(1 << 16): + value = tuple((number >> (2 * i)) & 3 for i in range(8)) + forward, backward = literal(value), literal(value, inverse=True) + expected = pair_action(operator, value) + need(forward == backward == expected == endpoint(value), 'full formal vector case') + after_forward = literal(forward, inverse=True) + after_backward = literal(backward) + need(after_forward == after_backward == value, 'literal roundtrip') + if not (value[6] or value[7]): + clean += 1 + need(forward[:6] == tuple(q(x) for x in value[:6]) and + forward[6:] == (0, 0), 'clean entrance/return') + digest.update(bytes(value + forward + backward + after_forward + after_backward)) + need(clean == 4096, 'complete clean domain') + return {'formal_vectors': 65536, 'clean_vectors': clean, + 'forward_checks': 65536, 'reverse_checks': 65536, + 'roundtrip_compositions': 131072, 'literal_word_executions': 262144, + 'profile_sha256': digest.hexdigest()} + + +def one_helper_reduction(): + unit = identity(7) + target = (*identity(6), 0) + digest = hashlib.sha256() + for column in range(64): + projection = tuple((1 << i) | (((column >> i) & 1) << 6) + for i in range(6)) + (0,) + shear = projection[:6] + (64,) + need(trace(projection) == 0 and rank(projection) == 6 and + multiply(projection, projection) == projection, 'one-helper projection') + need(multiply(shear, shear) == unit and + multiply(multiply(shear, projection), shear) == target, + 'one-helper public-fixing shear') + forbidden = projection[:6] + (64,) + need(trace(forbidden) == 1, 'one-helper nonzero scalar block trace') + digest.update(bytes(projection + shear + forbidden)) + need(rank(identity(6)) == 6, 'zero-helper projection') + return {'binary_A_columns': 64, 'projection_and_shear_cases': 64, + 'nonzero_scalar_block_trace_cases': 64, + 'profile_sha256': digest.hexdigest(), + 'minimality_basis': 'Written all-field trace/projection reduction plus cited PR6800 ' + 'dirty projection floor9; not an exhaustive word search.'} + + +class EndpointMismatch(ValueError): + def __init__(self, witness): + super().__init__('endpoint mismatch') + self.witness = witness + + +def check_contract(actual, claimed): + for index in range(8): + value = tuple(int(i == index) for i in range(8)) + got, expected = actual(value), claimed(value) + if got != expected: + raise EndpointMismatch({'input': list(value), 'actual': list(got), + 'false_claim': list(expected)}) + + +def rejection(name, call, expected_reason="endpoint mismatch"): + try: + call() + except ValueError as error: + need(str(error) == expected_reason, 'control rejected for wrong reason: ' + name) + if expected_reason == 'endpoint mismatch': + need(isinstance(error, EndpointMismatch) and + error.witness['actual'] != error.witness['false_claim'], + 'control requires an actual endpoint witness: ' + name) + result = {'name': name, 'status': 'rejected', 'reason': str(error)} + if isinstance(error, EndpointMismatch): + result['witness'] = error.witness + return result + raise ValueError('control did not reject: ' + name) + + +def controls(operator): + wrong_rank = (8, 16, 32, 0, 0, 0, 0, 0) + wrong_endpoint = ((operator[0][0] ^ 1,) + operator[0][1:], + (operator[1][0] ^ 1,) + operator[1][1:]) + dirty_claim = lambda v: tuple(q(x) if i < 6 else x for i, x in enumerate(v)) + tests = [ + rejection('non_square_zero_paid', lambda: check_paid(identity(8)), 'paid square-zero'), + rejection('paid_rank_cap', lambda: check_paid(wrong_rank), 'paid rank cap'), + rejection('omitted_common_basis', lambda: check_contract( + lambda v: literal(v, without_basis=True), endpoint)), + rejection('omitted_free_normalizer_cleanup', lambda: check_contract( + lambda v: literal(v, omit_free=0), endpoint)), + rejection('wrong_public_endpoint', lambda: check_contract( + literal, lambda v: pair_action(wrong_endpoint, v))), + rejection('missing_paid_call', lambda: check_contract( + lambda v: literal(v, omit_paid=0), endpoint)), + rejection('formal_Q_collapsed_to_one', lambda: check_contract( + lambda v: literal(v, q_is_one=True), endpoint)), + rejection('false_arbitrary_dirty_restoration', lambda: check_contract( + literal, dirty_claim)), + ] + need(len(tests) == 8, 'control count') + return tests + + +def main(): + try: + pin_sha, sources = authenticate() + terms, basis, operator = construction() + check_contract(literal, endpoint) + observed = exhaustive(operator) + helper = one_helper_reduction() + rejected = controls(operator) + receipt = {'schema_version': 1, 'status': 'PASS_CLEAN_TWO_HELPER_QUERY', + 'source_head': SOURCE_HEAD, 'source_manifest_sha256': pin_sha, + 'source_sha256': sources, 'paid_terms': [list(x) for x in terms], + 'paid_ranks': [rank(x) for x in terms], + 'constructed_paid_rank_sum': sum(rank(x) for x in terms), + 'common_basis': list(basis), + 'formal_operator': {'constant_rows': list(operator[0]), + 'Q_rows': list(operator[1])}, + 'exhaustive_F2_Q_checks': observed, 'one_helper_reduction': helper, + 'rejection_controls': rejected, + 'methods': ['Ordered pair-polynomial binary matrix multiplication', + 'Separate literal component-gate vector interpreter', + 'All65536F2[Q]/(Q2-1) input vectors; no predecessor imports'], + 'limits': 'One explicit n6/k4/r2/h2 clean construction. All-field and h2minimal ' + 'statements rest on written proofs and cited PR6800floor9. ' + 'No all-words census, paid-rank8optimality, predecessor replay, ' + 'physical/native cost, caller/supplier or frontier claim.'} + receipt['instrumentation'] = ('Python-managed fixed-size matrices and streaming finite ' + 'verification storage are not physical helper resources.') + receipt['package_sha256'] = {f.relative_to(P).as_posix(): sha(f.read_bytes()) + for f in sorted(P.rglob('*')) if f.is_file()} + print(json.dumps(receipt, sort_keys=True, separators=(',', ':'), + ensure_ascii=True, allow_nan=False)) + except (OSError, ValueError, KeyError, TypeError) as error: + print('FAIL_CLEAN_TWO_HELPER_QUERY: ' + str(error), file=sys.stderr) + raise SystemExit(1) + + +if __name__ == '__main__': + main()