diff --git a/research/partial-helper-capture/LICENSE b/research/partial-helper-capture/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/partial-helper-capture/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/partial-helper-capture/README.md b/research/partial-helper-capture/README.md new file mode 100644 index 0000000000..0e6b38f954 --- /dev/null +++ b/research/partial-helper-capture/README.md @@ -0,0 +1,115 @@ +# Partial capture of two staged544 consumers + +The temporary sum capture is exact, but does not reduce the recursive child +profile or either helper width. This answers the concrete partial-capture +question left by [PR4061](https://github.com/CrocSwap/integer-mult-bounds/pull/4061) +on its two frozen PR3945 words. No new supplier or kappa is claimed. + +## Construction and cost + +Write `x = helper600`, `y = helper601`. At the common frame `(45,)`, the +original block adds `(x+y)/4` to each of targets 175 and 183, and +`(-x+y)/4` to each of targets 123 and 202. All six registers may contain +arbitrary entering values. One exact partial capture is: + +1. Keep the four disagreeing reads into 123 and 202. +2. Set `x += y`, add `x/4` to 175 and 183, then set `x -= y`. + +The source pair returns literally to `(x,y)` before the next original event. +The eight scalar ADDs replace eight scalar ADDs. Both helpers already enter +at `(45,)`; every original read in this block occurs at that same frame and +the first native warp is later. Each of the four targets climbs from ZERO +to `(45,)` once, contributing four rank-one children. The capture retains all +four target climbs and introduces no helper climb. The disagreeing reads +keep both helper roles. + +Literal reverse cleanup contains two additional adjacent inverse shears. +Their product is the identity, so explicit cancellation recovers the original +cleanup exactly. The strongest version of this candidate has zero complete +scalar delta; keeping the unsimplified literal cleanup adds two scalar ADDs. +Both have the same native child profile and widths: + +| Invoice | Frozen word | Partial capture | +| --- | ---: | ---: | +| Rank 1 children | 2482 | 2482 | +| Rank 2 children | 712 | 712 | +| Rank 3 children | 218 | 218 | +| Rank 4 children | 109 | 109 | +| Rank 5 children | 20 | 20 | +| Rank 8 children | 8 | 8 | +| Helper widths 5 / 6 / 7 / 8 / 9 | 28 / 18 / 53 / 96 / 213 | unchanged | + +Thus the difference of the local moments `sum H_r * r^(1-a)` is exactly zero +for every exponent `a`. Helper identities, invocation endpoints and width +requests are unchanged, so this splice supplies no new owner-residual saving. +No new physical owner fill or complete supplier admission is asserted. + +The partial capture reduces target writes by two and adds two helper writes. +Each helper is still read four times in the block; its later paid native climbs +and helper role remain. Those scalar changes are not a new recursive saving. +The `0.03825` allowance discussed for PR4045's different +rank-16 replacement is not an allowance for this splice. + +## Evidence and exact scope + +The public checkers and their result files document the exact source, local +matrix, whole-word dirty-input, inverse-transpose, literal cleanup, frame and +rejection-control coverage. See [construction/DERIVATION.md](construction/DERIVATION.md) +and the separate [independent review](independent/REVIEW.md). + +The matrix identity is a written argument for arbitrary vector-valued fields +with dyadic coefficients, under the common identical frame representative. +The source bindings and whole-word tests concern exactly two finite words. +They are not a formal-kernel proof, an approximate/native phase replay, a new +owner/precision/tape/stock proof, or a new multiplication theorem. + +More generally, under the inherited monotone, single-register native contract, +any replacement with these six physical block endpoints must pay the four +targets' ZERO-to-`(45,)` transitions. Each has dimension difference one, so +four rank-one children are a sharp floor; the original block attains it. +This does not exclude a different source boundary, changed surrounding +itinerary, extra storage, a different consumer or a changed joint-child ABI. +The larger-kappa target remains open; this run stops on the zero-saving result. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/partial-helper-capture +``` + +The registered commands are self-contained within this package and also run +in an official Git-free export. Local replay, hosted CI and mathematical +acceptance are separate evidence gates. + +## Sources and credit + +Canonical base: `bb4bccbf42844d2801487450727c2f63e10d1d0f`, priority revision 6. +[SOURCE-EXPORT.json](SOURCE-EXPORT.json) maps the retained bytes to their exact +original public heads and paths; [SOURCES.json](SOURCES.json) binds their +source-only publication ancestor. These two provenance roles are distinct. + +Riquelme Soares (@hevlyo), PR4061 at +`f977a8a3dcb2983829d066a80420b7ded42d3e09`, supplies the sign-column result and +the open partial-capture question. Dugongue's PR3945 supplies the frozen words, +retained through Chris R / Clear1nsight's PR4045. Tekalign's PR4048 supplies the +same-frame capture idea. Rohan Arun's PR4076 retains the audit core written by +Sagar Thakrar, with its Arham Tahir contract lineage. The original staged-entry, +geometry, compiler, native, owner and outer credit remains in the unchanged +[predecessor note](predecessor4061/README.md) and +[source notice](source4076/NOTICE.md). + +New construction, exact checks and scoped comparison: Ross Richardson with +substantial OpenAI GPT-6.1 Sol assistance, including separate mathematical AI +contexts. AI checks are not independent human review. Apache-2.0; retained +source licenses and notices apply. The canonical investigation is +[Discussion4060](https://github.com/CrocSwap/integer-mult-bounds/discussions/4060#discussioncomment-19051443). + +## Open next questions + +A useful successor must change a source or consumer boundary so that a real +positive-rank visit or helper role disappears, then pay the changed access, +restoration and owner costs. Specify that boundary and a favorable complete +invoice before another construction. This package provides no such successor; +it does not justify a new search over the same scalar block. diff --git a/research/partial-helper-capture/SOURCE-EXPORT.json b/research/partial-helper-capture/SOURCE-EXPORT.json new file mode 100644 index 0000000000..eb63730b1b --- /dev/null +++ b/research/partial-helper-capture/SOURCE-EXPORT.json @@ -0,0 +1,68 @@ +{ + "base": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "sources": [ + { + "head": "f977a8a3dcb2983829d066a80420b7ded42d3e09", + "original_path": "research/staged544-helper600-sign-columns/README.md", + "local_path": "predecessor4061/README.md", + "sha256": "06f9a0d0f5141cb93fa6710b7573428e5b3c89358d918a32762a0a4218071a27", + "git_blob": "0ff1289a3b210e3ba27b1e354fb7983d2c548b2d" + }, + { + "head": "f977a8a3dcb2983829d066a80420b7ded42d3e09", + "original_path": "research/staged544-helper600-sign-columns/SOURCES.json", + "local_path": "predecessor4061/SOURCES.json", + "sha256": "e5822ba1b619af70e55e88a0b4bf81eddd8497bc98b5aac7b00c9d6b63b64bf9", + "git_blob": "0839f4876a67fc26084ae94d832ccd69d2b5edb7" + }, + { + "head": "f977a8a3dcb2983829d066a80420b7ded42d3e09", + "original_path": "research/staged544-helper600-sign-columns/TASK.json", + "local_path": "predecessor4061/TASK.json", + "sha256": "dc895b0394d73b8826ae02c54d8d3c8aeff5ad2b9d41aadc2c700f3be635e5e4", + "git_blob": "40e8cff79c5f4898ef66d74d32c7ec1a33138f06" + }, + { + "head": "f977a8a3dcb2983829d066a80420b7ded42d3e09", + "original_path": "research/staged544-helper600-sign-columns/VERIFY.json", + "local_path": "predecessor4061/VERIFY.json", + "sha256": "498a515150648097231c79926e12aaeaf5334727260b7dd755daf225967ea78d", + "git_blob": "97440ad70b5310729a449cd17ae7c964971fda9a" + }, + { + "head": "f977a8a3dcb2983829d066a80420b7ded42d3e09", + "original_path": "research/staged544-helper600-sign-columns/verify.py", + "local_path": "predecessor4061/verify.py", + "sha256": "e7ce561154d679b66f025e999ffe7f3861c4ab9592fc36131a24e5fe124f7e79", + "git_blob": "7a2dd9f306885d0168a8e31c89f30cf68919d90a" + }, + { + "head": "f977a8a3dcb2983829d066a80420b7ded42d3e09", + "original_path": "research/staged544-helper600-sign-columns/frozen/WORD-base.json.gz", + "local_path": "predecessor4061/frozen/WORD-base.json.gz", + "sha256": "08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0", + "git_blob": "806784bf99d9d15004d2d227d06268556a0726c8" + }, + { + "head": "f977a8a3dcb2983829d066a80420b7ded42d3e09", + "original_path": "research/staged544-helper600-sign-columns/frozen/WORD-extra.json.gz", + "local_path": "predecessor4061/frozen/WORD-extra.json.gz", + "sha256": "d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299", + "git_blob": "c531be7383ad3ba941600c7ced14e5e10d6d1c67" + }, + { + "head": "9744f9df268590295a9872b1952c695a678192b9", + "original_path": "research/staged544-triple-entry-fill/vendor/audit_core.py", + "local_path": "source4076/vendor/audit_core.py", + "sha256": "888679ca8502cdcb100420fe5382a052529a494bf76cb332928b86e62612b951", + "git_blob": "8b5e1d5f2a106402f036b63028ecef31a4e4c462" + }, + { + "head": "9744f9df268590295a9872b1952c695a678192b9", + "original_path": "research/staged544-triple-entry-fill/NOTICE.md", + "local_path": "source4076/NOTICE.md", + "sha256": "91f7f723bb616aca757812f940f6b893559e64e441d6158c907155a79b3b15a7", + "git_blob": "9ccffcfb7da1e36b158752ffed293dc95797e68e" + } + ] +} diff --git a/research/partial-helper-capture/SOURCES.json b/research/partial-helper-capture/SOURCES.json new file mode 100644 index 0000000000..adf8ce209a --- /dev/null +++ b/research/partial-helper-capture/SOURCES.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "source_export_notice": "Local freeze pins are publication ancestors. SOURCE-EXPORT.json separately records original public PR heads, paths, Git blobs and exact-byte equality.", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "research/partial-helper-capture/SOURCE-EXPORT.json", + "usage": "input", + "pin": "head:f0631e4329ef4124c498fe3d1c500aab34ce6490:research/partial-helper-capture/SOURCE-EXPORT.json", + "git_blob": "eb63730b1b7c24d22b8a011f72939e9dd409c4c5", + "sha256": "c436ab59a73ea967782912955787e1f83ce18a14d1a1baa3a6d2520f57ab5b23" + }, + { + "path": "research/partial-helper-capture/LICENSE", + "usage": "input", + "pin": "head:f0631e4329ef4124c498fe3d1c500aab34ce6490:research/partial-helper-capture/LICENSE", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "path": "research/partial-helper-capture/predecessor4061/README.md", + "usage": "input", + "pin": "head:f0631e4329ef4124c498fe3d1c500aab34ce6490:research/partial-helper-capture/predecessor4061/README.md", + "git_blob": "0ff1289a3b210e3ba27b1e354fb7983d2c548b2d", + "sha256": "06f9a0d0f5141cb93fa6710b7573428e5b3c89358d918a32762a0a4218071a27" + }, + { + "path": "research/partial-helper-capture/predecessor4061/SOURCES.json", + "usage": "input", + "pin": "head:f0631e4329ef4124c498fe3d1c500aab34ce6490:research/partial-helper-capture/predecessor4061/SOURCES.json", + "git_blob": "0839f4876a67fc26084ae94d832ccd69d2b5edb7", + "sha256": "e5822ba1b619af70e55e88a0b4bf81eddd8497bc98b5aac7b00c9d6b63b64bf9" + }, + { + "path": "research/partial-helper-capture/predecessor4061/TASK.json", + "usage": "input", + "pin": "head:f0631e4329ef4124c498fe3d1c500aab34ce6490:research/partial-helper-capture/predecessor4061/TASK.json", + "git_blob": "40e8cff79c5f4898ef66d74d32c7ec1a33138f06", + "sha256": "dc895b0394d73b8826ae02c54d8d3c8aeff5ad2b9d41aadc2c700f3be635e5e4" + }, + { + "path": "research/partial-helper-capture/predecessor4061/VERIFY.json", + "usage": "input", + "pin": "head:f0631e4329ef4124c498fe3d1c500aab34ce6490:research/partial-helper-capture/predecessor4061/VERIFY.json", + "git_blob": "97440ad70b5310729a449cd17ae7c964971fda9a", + "sha256": "498a515150648097231c79926e12aaeaf5334727260b7dd755daf225967ea78d" + }, + { + "path": "research/partial-helper-capture/predecessor4061/verify.py", + "usage": "input", + "pin": "head:f0631e4329ef4124c498fe3d1c500aab34ce6490:research/partial-helper-capture/predecessor4061/verify.py", + "git_blob": "7a2dd9f306885d0168a8e31c89f30cf68919d90a", + "sha256": "e7ce561154d679b66f025e999ffe7f3861c4ab9592fc36131a24e5fe124f7e79" + }, + { + "path": "research/partial-helper-capture/predecessor4061/frozen/WORD-base.json.gz", + "usage": "input", + "pin": "head:f0631e4329ef4124c498fe3d1c500aab34ce6490:research/partial-helper-capture/predecessor4061/frozen/WORD-base.json.gz", + "git_blob": "806784bf99d9d15004d2d227d06268556a0726c8", + "sha256": "08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0" + }, + { + "path": "research/partial-helper-capture/predecessor4061/frozen/WORD-extra.json.gz", + "usage": "input", + "pin": "head:f0631e4329ef4124c498fe3d1c500aab34ce6490:research/partial-helper-capture/predecessor4061/frozen/WORD-extra.json.gz", + "git_blob": "c531be7383ad3ba941600c7ced14e5e10d6d1c67", + "sha256": "d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299" + }, + { + "path": "research/partial-helper-capture/source4076/vendor/audit_core.py", + "usage": "input", + "pin": "head:f0631e4329ef4124c498fe3d1c500aab34ce6490:research/partial-helper-capture/source4076/vendor/audit_core.py", + "git_blob": "8b5e1d5f2a106402f036b63028ecef31a4e4c462", + "sha256": "888679ca8502cdcb100420fe5382a052529a494bf76cb332928b86e62612b951" + }, + { + "path": "research/partial-helper-capture/source4076/NOTICE.md", + "usage": "input", + "pin": "head:f0631e4329ef4124c498fe3d1c500aab34ce6490:research/partial-helper-capture/source4076/NOTICE.md", + "git_blob": "9ccffcfb7da1e36b158752ffed293dc95797e68e", + "sha256": "91f7f723bb616aca757812f940f6b893559e64e441d6158c907155a79b3b15a7" + } + ] +} diff --git a/research/partial-helper-capture/TASK.json b/research/partial-helper-capture/TASK.json new file mode 100644 index 0000000000..ecfa60c388 --- /dev/null +++ b/research/partial-helper-capture/TASK.json @@ -0,0 +1,73 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 6, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. 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", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "refined", + "actual_scope": "Construct and price the partial helper600/601 capture for consumers175/183 left open by PR4061, preserving123/202, on both frozen PR3945 words.", + "scope_change_reason": "Handoff-first selection: PR4061 already excludes a full signed-column merge but leaves this concrete partial capture unpriced. This tests whether changed consumer sharing removes actual recursive children; it is not another rank16 or scalar census.", + "bottleneck_link": "A same-frame partial capture can matter only if its fully completed frame/helper/restoration invoice strictly improves. The complete paid-profile delta, not the two fewer targetwrites, decides this mechanism.", + "budget_minutes": 240, + "stop_rule": "Stop when the exact partial capture is verified but a complete native/helper/restoration comparison has no favorable delta, or when legal frames/dirty restoration fail. Do not extend to unrelated pairs or spend the remaining budget on a new round.", + "outcome": "negative-result", + "evidence": "Both complete723-coordinate symbolic words in forward/inverse-transpose/reverse propagation, literal and certified canceled cleanup; separate6x6 rational matrices and completeRREF frame ledger; written sharp fixed-boundary4H1 floor. Public result files and defect-sensitive controls are under construction/ and independent/.", + "author": "Ross Richardson", + "ai_assistance": "Substantial OpenAI GPT-6.1 Sol assistance, including separate mathematical AI derivations/checks; not independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Can a changed consumer/source boundary remove a positive-rank visit or a helper while also serving the disagreeing consumers?", + "why_it_matters": "The tested same-frame partial capture leaves both helper roles and every paid rank unchanged.", + "first_step": "Propose one exact boundary change with its frame/source contracts and fully charged favorable native/owner/restoration invoice before another construction.", + "blocked_by": "No such changed complete boundary is provided by this package; existing full-column sign and fixed-word restrictions remain scoped." + } + ], + "result_scope": "Finite source-bound word certificates and a written fixed-endpoint native-cost proof; no formal-kernel, physical supplier, improved owner fill, newkappa or selected-frontier claim." +} diff --git a/research/partial-helper-capture/VERIFY.json b/research/partial-helper-capture/VERIFY.json new file mode 100644 index 0000000000..5790426883 --- /dev/null +++ b/research/partial-helper-capture/VERIFY.json @@ -0,0 +1,63 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/partial-helper-capture/SOURCE-EXPORT.json", + "research/partial-helper-capture/LICENSE", + "research/partial-helper-capture/predecessor4061/README.md", + "research/partial-helper-capture/predecessor4061/SOURCES.json", + "research/partial-helper-capture/predecessor4061/TASK.json", + "research/partial-helper-capture/predecessor4061/VERIFY.json", + "research/partial-helper-capture/predecessor4061/verify.py", + "research/partial-helper-capture/predecessor4061/frozen/WORD-base.json.gz", + "research/partial-helper-capture/predecessor4061/frozen/WORD-extra.json.gz", + "research/partial-helper-capture/source4076/vendor/audit_core.py", + "research/partial-helper-capture/source4076/NOTICE.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/construction/verify.py" + ], + "timeout_seconds": 120, + "checks": "Both frozen words;723 dirty coordinates, forward/inverse-transpose/reverse traversals, literal and canceled cleanup, native profile and rejection witnesses." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-O", + "{package}/construction/verify.py" + ], + "timeout_seconds": 120, + "checks": "Both frozen words;723 dirty coordinates, forward/inverse-transpose/reverse traversals, literal and canceled cleanup, native profile and rejection witnesses. Optimized Python control." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent/check.py" + ], + "timeout_seconds": 120, + "checks": "Separate exact6x6 dirty-input matrices, RREF full frame/width ledger, sharp fixed-boundary4H1 floor and defect-sensitive controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-O", + "{package}/independent/check.py" + ], + "timeout_seconds": 120, + "checks": "Separate exact6x6 dirty-input matrices, RREF full frame/width ledger, sharp fixed-boundary4H1 floor and defect-sensitive controls. Optimized Python control." + } + ] +} diff --git a/research/partial-helper-capture/construction/DERIVATION.md b/research/partial-helper-capture/construction/DERIVATION.md new file mode 100644 index 0000000000..3a0b5b0219 --- /dev/null +++ b/research/partial-helper-capture/construction/DERIVATION.md @@ -0,0 +1,287 @@ +# Partial capture of helpers 600 and 601 + +The explicit partial sum capture is exact on both frozen words, including all +dirty inputs. Its best certified cleanup has **zero change in the paid recursive +profile, ordered helper widths, and scalar primitive count**. This concrete +capture therefore supplies no exponent-saving mechanism. This is a scoped +construction and cost test, not a lower bound for captures with changed boundary +frames or a changed child interface. + +## Pins and exact covered model + +The immutable source-only freeze is +`f0631e4329ef4124c498fe3d1c500aab34ce6490`. The two compressed PR3945 words are +the bytes exported by PR4061 head +`f977a8a3dcb2983829d066a80420b7ded42d3e09`: + +| File under `predecessor4061/frozen/` | SHA-256 | +| --- | --- | +| `WORD-base.json.gz` | `08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0` | +| `WORD-extra.json.gz` | `d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299` | + +The exact semantics, chronological binary frames, and literal cleanup generator +are imported from the retained `source4076/vendor/audit_core.py`, SHA-256 +`888679ca8502cdcb100420fe5382a052529a494bf76cb332928b86e62612b951`, at source +PR4076 head `9744f9df268590295a9872b1952c695a678192b9`. The verifier checks all +three hashes before importing or evaluating them. It does not change the source +words or the source checker. + +There are 632 live independent inputs: sources 0 through 111, targets 112 through +223, and 408 live helpers among 224 through 703. The 72 removed helpers are +absent. Each of the 91 declared private buffers, at its retained helper number +plus 704, is also an independent arbitrary input. The exact checks therefore +cover 723 independent coordinates, not just clean helpers or zero buffers. +Coefficients are dyadic rationals. The 72 native operators are independent +invertible noncommuting symbols; cancellation uses only adjacent inverse pairs. + +## Reconstructible edit + +Every index below is zero-based. In each frozen word replace exactly `B[77:85]` +by the following eight ADD records, all on common frame `[45]`: + +```text +202 -= 600/4 # retained exception read, originally B78 +123 -= 600/4 # retained exception read, originally B80 +202 += 601/4 # retained exception read, originally B82 +123 += 601/4 # retained exception read, originally B84 +600 += 601 # capture +183 += 600/4 # agreeing consumer +175 += 600/4 # agreeing consumer +600 -= 601 # undo +``` + +The four exception ADD records are byte-identical to their predecessor records. +The two removed records are the agreeing reads of 601 into 183 and 175. The B +list still has 1870 records, so every native warp position is unchanged. All +other forward word fields, including A, wrappers, compensation, cut, restore, +entrance/terminal frames, removed helpers, and initial operator corrections, +remain unchanged. The cleanup is derived separately below. + +## Current pullbacks and arbitrary-input identity + +Write `a` and `b` for the values in helpers 600 and 601 on entry to B77. Neither +helper is touched in A or in B before this block. The wrappers and cut do not +write these helpers. Consequently their current pullbacks are exactly their +original independent dirt `a = x_600`, `b = x_601`. Neither has zero input merely +because a frame is declared. No native operator occurs within this block; the +first native B warp is at position 250. + +The predecessor's eight reads add `(b-a)/4` to each exception consumer 123 and +202, and `(a+b)/4` to each agreeing consumer 175 and 183. The new block first +performs the four exception reads. It then changes `(a,b)` to `(a+b,b)`, uses the +captured sum twice, and applies the exact inverse shear. Its endpoint map is + +```text +123 -> 123 + (-a+b)/4 +175 -> 175 + ( a+b)/4 +183 -> 183 + ( a+b)/4 +202 -> 202 + (-a+b)/4 +600 -> a +601 -> b +``` + +Target values on block entry are arbitrary. They are never read by the changed +block, so reordering its target additions introduces no cross term. If T is the +four-target vector in the order 123, 175, 183, 202, and H is `(a,b)`, the complete +local matrix is + +```text +M = [[I_4, C], [0, I_2]], +C = (1/4) * [[-1,1], [1,1], [1,1], [-1,1]]. +``` + +Its inverse transpose is `[[I_4,0],[-C^T,I_2]]`. Equivalently, chronological dual +propagation replaces each `dst += q src` by `src -= q dst`. Thus the partial +capture is a local equality on all six independent values, including both +dirty helpers, and in both orientations. This is not a permanent raw-dirt +change `A_new = A_old S`: the intermediate capture and its undo have joint +source map I at the block endpoint. The target-dirt compensation remains +exactly the predecessor's map because the entire local block map is equal, +rather than because any compensation direction was guessed. + +The rational six-coordinate identity in `verify.py` is separate from the +imported whole-word evaluator. Full evaluation then checks both frozen words, +both cleanup choices below, and both orientations over the free group algebra. +Every one of the 723 output rows and 723 input columns is covered. A separate +reverse traversal checks the forward matrix by pulling back every input column. +Both words have exactly the declared complete forward map +`target_i += source_i`, with all other live and private-buffer coordinates +unchanged; their inverse transposes have `source_i -= target_i`. This includes +arbitrary private-buffer inputs: they have identity self-map and no leak. +The entire 723-coordinate state at the cleanup boundary also matches the +predecessor, including its restored-helper isolation contract. + +## Cut/frame legality and helper identities + +Both helpers enter the word at frame `span(45)`. Their old four reads and all +six new uses remain at this same frame. The added shears therefore require no +positive frame climb. Each of the four targets still needs its first climb +from the zero frame to `span(45)`; reducing two repeated reads removes none of +these target climbs. All following source productions and target reads occur +after the helpers have been restored to their original current values. + +There is also a small fixed-contract floor: a monotone scalar rewrite on these +six registers with the same block entrance and exit frames must take each of +the four targets from dimension 0 to dimension 1. Under the inherited rule +that native charges are counted per register, each requires one rank-1 climb, +so the block costs at least `4 H_1`. Native frame warps preserve dimension and +cannot supply these climbs. The predecessor and this capture both attain the +floor. This statement fixes the six-register boundary and monotone native +contract; it is not a barrier against changing that boundary or using a +different joint native interface. + +The checker walks every gate in chronological order, including native frame +warps, and rechecks the lifted binary-frame action. It checks dyadic/access +hygiene, the unchanged target cut, and each declared endpoint. The old and new +positive frame transitions agree register by register, including their exact +subspace masks. Ordered helper identities and their entrance/terminal masks +also agree, not merely their multiset of widths. Helpers 600 and 601 each keep +entrance dimension 1, terminal dimension 9, and width 8, with positive climbs +`4,1,1,1,1`. Neither helper is removed or mapped to a private restoration buffer. + +This binary-frame verification is not a native Clifford-phase certificate or +an owner-allocation proof. + +## Literal reverse-inverse cleanup and certified cancellation + +Cleanup is first regenerated by reversing the **complete changed** invertible +non-target word and inverting every gate under the inherited target/prelude +exclusions. The two added forward source shears are not silently omitted. +Their inverses are adjacent in cleanup because the intervening forward gates +write only targets and are excluded by the inherited cleanup contract. + +On both words the literal cleanup has 5227 records. At zero-based cleanup +indices 1225 and 1226 it contains + +```text +600 += 601 # inverse of the forward undo +600 -= 601 # inverse of the forward capture +``` + +Both are at the full nine-dimensional frame. The private-buffer remapping is +the identity for these two helpers. This adjacent pair is exactly I on +arbitrary values. Removing **that explicit pair only** reproduces the frozen +5225-record cleanup byte for byte. This is a certified adjacent cancellation, +not an assertion that a newly added source gate is absent from the literal +inverse. Both the 5227-record literal cleanup and the canceled cleanup pass +the full arbitrary-input forward and inverse-transpose checks. + +The frozen cleanup is consequently semantically valid for this changed word. +Calling it the unmodified literal reverse-inverse list is a representation +error; calling it the result of the exhibited cancellation is correct. + +## Complete paid deltas + +The complete recomputed paid profile on each word is + +```text +2482 H_1 + 712 H_2 + 218 H_3 + 109 H_4 + 20 H_5 + 8 H_8. +``` + +The helper width inventory is `28 W_5 + 18 W_6 + 53 W_7 + 96 W_8 + 213 W_9`, +with all 408 helper identities and endpoint masks retained. For both cleanup +choices the profile and every ordered helper width are unchanged. Hence the +rank moment `sum_r c_r r^p` changes by exactly zero for every exponent p. + +| Executed records | Predecessor | Literal cleanup | Canceled cleanup | +| --- | ---: | ---: | ---: | +| Prefix ADD | 11597 | 11597 | 11597 | +| Cleanup ADD | 4633 | 4635 | 4633 | +| Complete ADD | 16230 | 16232 | 16230 | +| Complete SCALE | 1164 | 1164 | 1164 | +| Complete WARP | 168 | 168 | 168 | +| Initial operator-correction records | 36 | 36 | 36 | +| Complete records | 17598 | 17600 | 17598 | + +The 168 WARP count includes the implicit native B warps. The 36 initial +operator-correction records are high-level records; this table does not +relabel them as scalar gates. Their source accesses, operator words and any +expanded wrappers are unchanged, so their expanded delta is zero. In the +changed local block two target ADDs are exchanged for two helper ADDs. The +literal cleanup adds two ADDs; the explicit cancellation removes those two. +No paid source visit, recursive child, helper width, correction, or restoration +charge is eliminated. Even the strongest verified cleanup therefore has no +positive recursive saving to transfer to a larger kappa. + +## Defect-sensitive controls and reproduction + +On each word the verifier actually changes the relevant gates and rejects: + +- Missing the forward capture undo, with downstream warp positions retimed + and cleanup regenerated: the exact map acquires coefficient `-1/2` from + entering helper 601 to target 123. +- Capturing a difference instead of a sum, with the matching inverse undo: + the same dirty-input coefficient is wrong by `-1/2`. +- Deleting just one member of the literal inverse pair: the final map + acquires coefficient `1` from entering helper 601 to helper 600. +- Giving the capture shear incomparable frame `[51]`: chronological frame + containment fails at B81 on helper 600. +- Describing the canceled/frozen cleanup as the literal reverse-inverse list: + literal-list equality rejects it, while the checker explicitly confirms + that its semantic map passes with the cancellation certificate. + +From the repository root: + +```sh +python3 -B research/partial-helper-capture/construction/verify.py +python3 -O -B research/partial-helper-capture/construction/verify.py +``` + +Both commands compare fresh exact results to `RESULT.json`; neither changes +the frozen inputs or the committed result. The verifier uses explicit checks, +not Python assertions. An external checkpoint stage may write a separate +fresh result using + +```sh +python3 -B research/partial-helper-capture/construction/verify.py --output /ABSOLUTE/PATH/result.json +``` + +The marker is `PASS_PARTIAL_HELPER_CAPTURE`; the deterministic result includes +the verifier hash, source hashes, both derived word hashes, exact matrix +hashes, the cleanup cancellation location, and rejecting witnesses. + +## Scope, stop rule, and remaining obligations + +The local written identity applies over any additive module with central +dyadic scalars. The global certificate is a complete symbolic linear-map and +frame check for these two fixed words; it is not a search over all possible +captures, a formal-kernel proof, or an all-size multiplication theorem. + +The decisive stop rule fires because this partial capture removes no paid +child or helper width even after the best explicit cleanup cancellation. +No new kappa, selected-frontier change, or improved owner fill is claimed. +Physical native phases, compiler/common-label realization, the full owner's +chronological allocation, precision/source-access implementation, and an +all-size recursive/outer transfer remain inherited or unverified obligations. +Equal ordered widths alone would not certify a changed owner schedule. This +package does not charge an optimistic owner reuse as an additional gain. + +**Open next questions:** any successful use of this pair must change a further +paid boundary, child rank, restoration path, or helper requirement. This +package provides no such change and undertakes no broader optimization. + +## Sources and credit + +- Dugongue / PR3945 supplies the two complete supplier words and their + inherited staged/terminal, restoration, owner and native framework. +- Riquelme Soares (@hevlyo) / PR4061 supplies the exact frozen inputs and + signed-consumer test. Its explicit open question is partial capture of + agreeing consumers 175/183 while retaining exceptions 123/202. +- Chris R / Clear1nsight / PR4045 identifies this helper group and its + support-restricted interface; no result from its allowance screen is + strengthened here. +- PR4061 credits Tekalign / PR4048 for the same-frame signed-capture idea. + Its global-sign mechanism does not directly apply to the disagreeing + columns. The new contribution here is the displayed partial capture, + its literal inverse/cancellation, complete dirty-input comparison, and + the exact zero-profile result. +- Rohan Arun / PR4076 retains the imported audit core. That core is Sagar + Thakrar's PR3687 code and credits Arham Tahir's coupled-carrier audit for + its frame/word contract. It is reused source code, not a newly independent + implementation. The separate rational six-cell calculation and reverse + column traversal are identified above without claiming independent human + review. + +Retain the package Apache-2.0 license and all predecessor notices. The new +construction, verifier and write-up were prepared with substantial OpenAI +Codex assistance. No independent human review is claimed. diff --git a/research/partial-helper-capture/construction/RESULT.json b/research/partial-helper-capture/construction/RESULT.json new file mode 100644 index 0000000000..a092fa27d0 --- /dev/null +++ b/research/partial-helper-capture/construction/RESULT.json @@ -0,0 +1,797 @@ +{ + "audit_core_source4076_head": "9744f9df268590295a9872b1952c695a678192b9", + "conclusion": { + "canceled_scalar_add_delta": 0, + "complete_paid_rank_moment_delta": "0 for every exponent p", + "literal_scalar_add_delta": 2, + "new_kappa_claim": false, + "ordered_helper_width_change": false, + "stop_rule": "This concrete partial capture removes no recursive child charge or helper width." + }, + "domain": { + "coefficient_ring": "dyadic rationals over the free group algebra", + "formal_kernel_claim": false, + "independent_coordinates": 723, + "independent_native_operator_symbols": 72, + "live_dirty_inputs": 632, + "phase_claim": false, + "private_buffer_inputs": 91 + }, + "edit": { + "all_other_forward_fields_unchanged": true, + "field": "B", + "new": [ + [ + "add", + 202, + 600, + -1, + 4, + [ + 45 + ] + ], + [ + "add", + 123, + 600, + -1, + 4, + [ + 45 + ] + ], + [ + "add", + 202, + 601, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 123, + 601, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 600, + 601, + 1, + 1, + [ + 45 + ] + ], + [ + "add", + 183, + 600, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 175, + 600, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 600, + 601, + -1, + 1, + [ + 45 + ] + ] + ], + "old": [ + [ + "add", + 183, + 600, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 202, + 600, + -1, + 4, + [ + 45 + ] + ], + [ + "add", + 175, + 600, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 123, + 600, + -1, + 4, + [ + 45 + ] + ], + [ + "add", + 183, + 601, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 202, + 601, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 175, + 601, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 123, + 601, + 1, + 4, + [ + 45 + ] + ] + ], + "warp_positions_unchanged": true, + "zero_based_half_open_slice": [ + 77, + 85 + ] + }, + "local_identity": { + "123": { + "123": "1", + "600": "-1/4", + "601": "1/4" + }, + "175": { + "175": "1", + "600": "1/4", + "601": "1/4" + }, + "183": { + "183": "1", + "600": "1/4", + "601": "1/4" + }, + "202": { + "202": "1", + "600": "-1/4", + "601": "1/4" + }, + "600": { + "600": "1" + }, + "601": { + "601": "1" + } + }, + "predecessor4061_head": "f977a8a3dcb2983829d066a80420b7ded42d3e09", + "schema_version": 1, + "source_freeze_commit": "f0631e4329ef4124c498fe3d1c500aab34ce6490", + "source_sha256": { + "predecessor4061/frozen/WORD-base.json.gz": "08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0", + "predecessor4061/frozen/WORD-extra.json.gz": "d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299", + "source4076/vendor/audit_core.py": "888679ca8502cdcb100420fe5382a052529a494bf76cb332928b86e62612b951" + }, + "status": "exact_partial_capture_with_zero_recursive_profile_gain", + "verifier_sha256": "d9335bfeed8db914404adb486797829f9913b8c00a5210c00be45e29a4cdab64", + "words": { + "base": { + "algebra": { + "cleanup_boundary": { + "all_723_rows_equal": true, + "target_and_restored_helper_contract": true + }, + "forward": { + "all_rows_equal": true, + "full_contract": true, + "independent_coordinates": 723, + "matrix_sha256": "2b92555ebf438c5a563252ded44e6950831a1576102e646f5b3dbd58978a2c26", + "nonzero_coefficients": 835 + }, + "inverse_transpose": { + "all_rows_equal": true, + "full_contract": true, + "independent_coordinates": 723, + "matrix_sha256": "4cfd33e94d6339f31b6ee00850ad8574f26d0d29a18d59dac84f01f1e6fd4f6c", + "nonzero_coefficients": 835 + }, + "reverse_column_traversal": { + "all_three_words_match_forward": true, + "input_columns": 723 + } + }, + "cleanup": { + "adjacent_pair_zero_based_index": 1225, + "deleting_exact_pair_equals_predecessor_cleanup": true, + "literal_reverse_inverse_verified": true, + "pair": [ + [ + "add", + 600, + 601, + 1, + 1, + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ], + [ + "add", + 600, + 601, + -1, + 1, + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ] + ] + }, + "frozen_file_sha256": "08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0", + "paid": { + "capture_helpers": { + "600": { + "entrance_dimension": 1, + "positive_climbs": [ + 4, + 1, + 1, + 1, + 1 + ], + "terminal_dimension": 9, + "width": 8 + }, + "601": { + "entrance_dimension": 1, + "positive_climbs": [ + 4, + 1, + 1, + 1, + 1 + ], + "terminal_dimension": 9, + "width": 8 + } + }, + "live_helpers": 408, + "local_block": { + "entrance_dimensions": { + "123": 0, + "175": 0, + "183": 0, + "202": 0, + "600": 1, + "601": 1 + }, + "exit_dimensions": { + "123": 1, + "175": 1, + "183": 1, + "202": 1, + "600": 1, + "601": 1 + }, + "helper_positive_climbs": 0, + "paid_profile": { + "1": 4 + }, + "target_rank1_climbs": 4 + }, + "ordered_helper_contract_sha256": "aea056c5a94af736eb9444d8b31de404b43d10eff9609be39e6c7803713ccee4", + "positive_frame_transitions_sha256": "b2565bd405e75cbb414230aba76beb374caa8b654e64c826e9a777a9822d7a68", + "profile": { + "1": 2482, + "2": 712, + "3": 218, + "4": 109, + "5": 20, + "8": 8 + }, + "width_inventory": { + "5": 28, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + } + }, + "primitive_counts": { + "canceled": { + "cleanup": { + "add": 4633, + "scale": 520, + "warp": 72 + }, + "cleanup_records": 5225, + "complete": { + "add": 16230, + "corr": 36, + "scale": 1164, + "warp": 168 + }, + "complete_records": 17598, + "prefix": { + "add": 11597, + "corr": 36, + "scale": 644, + "warp": 96 + }, + "prefix_records": 12373 + }, + "literal": { + "cleanup": { + "add": 4635, + "scale": 520, + "warp": 72 + }, + "cleanup_records": 5227, + "complete": { + "add": 16232, + "corr": 36, + "scale": 1164, + "warp": 168 + }, + "complete_records": 17600, + "prefix": { + "add": 11597, + "corr": 36, + "scale": 644, + "warp": 96 + }, + "prefix_records": 12373 + }, + "predecessor": { + "cleanup": { + "add": 4633, + "scale": 520, + "warp": 72 + }, + "cleanup_records": 5225, + "complete": { + "add": 16230, + "corr": 36, + "scale": 1164, + "warp": 168 + }, + "complete_records": 17598, + "prefix": { + "add": 11597, + "corr": 36, + "scale": 644, + "warp": 96 + }, + "prefix_records": 12373 + } + }, + "primitive_delta": { + "canceled": { + "add": 0, + "corr": 0, + "scale": 0, + "warp": 0 + }, + "literal": { + "add": 2, + "corr": 0, + "scale": 0, + "warp": 0 + } + }, + "profile_delta": { + "1": 0, + "2": 0, + "3": 0, + "4": 0, + "5": 0, + "8": 0 + }, + "rejection_controls": { + "difference_instead_of_sum": { + "rejected_by": "full arbitrary-dirty forward map", + "witness": { + "actual": "-1/2", + "expected": "0", + "input": 601, + "operator_word": [], + "output": 123 + } + }, + "frozen_cleanup_mislabelled_literal": { + "rejected_by": "literal reverse-inverse representation only", + "semantic_map_passes": true, + "valid_with_explicit_adjacent_cancellation_certificate": true + }, + "missing_capture_undo": { + "rejected_by": "full arbitrary-dirty forward map", + "witness": { + "actual": "-1/2", + "expected": "0", + "input": 601, + "operator_word": [], + "output": 123 + } + }, + "one_literal_inverse_shear_missing": { + "rejected_by": "full arbitrary-dirty forward map", + "witness": { + "actual": "1", + "expected": "0", + "input": 601, + "operator_word": [], + "output": 600 + } + }, + "wrong_capture_frame": { + "rejected_by": "chronological binary-frame containment", + "witness": "frame containment fails ('B', 81) 600" + } + }, + "width_delta": { + "5": 0, + "6": 0, + "7": 0, + "8": 0, + "9": 0 + }, + "word_json_sha256": { + "canceled": "f737212db051125e821920ccebc7fa9b558da37d2a586ec27e14eb647ff91ca3", + "literal": "dd92a036924d3162b1d5268d9748b283628b113255c6db4dcf4828abdd676f2f", + "predecessor": "cee1ddcbdf3cdcba99146f281cbb452440dd1ed641aa3a47ccc3343680ae7ddc" + } + }, + "extra": { + "algebra": { + "cleanup_boundary": { + "all_723_rows_equal": true, + "target_and_restored_helper_contract": true + }, + "forward": { + "all_rows_equal": true, + "full_contract": true, + "independent_coordinates": 723, + "matrix_sha256": "2b92555ebf438c5a563252ded44e6950831a1576102e646f5b3dbd58978a2c26", + "nonzero_coefficients": 835 + }, + "inverse_transpose": { + "all_rows_equal": true, + "full_contract": true, + "independent_coordinates": 723, + "matrix_sha256": "4cfd33e94d6339f31b6ee00850ad8574f26d0d29a18d59dac84f01f1e6fd4f6c", + "nonzero_coefficients": 835 + }, + "reverse_column_traversal": { + "all_three_words_match_forward": true, + "input_columns": 723 + } + }, + "cleanup": { + "adjacent_pair_zero_based_index": 1225, + "deleting_exact_pair_equals_predecessor_cleanup": true, + "literal_reverse_inverse_verified": true, + "pair": [ + [ + "add", + 600, + 601, + 1, + 1, + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ], + [ + "add", + 600, + 601, + -1, + 1, + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ] + ] + }, + "frozen_file_sha256": "d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299", + "paid": { + "capture_helpers": { + "600": { + "entrance_dimension": 1, + "positive_climbs": [ + 4, + 1, + 1, + 1, + 1 + ], + "terminal_dimension": 9, + "width": 8 + }, + "601": { + "entrance_dimension": 1, + "positive_climbs": [ + 4, + 1, + 1, + 1, + 1 + ], + "terminal_dimension": 9, + "width": 8 + } + }, + "live_helpers": 408, + "local_block": { + "entrance_dimensions": { + "123": 0, + "175": 0, + "183": 0, + "202": 0, + "600": 1, + "601": 1 + }, + "exit_dimensions": { + "123": 1, + "175": 1, + "183": 1, + "202": 1, + "600": 1, + "601": 1 + }, + "helper_positive_climbs": 0, + "paid_profile": { + "1": 4 + }, + "target_rank1_climbs": 4 + }, + "ordered_helper_contract_sha256": "aea056c5a94af736eb9444d8b31de404b43d10eff9609be39e6c7803713ccee4", + "positive_frame_transitions_sha256": "acafac208072a5ad6239cec60d4844282630bc1787d156ac6d48d44a780bfdcd", + "profile": { + "1": 2482, + "2": 712, + "3": 218, + "4": 109, + "5": 20, + "8": 8 + }, + "width_inventory": { + "5": 28, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + } + }, + "primitive_counts": { + "canceled": { + "cleanup": { + "add": 4633, + "scale": 520, + "warp": 72 + }, + "cleanup_records": 5225, + "complete": { + "add": 16230, + "corr": 36, + "scale": 1164, + "warp": 168 + }, + "complete_records": 17598, + "prefix": { + "add": 11597, + "corr": 36, + "scale": 644, + "warp": 96 + }, + "prefix_records": 12373 + }, + "literal": { + "cleanup": { + "add": 4635, + "scale": 520, + "warp": 72 + }, + "cleanup_records": 5227, + "complete": { + "add": 16232, + "corr": 36, + "scale": 1164, + "warp": 168 + }, + "complete_records": 17600, + "prefix": { + "add": 11597, + "corr": 36, + "scale": 644, + "warp": 96 + }, + "prefix_records": 12373 + }, + "predecessor": { + "cleanup": { + "add": 4633, + "scale": 520, + "warp": 72 + }, + "cleanup_records": 5225, + "complete": { + "add": 16230, + "corr": 36, + "scale": 1164, + "warp": 168 + }, + "complete_records": 17598, + "prefix": { + "add": 11597, + "corr": 36, + "scale": 644, + "warp": 96 + }, + "prefix_records": 12373 + } + }, + "primitive_delta": { + "canceled": { + "add": 0, + "corr": 0, + "scale": 0, + "warp": 0 + }, + "literal": { + "add": 2, + "corr": 0, + "scale": 0, + "warp": 0 + } + }, + "profile_delta": { + "1": 0, + "2": 0, + "3": 0, + "4": 0, + "5": 0, + "8": 0 + }, + "rejection_controls": { + "difference_instead_of_sum": { + "rejected_by": "full arbitrary-dirty forward map", + "witness": { + "actual": "-1/2", + "expected": "0", + "input": 601, + "operator_word": [], + "output": 123 + } + }, + "frozen_cleanup_mislabelled_literal": { + "rejected_by": "literal reverse-inverse representation only", + "semantic_map_passes": true, + "valid_with_explicit_adjacent_cancellation_certificate": true + }, + "missing_capture_undo": { + "rejected_by": "full arbitrary-dirty forward map", + "witness": { + "actual": "-1/2", + "expected": "0", + "input": 601, + "operator_word": [], + "output": 123 + } + }, + "one_literal_inverse_shear_missing": { + "rejected_by": "full arbitrary-dirty forward map", + "witness": { + "actual": "1", + "expected": "0", + "input": 601, + "operator_word": [], + "output": 600 + } + }, + "wrong_capture_frame": { + "rejected_by": "chronological binary-frame containment", + "witness": "frame containment fails ('B', 81) 600" + } + }, + "width_delta": { + "5": 0, + "6": 0, + "7": 0, + "8": 0, + "9": 0 + }, + "word_json_sha256": { + "canceled": "02393fbb7d24c86e3bfe247b9e56c6e4e919ed0b5e88786710303b1a533e34ee", + "literal": "324742bc5392516731e4f64693e4ab756a07188f3f04b9f35f6b1382f3410815", + "predecessor": "cc1826748ed24cd085a5756b46f0090d5a43ad54820c025366cf2848aca589b2" + } + } + } +} diff --git a/research/partial-helper-capture/construction/verify.py b/research/partial-helper-capture/construction/verify.py new file mode 100644 index 0000000000..f2e34de284 --- /dev/null +++ b/research/partial-helper-capture/construction/verify.py @@ -0,0 +1,380 @@ +#!/usr/bin/env python3 +"""Exact partial sum capture on the two immutable PR3945 words. + +Python standard library only. No assertions are used. With --output, write a +fresh deterministic result to that path; otherwise compare against RESULT.json. +The imported, source-pinned audit core is credited in DERIVATION.md. +""" +import argparse +import copy +import gzip +import hashlib +import importlib.util +import json +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path +import sys + + +HERE = Path(__file__).resolve().parent +PACKAGE = HERE.parent +SOURCE_FREEZE = "f0631e4329ef4124c498fe3d1c500aab34ce6490" +SOURCE_PINS = { + "predecessor4061/frozen/WORD-base.json.gz": + "08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0", + "predecessor4061/frozen/WORD-extra.json.gz": + "d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299", + "source4076/vendor/audit_core.py": + "888679ca8502cdcb100420fe5382a052529a494bf76cb332928b86e62612b951", +} +OLD_BLOCK = [ + ["add", 183, 600, 1, 4, [45]], + ["add", 202, 600, -1, 4, [45]], + ["add", 175, 600, 1, 4, [45]], + ["add", 123, 600, -1, 4, [45]], + ["add", 183, 601, 1, 4, [45]], + ["add", 202, 601, 1, 4, [45]], + ["add", 175, 601, 1, 4, [45]], + ["add", 123, 601, 1, 4, [45]], +] +# Indices are zero-based. The four exception reads remain byte-identical. +NEW_BLOCK = [copy.deepcopy(OLD_BLOCK[i]) for i in (1, 3, 5, 7)] + [ + ["add", 600, 601, 1, 1, [45]], + copy.deepcopy(OLD_BLOCK[0]), + copy.deepcopy(OLD_BLOCK[2]), + ["add", 600, 601, -1, 1, [45]], +] +FULL_BASIS = [256, 128, 64, 32, 16, 8, 4, 2, 1] +INVERSE_PAIR = [ + ["add", 600, 601, 1, 1, FULL_BASIS], + ["add", 600, 601, -1, 1, FULL_BASIS], +] + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def digest(value): + return hashlib.sha256(canonical(value)).hexdigest() + + +def file_digest(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def load_core(): + for name, expected in SOURCE_PINS.items(): + need(file_digest(PACKAGE / name) == expected, "source pin differs: " + name) + spec = importlib.util.spec_from_file_location("pinned_partial_capture_audit", + PACKAGE / "source4076/vendor/audit_core.py") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def local_rows(gates): + """An independent six-coordinate rational check of the changed block.""" + regs = (123, 175, 183, 202, 600, 601) + rows = {r: {r: Q(1)} for r in regs} + for kind, dst, src, num, den, frame in gates: + need(kind == "add" and dst != src and frame == [45], "local gate format") + for var, coefficient in list(rows[src].items()): + value = rows[dst].get(var, Q(0)) + Q(num, den) * coefficient + if value: + rows[dst][var] = value + else: + rows[dst].pop(var, None) + return rows + + +def row_digest(rows): + return digest([[r, [[var, list(word), str(q)] for (var, word), q in sorted(row.items())]] + for r, row in sorted(rows.items())]) + + +def first_difference(expected, actual): + for r in sorted(set(expected) | set(actual)): + erow, arow = expected.get(r, {}), actual.get(r, {}) + for var, word in sorted(set(erow) | set(arow)): + if erow.get((var, word), 0) != arow.get((var, word), 0): + return {"output": r, "input": var, "operator_word": list(word), + "expected": str(erow.get((var, word), 0)), + "actual": str(arow.get((var, word), 0))} + return None + + +def exact_contract(core, word, rows, dual=False): + regs = sorted(set(range(core.N)) - set(word["removed"])) + regs += sorted(int(c) + core.N for c in word["helper_final"]) + need(len(regs) == 723 and set(rows) == set(regs), "incomplete 723-coordinate domain") + for r in regs: + expected = {(r, ()): Q(1)} + if not dual and core.is_target(r): + expected[r - core.V, ()] = Q(1) + if dual and r < core.V: + expected[r + core.V, ()] = Q(-1) + need(rows[r] == expected, "full arbitrary-input contract differs at " + str(r)) + + +def primitive_counts(core, word): + prefix, cleanup = core.program(word) + counts = lambda gates: dict(sorted(Counter(g[0] for g in gates).items())) + return {"prefix": counts(prefix), "cleanup": counts(cleanup), + "complete": counts(prefix + cleanup), + "prefix_records": len(prefix), "cleanup_records": len(cleanup), + "complete_records": len(prefix) + len(cleanup)} + + +def count_delta(old, new): + return {k: new.get(k, 0) - old.get(k, 0) for k in sorted(set(old) | set(new))} + + +def paid_description(core, word): + bill, widths, chain, start, end = core.frame_bill(word, lagrangian=True) + local_regs = (123, 175, 183, 202, 600, 601) + block_events = {r: [(where, d, mask) for where, d, mask in chain[r] + if where[0] == "B" and 77 <= where[1] < 85] + for r in local_regs} + need(all(block_events[r] and chain[r][0] == block_events[r][0] for r in local_regs), + "local frame entrances are not the declared starting frames") + entrance = {str(r): core.dim(start[r]) for r in local_regs} + exit_frames = {str(r): core.dim(block_events[r][-1][2]) for r in local_regs} + need(entrance == {str(r): int(r >= 600) for r in local_regs} + and all(mask == core.span([45]) for events in block_events.values() + for _, _, mask in events), "fixed local boundary frames differ") + local_bill = dict(sorted(Counter(d for events in block_events.values() + for _, d, _ in events if type(d) is int and d > 0).items())) + need(local_bill == {1: 4}, "local block does not attain the four-target rank-1 floor") + # Preserve helper identities as well as the width multiset. + ordered = [[r, core.dim(end[r]) - core.dim(start[r]), hex(start[r]), hex(end[r])] + for r in sorted(start) if r >= 2 * core.V] + positive = [[r, [[d, hex(mask)] for _, d, mask in chain[r] + if type(d) is int and d > 0]] for r in sorted(start)] + return {"profile": bill, "width_inventory": widths, + "local_block": {"entrance_dimensions": entrance, "exit_dimensions": exit_frames, + "paid_profile": local_bill, + "helper_positive_climbs": 0, "target_rank1_climbs": 4}, + "ordered_helper_contract_sha256": digest(ordered), + "positive_frame_transitions_sha256": digest(positive), + "live_helpers": len(ordered), + "capture_helpers": {str(r): {"entrance_dimension": core.dim(start[r]), + "terminal_dimension": core.dim(end[r]), + "width": core.dim(end[r]) - core.dim(start[r]), + "positive_climbs": [d for _, d, _ in chain[r] + if type(d) is int and d > 0]} + for r in (600, 601)}} + + +def candidate(core, old): + need(old["B"][77:85] == OLD_BLOCK, "frozen B77..84 context changed") + need(old["start_extra"]["600"] == old["start_extra"]["601"] == [45], + "capture entrance differs") + need(all(600 not in core.touched(g) and 601 not in core.touched(g) + for g in old["A"] + old["B"][:77]), "capture pullbacks are not original dirt") + need(min(w[0] for w in old["warps"]) > 84, "operator enters the changed local block") + need(600 not in map(int, old["helper_final"]) and 601 not in map(int, old["helper_final"]), + "capture pair would require a private-buffer remap") + need(core.same_cleanup(old["cleanup"], core.derive_cleanup(old)), "frozen cleanup is stale") + literal = copy.deepcopy(old) + literal["B"][77:85] = copy.deepcopy(NEW_BLOCK) + literal["cleanup"] = core.derive_cleanup(literal) + locations = [i for i in range(len(literal["cleanup"]) - 1) + if literal["cleanup"][i:i + 2] == INVERSE_PAIR + and literal["cleanup"][:i] + literal["cleanup"][i + 2:] == old["cleanup"]] + need(len(locations) == 1, "literal inverse pair has no unique cancellation witness") + i = locations[0] + canceled = copy.deepcopy(literal) + canceled["cleanup"] = literal["cleanup"][:i] + literal["cleanup"][i + 2:] + need(canceled["cleanup"] == old["cleanup"], "explicit cancellation differs from predecessor") + need(all(literal[k] == old[k] for k in old if k not in ("B", "cleanup")), + "unexpected word-field edit") + return literal, canceled, i + + +def algebra_checks(core, old, literal, canceled): + results = {} + for dual in (False, True): + orientation = "inverse_transpose" if dual else "forward" + expected = core.forward_rows(old, dual=dual, symbolic_buffers=True) + exact_contract(core, old, expected, dual) + for label, word in (("literal", literal), ("canceled", canceled)): + got = core.forward_rows(word, dual=dual, symbolic_buffers=True) + need(got == expected, orientation + " all-column equality failed: " + label) + exact_contract(core, word, got, dual) + results[orientation] = {"independent_coordinates": 723, + "nonzero_coefficients": sum(map(len, expected.values())), + "all_rows_equal": True, "full_contract": True, + "matrix_sha256": row_digest(expected)} + # A separately traversed reverse pullback checks every input column, including + # private buffers, against the forward traversal. + for label, word in (("predecessor", old), ("literal", literal), ("canceled", canceled)): + cols = core.reverse_columns(word) + need(len(cols) == 723, "reverse pullback has missing input columns") + need(core.transpose(cols) == core.forward_rows(word, symbolic_buffers=True), + "reverse-column/forward-row disagreement: " + label) + results["reverse_column_traversal"] = {"input_columns": 723, + "all_three_words_match_forward": True} + boundary = {} + for label, word in (("predecessor", old), ("literal", literal), ("canceled", canceled)): + def save(rows): + boundary[label] = copy.deepcopy(rows) + core.forward_rows(word, symbolic_buffers=True, snapshot=save) + need(core.boundary_defects(word, boundary[label]) == [], "cleanup-boundary defect: " + label) + need(boundary["literal"] == boundary["canceled"] == boundary["predecessor"], + "cleanup-boundary equality failed") + results["cleanup_boundary"] = {"all_723_rows_equal": True, + "target_and_restored_helper_contract": True} + return results + + +def controls(core, old, literal, canceled, pair_index): + expected = core.forward_rows(old, symbolic_buffers=True) + results = {} + + def reject_map(label, mutant): + need(mutant != literal, "no-op control: " + label) + actual = core.forward_rows(mutant, symbolic_buffers=True) + witness = first_difference(expected, actual) + need(witness is not None, "map control unexpectedly passed: " + label) + results[label] = {"rejected_by": "full arbitrary-dirty forward map", "witness": witness} + + missing = copy.deepcopy(literal) + missing["B"].pop(84) # Delete the actual -601 undo, preserving later warp cuts. + for record in missing["warps"]: + if record[0] > 84: + record[0] -= 1 + missing["cleanup"] = core.derive_cleanup(missing) + reject_map("missing_capture_undo", missing) + + wrong_sign = copy.deepcopy(literal) + wrong_sign["B"][81][3] = -1 + wrong_sign["B"][84][3] = 1 + wrong_sign["cleanup"] = core.derive_cleanup(wrong_sign) + reject_map("difference_instead_of_sum", wrong_sign) + + missing_inverse = copy.deepcopy(literal) + missing_inverse["cleanup"].pop(pair_index + 1) + reject_map("one_literal_inverse_shear_missing", missing_inverse) + + wrong_frame = copy.deepcopy(literal) + wrong_frame["B"][81][-1] = [51] + need(wrong_frame != literal, "no-op frame control") + try: + core.frame_bill(wrong_frame) + except core.AuditFailure as exc: + results["wrong_capture_frame"] = {"rejected_by": "chronological binary-frame containment", + "witness": str(exc)} + else: + raise ValueError("incomparable capture-frame control passed") + + # Frozen cleanup is semantically valid after certified adjacent cancellation. + # It is only rejected if falsely labelled as the literal reverse-inverse list. + need(not core.same_cleanup(canceled["cleanup"], core.derive_cleanup(canceled)), + "literal-format control did not change the actual cleanup list") + need(core.forward_rows(canceled, symbolic_buffers=True) == expected, + "certified cancellation was incorrectly treated as a semantic defect") + results["frozen_cleanup_mislabelled_literal"] = { + "rejected_by": "literal reverse-inverse representation only", + "semantic_map_passes": True, + "valid_with_explicit_adjacent_cancellation_certificate": True, + } + return results + + +def verify_word(core, name): + path = PACKAGE / "predecessor4061/frozen" / ("WORD-" + name + ".json.gz") + old = json.loads(gzip.decompress(path.read_bytes())) + literal, canceled, pair_index = candidate(core, old) + for word in (old, literal, canceled): + need(core.hygiene(word), "dyadic/access hygiene failed") + algebra = algebra_checks(core, old, literal, canceled) + paid = {label: paid_description(core, word) for label, word in + (("predecessor", old), ("literal", literal), ("canceled", canceled))} + need(paid["predecessor"] == paid["literal"] == paid["canceled"], + "capture unexpectedly changes paid frames or ordered widths") + need(paid["predecessor"]["profile"] == {int(k): v for k, v in old["report"]["local_profile"].items()}, + "recomputed profile differs from frozen report") + need(paid["predecessor"]["width_inventory"] == + {int(k): v for k, v in old["report"]["width_inventory"].items()}, + "recomputed widths differ from frozen report") + counts = {label: primitive_counts(core, word) for label, word in + (("predecessor", old), ("literal", literal), ("canceled", canceled))} + return { + "frozen_file_sha256": file_digest(path), + "word_json_sha256": {label: digest(word) for label, word in + (("predecessor", old), ("literal", literal), ("canceled", canceled))}, + "algebra": algebra, + "cleanup": {"literal_reverse_inverse_verified": True, + "adjacent_pair_zero_based_index": pair_index, + "pair": INVERSE_PAIR, + "deleting_exact_pair_equals_predecessor_cleanup": True}, + "paid": paid["predecessor"], + "profile_delta": count_delta(paid["predecessor"]["profile"], paid["canceled"]["profile"]), + "width_delta": count_delta(paid["predecessor"]["width_inventory"], + paid["canceled"]["width_inventory"]), + "primitive_counts": counts, + "primitive_delta": {label: count_delta(counts["predecessor"]["complete"], + counts[label]["complete"]) + for label in ("literal", "canceled")}, + "rejection_controls": controls(core, old, literal, canceled, pair_index), + } + + +def run(): + core = load_core() + old_local, new_local = local_rows(OLD_BLOCK), local_rows(NEW_BLOCK) + need(old_local == new_local, "independent rational local-block identity failed") + result = { + "schema_version": 1, + "status": "exact_partial_capture_with_zero_recursive_profile_gain", + "source_freeze_commit": SOURCE_FREEZE, + "predecessor4061_head": "f977a8a3dcb2983829d066a80420b7ded42d3e09", + "audit_core_source4076_head": "9744f9df268590295a9872b1952c695a678192b9", + "source_sha256": SOURCE_PINS, + "verifier_sha256": file_digest(Path(__file__).resolve()), + "edit": {"field": "B", "zero_based_half_open_slice": [77, 85], + "old": OLD_BLOCK, "new": NEW_BLOCK, + "all_other_forward_fields_unchanged": True, + "warp_positions_unchanged": True}, + "local_identity": {str(r): {str(s): str(q) for s, q in sorted(row.items())} + for r, row in sorted(old_local.items())}, + "domain": {"live_dirty_inputs": 632, "private_buffer_inputs": 91, + "independent_coordinates": 723, "independent_native_operator_symbols": 72, + "coefficient_ring": "dyadic rationals over the free group algebra", + "phase_claim": False, "formal_kernel_claim": False}, + "words": {name: verify_word(core, name) for name in ("base", "extra")}, + "conclusion": {"complete_paid_rank_moment_delta": "0 for every exponent p", + "ordered_helper_width_change": False, + "literal_scalar_add_delta": 2, + "canceled_scalar_add_delta": 0, + "new_kappa_claim": False, + "stop_rule": "This concrete partial capture removes no recursive child charge or helper width."}, + } + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, + help="write a fresh deterministic JSON result to this path") + args = parser.parse_args() + # Normalize JSON object keys before comparing the checked-in certificate. + result = json.loads(json.dumps(run())) + if args.output is not None: + args.output.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + committed = json.loads((HERE / "RESULT.json").read_text()) + need(result == committed, "fresh result differs from committed RESULT.json") + print("PASS_PARTIAL_HELPER_CAPTURE", digest(result), + "python=" + sys.version.split()[0], "optimize=" + str(sys.flags.optimize)) + + +if __name__ == "__main__": + main() diff --git a/research/partial-helper-capture/independent/INITIAL-DERIVATION.md b/research/partial-helper-capture/independent/INITIAL-DERIVATION.md new file mode 100644 index 0000000000..acb0baf069 --- /dev/null +++ b/research/partial-helper-capture/independent/INITIAL-DERIVATION.md @@ -0,0 +1,50 @@ +# Initial independent derivation + +This derivation was saved before reading another worker's construction code. +Only the two frozen words, their export/provenance records, the predecessor +README/TASK, and PR4076's `audit_core.py` frame/cleanup format contract were +read. The independent verifier will not import that module or any construction +checker. This is AI mathematical review, not independent human review. + +Let `a=ell_600`, `b=ell_601` and order the four arbitrary target inputs as +`(u,v,w,z)=(ell_123,ell_175,ell_183,ell_202)`. The source bytes at zero-based +`B[77:85]` on both frozen words give + +`(a,b,u,v,w,z) -> (a,b,u+(-a+b)/4,v+(a+b)/4,w+(a+b)/4,z+(-a+b)/4)`. + +Every gate here uses the identical frame list `[45]`. Take the four retained +updates to `u,z` using the original `a,b`, then execute + +`a += b; v += a/4; w += a/4; a -= b`. + +The helper pair is restored for every dirty `a,b`; each target retains its +arbitrary entering value. This is an identity of rational 6 by 6 matrices, +not a clean-input test. The matrix has full rank six, with inverse obtained +by subtracting each displayed source contribution from its target. + +There are eight forward ADD records before and after. Source reads remain +eight in total (four from each helper): the two discarded reads of `b` for +agreeing targets are replaced by its two capture/uncapture reads. The helper +`a` gains two writes; target writes fall from eight to six. The source-only +subword is `a+=b; a-=b`, so its reverse inverse cleanup is again an adjacent +inverse pair once target writes are omitted. The literal inverse generator +therefore adds two records, but exact scalar cancellation removes both with +no semantic defect. Old cleanup can consequently be algebraically sufficient +even though it is not the unsimplified literal generated list. + +At the block boundary all six registers have the same physical frame as +before. Therefore, for any fixed invertible representative `T_[45]`, the +logical scalar matrix identity lifts to exactly the same physical operator; +there is no appeal to binary-span equality between different representatives. +The added helper shears occur at their existing frame and cost zero native +climb rank. Both helpers remain read in `[45]` by the retained targets 123 and +202. Native source/target climbs and fixed entrance/terminal boundaries do not +change under this explicit rewrite. Endpoint widths therefore do not change. +Full-word chronology and histogram checks remain to be implemented. + +Scope: the explicit partial capture of this block, or a comparison that keeps +all external frame boundaries and their paid itinerary fixed. This is not a +lower bound against changed helper entrances/terminals, other source pairs, +retiming across outside events, changed child contracts, or global resynthesis. +Even exact scalar cancellation of the added cleanup gives no paid recursive +child saving. No supplier or kappa improvement follows. diff --git a/research/partial-helper-capture/independent/PROOF.md b/research/partial-helper-capture/independent/PROOF.md new file mode 100644 index 0000000000..e2a99ffc69 --- /dev/null +++ b/research/partial-helper-capture/independent/PROOF.md @@ -0,0 +1,221 @@ +# Independent partial-capture proof and paid-frame invoice + +This is an exact local proof and independent finite invoice for the two frozen +PR3945 words carried by PR4061. It is not a formal-kernel proof or independent +human review. The mathematical model is the pinned BORROW-WORD format, including +its existing source/helper entrances, terminal frames, center-service billing, +native warps, and literal inverse cleanup. No project checker is imported. +`check.py` uses exact rational matrices and reduced GF(2) row bases; PR4076's +`audit_core.py` was read only to establish the format's frame/cleanup contract. + +## Exact arbitrary-input operator + +Both source files have the same eight ADDs at zero-based `B[77:85]`, with the +same frame representative `[45]` and coefficient magnitudes `1/4`. Their byte +hashes are checked against both fixed constants and `SOURCE-EXPORT.json`: + +| word | SHA-256 | +| --- | --- | +| base | `08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0` | +| extra | `d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299` | + +The uncompressed words are not asserted identical. In coordinates +`(a,b,u,v,w,z)=(600,601,123,175,183,202)`, their local map is + +\[ +M=\begin{pmatrix} +1&0&0&0&0&0\\ +0&1&0&0&0&0\\ +-1/4&1/4&1&0&0&0\\ +1/4&1/4&0&1&0&0\\ +1/4&1/4&0&0&1&0\\ +-1/4&1/4&0&0&0&1 +\end{pmatrix}. +\] + +All six entering values are arbitrary. A zero *frame* means the zero binary +subspace, not a promise that the value stored in that register is zero. + +Retain the original four updates to `u,z`, in original relative order: + +``` +z -= a/4 +u -= a/4 +z += b/4 +u += b/4 +``` + +Then execute + +``` +a += b +w += a/4 +v += a/4 +a -= b +``` + +During the two agreeing-target reads, the value of `a` is its entering value +plus the entering value of `b`. The final subtraction restores `a`, while `b` +never changes. The targets receive exactly the four rows of `M` displayed +above, retaining their arbitrary entering values. The matrix has determinant +one and inverse obtained by negating its lower-left four-by-two block. This is +an identity over the rationals and therefore also over the complex numbers; +checking all 36 matrix coefficients proves every input, without numerical +sampling or an assumption of clean helpers or targets. + +All local gates use the same fixed representative `T_[45]` after each operand +reaches that frame. Hence the logical identity lifts to equality of physical +operators with the same entering and outgoing frames. For block-diagonal +frame operators `D_in,D_out`, the original and candidate both realize +`D_out M D_in^{-1}`. Binary-span equality between different representatives is +not being used. Substitution into the unchanged surrounding word is therefore +valid on every full dirty input, without replaying a complete full-word symbolic +operator or assuming an endpoint theorem for the predecessor. + +## Sharp fixed-boundary frame lower bound + +The independent chronological replay checks these six block boundaries on both +words, before and after the rewrite: + +| register | entering frame | outgoing frame | +| --- | --- | --- | +| 600, 601 | `[45]` | `[45]` | +| 123, 175, 183, 202 | `[]` | `[45]` | + +Assume the same six physical registers, the same boundaries and monotone frame +growth inside the block. Scalar couplings may otherwise be arbitrary, subject +to the format's common-frame operand rule. Each target starts at dimension zero +and ends at dimension one. The positive dimension increments on that target +are nonnegative integers summing to one. Thus each target pays exactly one +rank-1 climb. Different physical registers have separate child calls under the +existing single-register child ABI. Therefore every such rewrite pays at least + +\[ +H_1\geq4,\qquad \sum_r H_r r^{1-\alpha}\geq4. +\] + +The four unavoidable target calls contribute exactly four; added registers or +other permitted paid work can only add nonnegative charges. The original block +and the explicit partial capture both attain `H_1=4` and no other local child. +The source helpers already enter at `[45]`, so neither has a positive local +climb to remove. This establishes a local optimum under the specified +boundaries, irrespective of scalar coupling choices. It does not establish a +global optimum after changing outside boundaries, crossing other events, +descent/reset permissions, physical target ownership, or the child ABI. + +The candidate retimes target climbs inside the block: originally 183, 202, 175, +123 climb at B77, B78, B79, B80; in this candidate 202, 123, 183, 175 climb at +B77, B78, B82, B83. Their per-register frame paths are unchanged. This is not a +claim that the four chronological event indices are identical. + +## Literal and canceled cleanup + +The format omits target-destination gates from inverse cleanup. The only new +non-target gates are `a+=b` followed later by `a-=b`. Reversing and inverting +therefore inserts the adjacent FULL-frame pair + +``` +a += b +a -= b +``` + +at cleanup index 1225. Both helpers terminate at FULL and have no restored-helper +backing substitution. The pair is the identity on arbitrary inputs in the same +FULL frame. The unsimplified literal recipe increases from 5,225 to 5,227 +records. Canceling this exact adjacent inverse pair returns the complete +original 5,225-record cleanup list, byte-for-byte at the gate-data level after +frame-basis normalization. Consequently the original cleanup remains +*semantically sufficient* for the candidate. It differs from the unsimplified +literal inverse list. A checker may reject that old list for literal-recipe +noncompliance, but must not call it a semantic failure. + +## Complete invoice on both frozen words + +Every positive native climb is reconstructed, including read-only source +operands, center-service descents, frame-only terminal promotions and all native +warps. All frame containments, warp images and externally prescribed frames are +checked using separate GF(2) elimination. Positive climbs are compared in +chronological order within each physical register, including their old and new +frames. No positive source visit disappears. + +| item | original | literal capture | capture with pair canceled | +| --- | ---: | ---: | ---: | +| local forward ADD records | 8 | 8 | 8 | +| local source reads, 600 / 601 | 4 / 4 | 4 / 4 | 4 / 4 | +| local writes to helper 600 | 0 | 2 | 2 | +| local target writes | 8 | 6 | 6 | +| cleanup records | 5,225 | 5,227 | 5,225 | +| complete-word ADD records | 16,230 | 16,232 | 16,230 | +| complete-word SCALE records | 1,164 | 1,164 | 1,164 | +| complete executed records, including warps/corrections | 17,598 | 17,600 | 17,598 | +| source reads in complete word, 600 / 601 | 7 / 7 | 7 / 9 | 7 / 7 | +| source writes in complete word, 600 / 601 | 10 / 10 | 14 / 10 | 12 / 10 | +| positive native child calls | 3,549 | 3,549 | 3,549 | +| positive native rank mass | 5,160 | 5,160 | 5,160 | + +The complete native histogram is unchanged: + +`{1:2482, 2:712, 3:218, 4:109, 5:20, 8:8}`. + +The complete helper-width inventory is unchanged: + +`{5:28, 6:18, 7:53, 8:96, 9:213}`. + +Helpers 600 and 601 each have entrance dimension one, terminal dimension nine, +width eight and the same five paid climbs `(4,1,1,1,1)`. Their exact positive +source-access addresses are: + +| helper | B positions | terminal | +| --- | --- | --- | +| 600 | 936 (rank 4), 948, 1470, 1472 (rank 1 each) | rank 1 | +| 601 | 937 (rank 4), 949, 1474, 1476 (rank 1 each) | rank 1 | + +`RESULT.json` contains the exact binary bases for every displayed source climb, +the full histograms, endpoint widths, per-stage read/write counts, source-byte +pins and a digest of all positive per-register chronological paths. The +verifier reconstructs the complete list; the report digest does not replace +that computation. Because this invoice is identical, any recursive power bill +with fixed caller normalization and the existing child/hosting contract is +identical for the two words. The unsimplified literal recipe increases scalar +work; canceling its inverse pair recovers the original scalar record count. +Neither version supplies a recursive-cost saving. Physical tape/controller +costs or approximation error are not newly certified by this format-level +comparison. + +## Reproduction, controls and sources + +From the repository root, standard-library Python: + +``` +python3 -B research/partial-helper-capture/independent/check.py +``` + +The default performs no writes and compares the deterministic result against +`independent/RESULT.json`, including the verifier's own SHA-256. To emit a fresh +receipt, use `--output` with an absolute path. The expected marker is +`PASS_PARTIAL_CAPTURE_INDEPENDENT`. + +Defect-sensitive controls reject an agreeing-target sign error, capture sign +error, missing undo on arbitrary dirty sources, wrong common frame, an unpaid +read-only source frame, and a wrong cleanup inverse sign. The missing-undo +control also demonstrates why zero-source tests fail to detect that error. +Literal-list inequality and semantic sufficiency after pair cancellation are +tested separately. The construction worker's verifier was first read after +`INITIAL-DERIVATION.md` was saved. PR4076's retained audit core was read earlier +as the frame/cleanup format contract, as explicitly recorded in that initial +derivation. Neither implementation is imported at any point. + +Credit: Dugongue's PR3945 words; Riquelme Soares (@hevlyo)'s PR4061 extraction, +signed-column test and explicit partial-capture follow-up; PR4045's selection +of the relevant actual helpers; PR4048's same-frame signed-capture idea; Rohan +Arun's PR4076 retention of Sagar Thakrar's PR3687 BORROW-WORD audit code, itself +crediting Arham Tahir's frame/cleanup reading. Exact exported source heads, +paths and Git blobs are +recorded in `SOURCE-EXPORT.json`. This independent derivation/checker was +produced with substantial OpenAI GPT-6.1 Sol assistance. Source material is +Apache-2.0; see the package license and notices. + +No complete physical supplier, full recurrence improvement, new kappa, +selected-frontier change or broader impossibility theorem is claimed. Changed +helper entrances or terminals, larger capture sets, cross-block retiming, +different physical ownership or higher-rank delivery contracts remain open. diff --git a/research/partial-helper-capture/independent/RESULT.json b/research/partial-helper-capture/independent/RESULT.json new file mode 100644 index 0000000000..2a863a143a --- /dev/null +++ b/research/partial-helper-capture/independent/RESULT.json @@ -0,0 +1,2235 @@ +{ + "contract_reference": "source4076/vendor/audit_core.py was read for BORROW-WORD frame/cleanup semantics; no project module imported. RREF arithmetic and local matrix evaluation implemented separately.", + "coverage": "Two pinned finite words; exact rational local operator on arbitrary dirty inputs; complete native-frame and helper-width invoice under the BORROW-WORD contract.", + "implementation_sha256": "8ae562ae150866e1c8920c112b14ca7d5d0963527c2599d1edb43864006a8687", + "physical_lift": "All eight replaced ADDs and all eight candidate ADDs use the identical [45] representative; exact logical matrix equality gives exact physical equality for any fixed invertible T_[45].", + "result": "EXACT_PARTIAL_CAPTURE_WITH_ZERO_NATIVE_PROFILE_GAIN", + "schema_version": 1, + "source_export_sha256": "c436ab59a73ea967782912955787e1f83ce18a14d1a1baa3a6d2520f57ab5b23", + "universal_cost_comparison_scope": "The explicit rewrite retains every positive native climb and endpoint width, so every price depending on that invoice is unchanged. More generally, monotone scalar rewrites at the same six block-boundary frames require all four ZERO-to-[45] target climbs, hence at least four rank-1 children. The original and explicit capture attain that local minimum. No global claim with changed external boundaries or paid itinerary is made.", + "unresolved": "Changed entrances or terminals, larger source sets, cross-block retiming, other child/hosting contracts, and global resynthesis are not excluded. No physical supplier, full recurrence improvement or new kappa is established.", + "words": { + "base": { + "added_cleanup_pair": [ + [ + "add", + 600, + 601, + 1, + 1, + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ], + [ + "add", + 600, + 601, + -1, + 1, + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ] + ], + "added_cleanup_pair_index": 1225, + "all_external_frames_unchanged": true, + "all_positive_climbs_per_register_unchanged": true, + "block_boundary_frames": { + "entry": { + "123": [], + "175": [], + "183": [], + "202": [], + "600": [ + 45 + ], + "601": [ + 45 + ] + }, + "exit": { + "123": [ + 45 + ], + "175": [ + 45 + ], + "183": [ + 45 + ], + "202": [ + 45 + ], + "600": [ + 45 + ], + "601": [ + 45 + ] + } + }, + "block_minimum_profile_under_fixed_monotone_boundaries": { + "1": 4 + }, + "block_paid_climbs_after": [ + [ + 202, + "B", + 77, + 1, + [], + [ + 45 + ] + ], + [ + 123, + "B", + 78, + 1, + [], + [ + 45 + ] + ], + [ + 183, + "B", + 82, + 1, + [], + [ + 45 + ] + ], + [ + 175, + "B", + 83, + 1, + [], + [ + 45 + ] + ] + ], + "block_paid_climbs_before": [ + [ + 183, + "B", + 77, + 1, + [], + [ + 45 + ] + ], + [ + 202, + "B", + 78, + 1, + [], + [ + 45 + ] + ], + [ + 175, + "B", + 79, + 1, + [], + [ + 45 + ] + ], + [ + 123, + "B", + 80, + 1, + [], + [ + 45 + ] + ] + ], + "canceled_cleanup_records_after": 5225, + "candidate_block": [ + [ + "add", + 202, + 600, + -1, + 4, + [ + 45 + ] + ], + [ + "add", + 123, + 600, + -1, + 4, + [ + 45 + ] + ], + [ + "add", + 202, + 601, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 123, + 601, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 600, + 601, + 1, + 1, + [ + 45 + ] + ], + [ + "add", + 183, + 600, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 175, + 600, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 600, + 601, + -1, + 1, + [ + 45 + ] + ] + ], + "defect_sensitive_controls": { + "clean_zero_sources_do_not_detect_missing_undo": true, + "missing_undo_rejected_on_arbitrary_dirty_sources": true, + "unpaid_read_only_source_frame_rejected": true, + "wrong_agreeing_target_sign_rejected": true, + "wrong_capture_sign_rejected": true, + "wrong_cleanup_inverse_sign_rejected": true, + "wrong_common_frame_rejected": true + }, + "helper_width_inventory": { + "5": 28, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "literal_cleanup_records_after": 5227, + "literal_cleanup_records_before": 5225, + "local_operation_counts": { + "after": { + "adds": 8, + "source_reads": { + "600": 4, + "601": 4 + }, + "source_writes": { + "600": 2, + "601": 0 + }, + "target_writes": 6 + }, + "before": { + "adds": 8, + "source_reads": { + "600": 4, + "601": 4 + }, + "source_writes": { + "600": 0, + "601": 0 + }, + "target_writes": 8 + } + }, + "matrix": [ + [ + "1", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "0", + "0", + "0" + ], + [ + "-1/4", + "1/4", + "1", + "0", + "0", + "0" + ], + [ + "1/4", + "1/4", + "0", + "1", + "0", + "0" + ], + [ + "1/4", + "1/4", + "0", + "0", + "1", + "0" + ], + [ + "-1/4", + "1/4", + "0", + "0", + "0", + "1" + ] + ], + "matrix_coordinates": [ + 600, + 601, + 123, + 175, + 183, + 202 + ], + "matrix_entry_coverage": 36, + "native_profile": { + "1": 2482, + "2": 712, + "3": 218, + "4": 109, + "5": 20, + "8": 8 + }, + "old_cleanup_equals_unsimplified_literal_recipe": false, + "old_cleanup_semantically_sufficient_after_exact_pair_cancellation": true, + "operation_invoice": { + "canceled_capture": { + "A": { + "operations": { + "add": 3557, + "scale": 498, + "warp": 24 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "B": { + "operations": { + "add": 1796, + "scale": 74 + }, + "source_access": { + "600": { + "reads": 6, + "writes": 7 + }, + "601": { + "reads": 6, + "writes": 5 + } + } + }, + "cleanup": { + "operations": { + "add": 4633, + "scale": 520, + "warp": 72 + }, + "source_access": { + "600": { + "reads": 1, + "writes": 5 + }, + "601": { + "reads": 1, + "writes": 5 + } + } + }, + "compensation": { + "operations": { + "add": 5736 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "cut": { + "operations": { + "add": 176 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "initial_corrections": 36, + "native_warps": 72, + "precondition": { + "operations": { + "add": 136, + "scale": 56 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "restore": { + "operations": { + "add": 196, + "scale": 16 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "source_reads_and_writes": { + "600": { + "reads": 7, + "writes": 12 + }, + "601": { + "reads": 7, + "writes": 10 + } + }, + "total_executed_records": 17598, + "totals_excluding_native_warps_and_corrections": { + "add": 16230, + "scale": 1164, + "warp": 96 + } + }, + "literal_capture": { + "A": { + "operations": { + "add": 3557, + "scale": 498, + "warp": 24 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "B": { + "operations": { + "add": 1796, + "scale": 74 + }, + "source_access": { + "600": { + "reads": 6, + "writes": 7 + }, + "601": { + "reads": 6, + "writes": 5 + } + } + }, + "cleanup": { + "operations": { + "add": 4635, + "scale": 520, + "warp": 72 + }, + "source_access": { + "600": { + "reads": 1, + "writes": 7 + }, + "601": { + "reads": 3, + "writes": 5 + } + } + }, + "compensation": { + "operations": { + "add": 5736 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "cut": { + "operations": { + "add": 176 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "initial_corrections": 36, + "native_warps": 72, + "precondition": { + "operations": { + "add": 136, + "scale": 56 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "restore": { + "operations": { + "add": 196, + "scale": 16 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "source_reads_and_writes": { + "600": { + "reads": 7, + "writes": 14 + }, + "601": { + "reads": 9, + "writes": 10 + } + }, + "total_executed_records": 17600, + "totals_excluding_native_warps_and_corrections": { + "add": 16232, + "scale": 1164, + "warp": 96 + } + }, + "original": { + "A": { + "operations": { + "add": 3557, + "scale": 498, + "warp": 24 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "B": { + "operations": { + "add": 1796, + "scale": 74 + }, + "source_access": { + "600": { + "reads": 6, + "writes": 5 + }, + "601": { + "reads": 6, + "writes": 5 + } + } + }, + "cleanup": { + "operations": { + "add": 4633, + "scale": 520, + "warp": 72 + }, + "source_access": { + "600": { + "reads": 1, + "writes": 5 + }, + "601": { + "reads": 1, + "writes": 5 + } + } + }, + "compensation": { + "operations": { + "add": 5736 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "cut": { + "operations": { + "add": 176 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "initial_corrections": 36, + "native_warps": 72, + "precondition": { + "operations": { + "add": 136, + "scale": 56 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "restore": { + "operations": { + "add": 196, + "scale": 16 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "source_reads_and_writes": { + "600": { + "reads": 7, + "writes": 10 + }, + "601": { + "reads": 7, + "writes": 10 + } + }, + "total_executed_records": 17598, + "totals_excluding_native_warps_and_corrections": { + "add": 16230, + "scale": 1164, + "warp": 96 + } + } + }, + "original_block": [ + [ + "add", + 183, + 600, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 202, + 600, + -1, + 4, + [ + 45 + ] + ], + [ + "add", + 175, + 600, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 123, + 600, + -1, + 4, + [ + 45 + ] + ], + [ + "add", + 183, + 601, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 202, + 601, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 175, + 601, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 123, + 601, + 1, + 4, + [ + 45 + ] + ] + ], + "paid_source_visits": { + "600": { + "entrance": [ + 45 + ], + "paid_visits": [ + [ + 600, + "B", + 936, + 4, + [ + 45 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + [ + 600, + "B", + 948, + 1, + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 385, + 72, + 40, + 24, + 5, + 2 + ] + ], + [ + 600, + "B", + 1470, + 1, + [ + 385, + 72, + 40, + 24, + 5, + 2 + ], + [ + 257, + 128, + 72, + 40, + 24, + 5, + 2 + ] + ], + [ + 600, + "B", + 1472, + 1, + [ + 257, + 128, + 72, + 40, + 24, + 5, + 2 + ], + [ + 257, + 128, + 65, + 33, + 17, + 9, + 5, + 2 + ] + ], + [ + 600, + "terminal", + null, + 1, + [ + 257, + 128, + 65, + 33, + 17, + 9, + 5, + 2 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ] + ], + "terminal": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + }, + "601": { + "entrance": [ + 45 + ], + "paid_visits": [ + [ + 601, + "B", + 937, + 4, + [ + 45 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + [ + 601, + "B", + 949, + 1, + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 408, + 80, + 40, + 4, + 2, + 1 + ] + ], + [ + 601, + "B", + 1474, + 1, + [ + 408, + 80, + 40, + 4, + 2, + 1 + ], + [ + 280, + 128, + 80, + 40, + 4, + 2, + 1 + ] + ], + [ + 601, + "B", + 1476, + 1, + [ + 280, + 128, + 80, + 40, + 4, + 2, + 1 + ], + [ + 272, + 128, + 80, + 32, + 8, + 4, + 2, + 1 + ] + ], + [ + 601, + "terminal", + null, + 1, + [ + 272, + 128, + 80, + 32, + 8, + 4, + 2, + 1 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ] + ], + "terminal": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + } + }, + "positive_climb_signature_sha256": "807c3a6384ae6d6670388070b2c1ce7525c33c5ba4ce5e7523c3e8d729435bce", + "positive_native_climb_count": 3549, + "positive_native_rank_mass": 5160, + "source": { + "git_blob": "806784bf99d9d15004d2d227d06268556a0726c8", + "head": "f977a8a3dcb2983829d066a80420b7ded42d3e09", + "original_path": "research/staged544-helper600-sign-columns/frozen/WORD-base.json.gz", + "sha256": "08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0" + } + }, + "extra": { + "added_cleanup_pair": [ + [ + "add", + 600, + 601, + 1, + 1, + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ], + [ + "add", + 600, + 601, + -1, + 1, + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ] + ], + "added_cleanup_pair_index": 1225, + "all_external_frames_unchanged": true, + "all_positive_climbs_per_register_unchanged": true, + "block_boundary_frames": { + "entry": { + "123": [], + "175": [], + "183": [], + "202": [], + "600": [ + 45 + ], + "601": [ + 45 + ] + }, + "exit": { + "123": [ + 45 + ], + "175": [ + 45 + ], + "183": [ + 45 + ], + "202": [ + 45 + ], + "600": [ + 45 + ], + "601": [ + 45 + ] + } + }, + "block_minimum_profile_under_fixed_monotone_boundaries": { + "1": 4 + }, + "block_paid_climbs_after": [ + [ + 202, + "B", + 77, + 1, + [], + [ + 45 + ] + ], + [ + 123, + "B", + 78, + 1, + [], + [ + 45 + ] + ], + [ + 183, + "B", + 82, + 1, + [], + [ + 45 + ] + ], + [ + 175, + "B", + 83, + 1, + [], + [ + 45 + ] + ] + ], + "block_paid_climbs_before": [ + [ + 183, + "B", + 77, + 1, + [], + [ + 45 + ] + ], + [ + 202, + "B", + 78, + 1, + [], + [ + 45 + ] + ], + [ + 175, + "B", + 79, + 1, + [], + [ + 45 + ] + ], + [ + 123, + "B", + 80, + 1, + [], + [ + 45 + ] + ] + ], + "canceled_cleanup_records_after": 5225, + "candidate_block": [ + [ + "add", + 202, + 600, + -1, + 4, + [ + 45 + ] + ], + [ + "add", + 123, + 600, + -1, + 4, + [ + 45 + ] + ], + [ + "add", + 202, + 601, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 123, + 601, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 600, + 601, + 1, + 1, + [ + 45 + ] + ], + [ + "add", + 183, + 600, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 175, + 600, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 600, + 601, + -1, + 1, + [ + 45 + ] + ] + ], + "defect_sensitive_controls": { + "clean_zero_sources_do_not_detect_missing_undo": true, + "missing_undo_rejected_on_arbitrary_dirty_sources": true, + "unpaid_read_only_source_frame_rejected": true, + "wrong_agreeing_target_sign_rejected": true, + "wrong_capture_sign_rejected": true, + "wrong_cleanup_inverse_sign_rejected": true, + "wrong_common_frame_rejected": true + }, + "helper_width_inventory": { + "5": 28, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "literal_cleanup_records_after": 5227, + "literal_cleanup_records_before": 5225, + "local_operation_counts": { + "after": { + "adds": 8, + "source_reads": { + "600": 4, + "601": 4 + }, + "source_writes": { + "600": 2, + "601": 0 + }, + "target_writes": 6 + }, + "before": { + "adds": 8, + "source_reads": { + "600": 4, + "601": 4 + }, + "source_writes": { + "600": 0, + "601": 0 + }, + "target_writes": 8 + } + }, + "matrix": [ + [ + "1", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "0", + "0", + "0" + ], + [ + "-1/4", + "1/4", + "1", + "0", + "0", + "0" + ], + [ + "1/4", + "1/4", + "0", + "1", + "0", + "0" + ], + [ + "1/4", + "1/4", + "0", + "0", + "1", + "0" + ], + [ + "-1/4", + "1/4", + "0", + "0", + "0", + "1" + ] + ], + "matrix_coordinates": [ + 600, + 601, + 123, + 175, + 183, + 202 + ], + "matrix_entry_coverage": 36, + "native_profile": { + "1": 2482, + "2": 712, + "3": 218, + "4": 109, + "5": 20, + "8": 8 + }, + "old_cleanup_equals_unsimplified_literal_recipe": false, + "old_cleanup_semantically_sufficient_after_exact_pair_cancellation": true, + "operation_invoice": { + "canceled_capture": { + "A": { + "operations": { + "add": 3557, + "scale": 498, + "warp": 24 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "B": { + "operations": { + "add": 1796, + "scale": 74 + }, + "source_access": { + "600": { + "reads": 6, + "writes": 7 + }, + "601": { + "reads": 6, + "writes": 5 + } + } + }, + "cleanup": { + "operations": { + "add": 4633, + "scale": 520, + "warp": 72 + }, + "source_access": { + "600": { + "reads": 1, + "writes": 5 + }, + "601": { + "reads": 1, + "writes": 5 + } + } + }, + "compensation": { + "operations": { + "add": 5736 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "cut": { + "operations": { + "add": 176 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "initial_corrections": 36, + "native_warps": 72, + "precondition": { + "operations": { + "add": 136, + "scale": 56 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "restore": { + "operations": { + "add": 196, + "scale": 16 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "source_reads_and_writes": { + "600": { + "reads": 7, + "writes": 12 + }, + "601": { + "reads": 7, + "writes": 10 + } + }, + "total_executed_records": 17598, + "totals_excluding_native_warps_and_corrections": { + "add": 16230, + "scale": 1164, + "warp": 96 + } + }, + "literal_capture": { + "A": { + "operations": { + "add": 3557, + "scale": 498, + "warp": 24 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "B": { + "operations": { + "add": 1796, + "scale": 74 + }, + "source_access": { + "600": { + "reads": 6, + "writes": 7 + }, + "601": { + "reads": 6, + "writes": 5 + } + } + }, + "cleanup": { + "operations": { + "add": 4635, + "scale": 520, + "warp": 72 + }, + "source_access": { + "600": { + "reads": 1, + "writes": 7 + }, + "601": { + "reads": 3, + "writes": 5 + } + } + }, + "compensation": { + "operations": { + "add": 5736 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "cut": { + "operations": { + "add": 176 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "initial_corrections": 36, + "native_warps": 72, + "precondition": { + "operations": { + "add": 136, + "scale": 56 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "restore": { + "operations": { + "add": 196, + "scale": 16 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "source_reads_and_writes": { + "600": { + "reads": 7, + "writes": 14 + }, + "601": { + "reads": 9, + "writes": 10 + } + }, + "total_executed_records": 17600, + "totals_excluding_native_warps_and_corrections": { + "add": 16232, + "scale": 1164, + "warp": 96 + } + }, + "original": { + "A": { + "operations": { + "add": 3557, + "scale": 498, + "warp": 24 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "B": { + "operations": { + "add": 1796, + "scale": 74 + }, + "source_access": { + "600": { + "reads": 6, + "writes": 5 + }, + "601": { + "reads": 6, + "writes": 5 + } + } + }, + "cleanup": { + "operations": { + "add": 4633, + "scale": 520, + "warp": 72 + }, + "source_access": { + "600": { + "reads": 1, + "writes": 5 + }, + "601": { + "reads": 1, + "writes": 5 + } + } + }, + "compensation": { + "operations": { + "add": 5736 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "cut": { + "operations": { + "add": 176 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "initial_corrections": 36, + "native_warps": 72, + "precondition": { + "operations": { + "add": 136, + "scale": 56 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "restore": { + "operations": { + "add": 196, + "scale": 16 + }, + "source_access": { + "600": { + "reads": 0, + "writes": 0 + }, + "601": { + "reads": 0, + "writes": 0 + } + } + }, + "source_reads_and_writes": { + "600": { + "reads": 7, + "writes": 10 + }, + "601": { + "reads": 7, + "writes": 10 + } + }, + "total_executed_records": 17598, + "totals_excluding_native_warps_and_corrections": { + "add": 16230, + "scale": 1164, + "warp": 96 + } + } + }, + "original_block": [ + [ + "add", + 183, + 600, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 202, + 600, + -1, + 4, + [ + 45 + ] + ], + [ + "add", + 175, + 600, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 123, + 600, + -1, + 4, + [ + 45 + ] + ], + [ + "add", + 183, + 601, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 202, + 601, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 175, + 601, + 1, + 4, + [ + 45 + ] + ], + [ + "add", + 123, + 601, + 1, + 4, + [ + 45 + ] + ] + ], + "paid_source_visits": { + "600": { + "entrance": [ + 45 + ], + "paid_visits": [ + [ + 600, + "B", + 936, + 4, + [ + 45 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + [ + 600, + "B", + 948, + 1, + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 385, + 72, + 40, + 24, + 5, + 2 + ] + ], + [ + 600, + "B", + 1470, + 1, + [ + 385, + 72, + 40, + 24, + 5, + 2 + ], + [ + 257, + 128, + 72, + 40, + 24, + 5, + 2 + ] + ], + [ + 600, + "B", + 1472, + 1, + [ + 257, + 128, + 72, + 40, + 24, + 5, + 2 + ], + [ + 257, + 128, + 65, + 33, + 17, + 9, + 5, + 2 + ] + ], + [ + 600, + "terminal", + null, + 1, + [ + 257, + 128, + 65, + 33, + 17, + 9, + 5, + 2 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ] + ], + "terminal": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + }, + "601": { + "entrance": [ + 45 + ], + "paid_visits": [ + [ + 601, + "B", + 937, + 4, + [ + 45 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + [ + 601, + "B", + 949, + 1, + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 408, + 80, + 40, + 4, + 2, + 1 + ] + ], + [ + 601, + "B", + 1474, + 1, + [ + 408, + 80, + 40, + 4, + 2, + 1 + ], + [ + 280, + 128, + 80, + 40, + 4, + 2, + 1 + ] + ], + [ + 601, + "B", + 1476, + 1, + [ + 280, + 128, + 80, + 40, + 4, + 2, + 1 + ], + [ + 272, + 128, + 80, + 32, + 8, + 4, + 2, + 1 + ] + ], + [ + 601, + "terminal", + null, + 1, + [ + 272, + 128, + 80, + 32, + 8, + 4, + 2, + 1 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ] + ], + "terminal": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + } + }, + "positive_climb_signature_sha256": "8bef883b7c40043c8d05f55417b2e19e03e0d09abfd33952679b50b36fa99e31", + "positive_native_climb_count": 3549, + "positive_native_rank_mass": 5160, + "source": { + "git_blob": "c531be7383ad3ba941600c7ced14e5e10d6d1c67", + "head": "f977a8a3dcb2983829d066a80420b7ded42d3e09", + "original_path": "research/staged544-helper600-sign-columns/frozen/WORD-extra.json.gz", + "sha256": "d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299" + } + } + } +} diff --git a/research/partial-helper-capture/independent/REVIEW.md b/research/partial-helper-capture/independent/REVIEW.md new file mode 100644 index 0000000000..68722703e6 --- /dev/null +++ b/research/partial-helper-capture/independent/REVIEW.md @@ -0,0 +1,121 @@ +# Independent mathematical review + +**Result: exact partial capture, zero recursive-profile gain.** The local +arbitrary-input identity, complete native-frame invoice, helper widths and +literal/canceled cleanup agree with the construction worker's artifact. Under +the same six physical block endpoints and monotone single-register child +contract, four rank-1 target climbs are also a sharp lower bound. The original +and candidate both attain it. No broader optimization or kappa claim passes. + +## Independent work and checked scope + +`INITIAL-DERIVATION.md` was saved before reading the construction worker's +checker. The frozen word bytes, source export, predecessor description and +PR4076-retained frame/cleanup contract had already been read. `check.py` does +not import the construction checker, retained audit core or any other project +module. It separately implements exact six-by-six rational matrices and GF(2) +row-basis elimination. This is a separate AI mathematical context, not +independent human review. + +The checker binds both compressed input SHA-256 values and Git blob hashes, +checks all 36 local matrix entries on arbitrary dirty source and target values, +and reconstructs every positive native climb and every helper width. It +compares chronological positive frame paths separately for each register, +including the entering/outgoing bases; local event indices may move. Both +sources' positive event indices remain unchanged. Source-access counts include +all scalar stages; explicit checks exclude extra accesses through native warps +or initial corrections for helpers 600 and 601. + +The independent comparison certifies substitution of the local physical +operator into the unchanged surrounding word. It does not independently +reimplement the primary checker's complete 723-coordinate free-group-algebra +evaluator, certify its predecessor endpoint theorem from scratch, or certify +native Clifford phases. The primary checker separately reports those finite +symbolic-map checks, with the source audit implementation disclosed. + +## Substantive findings and corrections + +- The local capture and undo restore helper 600 for every entering value of + helper 601. Target diagonal coefficients are all one; neither clean targets + nor clean helpers are assumed. +- The sources already enter at `[45]`, but the four targets enter at `[]`. + Therefore the block has four target rank-1 calls, not zero total calls. + The independent result records all six entry and exit frames and the four + calls before and after. No target call is eliminated by merging two reads. +- The unsimplified inverse cleanup has two extra FULL-frame helper shears. + They are adjacent inverse gates and cancel exactly. The old cleanup is + semantically valid after that cancellation; describing it as the unchanged + unsimplified inverse recipe is a representation error. This distinction is + checked explicitly, not hidden behind a stale-cleanup negative control. +- The complete profile is `{1:2482,2:712,3:218,4:109,5:20,8:8}` and the helper + widths are `{5:28,6:18,7:53,8:96,9:213}` before and after. There are 3,549 + positive child calls and rank mass 5,160. Both sources retain the positive + climb chain `(4,1,1,1,1)`, width eight and exact paid source-visit addresses. +- Full executed record counts are 17,598 originally, 17,600 with literal + cleanup and 17,598 after cancellation. Both source roles and all later paid + source climbs remain. Two specific target reads are exchanged for capture + and undo reads; wording about unchanged source *events* must refer to paid + visits rather than literal scalar events. +- Read-only operands receive frame checks. A separate malformed control uses + a legal zero-frame destination with an illegal `[45]`-frame source; it is + rejected at the source operand. Wrong target/capture signs, missing undo, + a wrong common frame and an incorrect inverse sign are also rejected. +- The source-credit lineage is Rohan Arun's PR4076 retention of Sagar Thakrar's + PR3687 code, with Arham Tahir's earlier contract credit retained. + +The local minimum argument in `PROOF.md` is a written all-rewrite statement +under its fixed boundaries: the dimension increments on each target sum to +one and are nonnegative integers, so each physical target requires one +rank-1 child. It allows arbitrary scalar couplings within this model. It is +not an all-interface statement: changed boundaries, external retiming, +physical ownership, descent/reset permissions and a changed joint-child ABI +remain outside it. + +## Validation and artifact binding + +Final checks passed with Python 3.12.12, standard library only: + +``` +python3.12 -I -B research/partial-helper-capture/independent/check.py +python3.12 -I -B -O research/partial-helper-capture/independent/check.py +``` + +Both emit `PASS_PARTIAL_CAPTURE_INDEPENDENT`; the default compares the freshly +computed deterministic receipt without writing files. The receipt was first +generated by the same checker using its explicit absolute `--output` option. +The malformed-witness controls pass in normal and optimized Python. The primary +and independent JSON reports were also compared for exact candidate gates, +complete profile, width inventory, cancellation location and all three total +record counts on both words; those comparisons passed. The primary checker was +read after the independent derivation and implementation were established; it +was never imported or executed by this independent checker. + +Reviewed file SHA-256 values, relative to the package: + +| file | SHA-256 | +| --- | --- | +| `independent/check.py` | `8ae562ae150866e1c8920c112b14ca7d5d0963527c2599d1edb43864006a8687` | +| `independent/PROOF.md` | `dc25260c85b47d4e47d44ba3f7c5565abf13d43649daa4f331038924dfb07112` | +| `independent/RESULT.json` | `5cba1543742ca3d01f9049ad92d93caa9f02155a97e0d5e09f2709fbc9714b20` | +| `independent/INITIAL-DERIVATION.md` | `ece1a367b635dd47212e66f98c86e0450fff61bd49b4c4bb3c94faf77b7cc7f0` | +| `construction/verify.py` | `d9335bfeed8db914404adb486797829f9913b8c00a5210c00be45e29a4cdab64` | +| `construction/DERIVATION.md` | `7d90b3d977a4b2ffccb496e7116a21e93cd189ebffb10b3d666a8fb1864306b6` | +| `construction/RESULT.json` | `7fb8347e2103cec0d0ebfbcfa87348a3b3113c22e6c16985e9f8f9554e808a9d` | + +These are content bindings, not signatures, hosted CI or formal-kernel evidence. +Meaningful later edits invalidate the affected binding and checks. + +## Mathematical stop and remaining limits + +The smallest decisive obligation is complete: this exact partial capture cannot +save the paid rank profile or a helper width under the specified interface, +even after the favorable certified cleanup cancellation. Its fixed-boundary +block floor is already attained by the predecessor. This warrants stopping the +mechanism test, without broadening to another capture family. + +No physical supplier, precision theorem, tape/controller realization, owner +allocation improvement, all-size recurrence improvement or new kappa is +established. A useful successor must change and fully price a further boundary +or delivery contract; this result supplies no such successor. Parent-run +preservation, public submission, hosted checks and lifecycle closeout are +separate obligations outside this mathematical review. diff --git a/research/partial-helper-capture/independent/check.py b/research/partial-helper-capture/independent/check.py new file mode 100644 index 0000000000..7d1131338f --- /dev/null +++ b/research/partial-helper-capture/independent/check.py @@ -0,0 +1,517 @@ +#!/usr/bin/env python3 +"""Separate exact local matrix proof and complete BORROW-WORD frame invoice. + +No project module is imported. GF(2) frames use reduced row bases, rather than +the point-set bit masks in the PR4076 contract reference. Rational matrices are +composed from elementary row operations on all six independent dirty inputs. +The imported-source format/cleanup contract was read, not independently invented. +""" +import argparse +from collections import Counter +from copy import deepcopy +from fractions import Fraction +import gzip +import hashlib +import json +from pathlib import Path + + +ROOT = Path(__file__).resolve().parents[1] +HERE = Path(__file__).resolve().parent +FULL = tuple(1 << k for k in range(8, -1, -1)) +N = 704 +TARGETS = range(112, 224) +LOCAL = (600, 601, 123, 175, 183, 202) +EXPECTED = { + "base": "08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0", + "extra": "d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299", +} + + +class Invalid(Exception): + pass + + +def need(value, description): + if not value: + raise Invalid(description) + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def digest_json(value): + return sha(json.dumps(value, sort_keys=True, separators=(",", ":")).encode()) + + +def row_basis(vectors): + pivots = {} + for vector in vectors: + need(type(vector) is int and 0 <= vector < 512, "GF(2) vector outside nine bits") + x = vector + for p in sorted(pivots, reverse=True): + if x & (1 << p): + x ^= pivots[p] + if x: + p = x.bit_length() - 1 + for q in list(pivots): + if pivots[q] & (1 << p): + pivots[q] ^= x + pivots[p] = x + return tuple(pivots[p] for p in sorted(pivots, reverse=True)) + + +def contained(small, large): + return all(row_basis((*large, v)) == large for v in small) + + +def hyperplane(port): + need(type(port) is int and 0 < port < 512, "nonzero port required") + pivot = (port & -port).bit_length() - 1 + return row_basis((1 << j) ^ ((1 << pivot) if port & (1 << j) else 0) + for j in range(9) if j != pivot) + + +def operands(g): + need(g[0] in ("add", "scale"), "unknown scalar gate") + return g[1:3] if g[0] == "add" else g[1:2] + + +def basis_image(columns, frame, inverse=False): + need(len(columns) == 9 and row_basis(columns) == FULL, "noninvertible warp") + + def image(x): + result = 0 + for j in range(9): + if x & (1 << j): + result ^= columns[j] + return result + + if inverse: + lookup = {image(x): x for x in range(512)} + return row_basis(lookup[x] for x in frame) + return row_basis(image(x) for x in frame) + + +def audit_gate(g, current, stage, index, ledger): + frame = row_basis(g[-1]) + for r in operands(g): + need(r in current, f"absent scalar operand {r}") + old = current[r] + need(contained(old, frame), f"frame descent at {stage}:{index}, operand {r}") + rank = len(frame) - len(old) + if rank: + ledger.append([r, stage, index, rank, list(old), list(frame)]) + current[r] = frame + + +def frame_invoice(w): + need((w['report']['v'], w['report']['R'], w['report']['h']) == (112, 480, 9), + "fixed geometry") + removed = set(w['removed']) + need(len(removed) == len(w['removed']) and removed <= set(range(224, N)), + "removed helper set") + live = sorted(set(range(N)) - removed) + starts = {} + ends = {} + for r in live: + starts[r] = row_basis([w['ports'][r]]) if r < 112 else () + ends[r] = hyperplane(w['ports'][r - 112]) if r in TARGETS else FULL + for key, frame in w['start_extra'].items(): + r = int(key) + need(r in starts and r >= 224, "helper entrance register") + starts[r] = row_basis(frame) + for key, frame in w['helper_final'].items(): + r = int(key) + need(r in ends and r >= 224, "helper terminal register") + ends[r] = row_basis(frame) + current = dict(starts) + paid = [] + warps = w['warps'] + for pos, r, cols, old, new in warps: + need(0 <= pos <= len(w['B']) and r in current and r not in TARGETS, + "native warp address") + need(len(row_basis(old)) == len(old) == len(new) == len(row_basis(new)), + "warp frame dimensions") + need(basis_image(cols, row_basis(old)) == row_basis(new), "warp frame image") + for i, g in enumerate(w['A']): + if g[0] == 'warp': + need(i < w['prelude_events'] and len(g) == 5, "prelude warp record") + _, r, operator, old, new = g + need(0 < abs(operator) <= len(warps), "prelude operator index") + rec = warps[abs(operator) - 1] + need(rec[1] == r and current[r] == row_basis(old), "prelude warp entrance") + need(basis_image(rec[2], row_basis(old), operator < 0) == row_basis(new), + "prelude warp action") + current[r] = row_basis(new) + else: + if i < w['prelude_events']: + need(g[1] in TARGETS, "prelude writes helper") + audit_gate(g, current, 'A', i, paid) + levels = {112 + int(k): row_basis(v) for k, v in w['target_levels'].items()} + need(all(current[r] == levels.get(r, ()) for r in TARGETS), "cut target frames") + for r, entry in zip(w['centers'], w['center_frames']): + cursor = row_basis(entry) + need(current[r] == cursor, "center entrance") + served = {levels.get(g[1], ()) for g in w['cut'] if g[2] == r} + for destination in sorted(served, key=lambda b: (-len(b), b)): + need(contained(destination, cursor), "nested center service frames") + rank = len(cursor) - len(destination) + if rank: + paid.append([r, 'center-service', None, rank, + list(cursor), list(destination)]) + cursor = destination + indexed = {} + for i, rec in enumerate(warps): + indexed.setdefault(rec[0], []).append((i, rec)) + block_boundaries = {} + for pos in range(len(w['B']) + 1): + for k, (_, r, _, old, new) in indexed.get(pos, []): + need(current[r] == row_basis(old), f"native warp entrance {k + 1}") + current[r] = row_basis(new) + if pos in (77, 85): + block_boundaries[pos] = {r: current[r] for r in LOCAL} + if pos < len(w['B']): + audit_gate(w['B'][pos], current, 'B', pos, paid) + for i, g in enumerate(w['restore']): + audit_gate(g, current, 'restore', i, paid) + for r in live: + need(contained(current[r], ends[r]), f"terminal containment {r}") + rank = len(ends[r]) - len(current[r]) + if rank: + paid.append([r, 'terminal', None, rank, list(current[r]), list(ends[r])]) + current[r] = ends[r] + # The literal tail executes at FULL or on terminal-helper backing buffers; + # these inverse records are scalar operations, not fresh frame promotions. + histogram = Counter(record[3] for record in paid) + widths = Counter(len(ends[r]) - len(starts[r]) for r in live if r >= 224) + need(all(width >= 0 for width in widths), "negative endpoint width") + return { + 'profile': dict(sorted(histogram.items())), + 'widths': dict(sorted(widths.items())), + 'paid': paid, + 'starts': starts, + 'ends': ends, + 'block_boundaries': block_boundaries, + } + + +def local_matrix(gates): + rows = [[Fraction(i == j) for j in range(6)] for i in range(6)] + coordinates = {r: i for i, r in enumerate(LOCAL)} + for g in gates: + need(g[0] == 'add' and g[1] in coordinates and g[2] in coordinates, + "local matrix gate") + t, s = coordinates[g[1]], coordinates[g[2]] + q = Fraction(g[3], g[4]) + rows[t] = [a + q * b for a, b in zip(rows[t], rows[s])] + return rows + + +def expected_matrix(): + answer = [[Fraction(i == j) for j in range(6)] for i in range(6)] + for i, sign in [(2, -1), (3, 1), (4, 1), (5, -1)]: + answer[i][0] = Fraction(sign, 4) + answer[i][1] = Fraction(1, 4) + return answer + + +def candidate_block(original): + need(original == [ + ['add', 183, 600, 1, 4, [45]], ['add', 202, 600, -1, 4, [45]], + ['add', 175, 600, 1, 4, [45]], ['add', 123, 600, -1, 4, [45]], + ['add', 183, 601, 1, 4, [45]], ['add', 202, 601, 1, 4, [45]], + ['add', 175, 601, 1, 4, [45]], ['add', 123, 601, 1, 4, [45]], + ], "source block differs from pinned signed columns") + return [deepcopy(original[i]) for i in (1, 3, 5, 7)] + [ + ['add', 600, 601, 1, 1, [45]], + ['add', 183, 600, 1, 4, [45]], + ['add', 175, 600, 1, 4, [45]], + ['add', 600, 601, -1, 1, [45]], + ] + + +def ordinary_actions(w): + actions = deepcopy(w['A'][w['prelude_events']:]) + indexed = {} + for k, rec in enumerate(w['warps'], 1): + indexed.setdefault(rec[0], []).append(['warp', rec[1], k]) + for i in range(len(w['B']) + 1): + actions.extend(indexed.get(i, [])) + if i < len(w['B']): + actions.append(w['B'][i]) + actions.extend(w['restore']) + return actions + + +def literal_cleanup(w): + restored = set(map(int, w['helper_final'])) + + def backing(r): + return r + N if r in restored else r + + answer = [] + for g in reversed(ordinary_actions(w)): + if g[0] == 'warp': + answer.append(['warp', backing(g[1]), -g[2], list(FULL)]) + elif g[1] in TARGETS: + continue + elif g[0] == 'add': + answer.append(['add', backing(g[1]), backing(g[2]), -g[3], g[4], list(FULL)]) + else: + need(g[0] == 'scale', "unknown cleanup inverse") + answer.append(['scale', backing(g[1]), g[3], g[2], list(FULL)]) + return answer + + +def normalized_tail(gates): + return [(*g[:-1], row_basis(g[-1])) for g in gates] + + +def cancel_added_pair(tail, old_tail): + plus = ['add', 600, 601, 1, 1, list(FULL)] + minus = ['add', 600, 601, -1, 1, list(FULL)] + hits = [i for i in range(len(tail) - 1) if tail[i:i + 2] == [plus, minus]] + need(len(hits) == 1, "unique added adjacent inverse cleanup pair") + i = hits[0] + reduced = tail[:i] + tail[i + 2:] + need(normalized_tail(reduced) == normalized_tail(old_tail), "canceled cleanup equals source") + return reduced, i + + +def op_counts(w): + answer = {} + totals = Counter() + sources = {r: {'reads': 0, 'writes': 0} for r in (600, 601)} + for name in ('precondition', 'compensation', 'A', 'cut', 'B', 'restore', 'cleanup'): + ops = Counter(g[0] for g in w[name]) + stage_sources = {str(r): {'reads': 0, 'writes': 0} for r in sources} + answer[name] = {'operations': dict(sorted(ops.items())), 'source_access': stage_sources} + totals.update(ops) + for g in w[name]: + for r in sources: + if g[0] == 'add' and g[2] == r: + sources[r]['reads'] += 1 + stage_sources[str(r)]['reads'] += 1 + if g[1] == r: + sources[r]['writes'] += 1 + stage_sources[str(r)]['writes'] += 1 + answer['totals_excluding_native_warps_and_corrections'] = dict(sorted(totals.items())) + answer['native_warps'] = len(w['warps']) + answer['initial_corrections'] = len(w['initial_corrections']) + answer['total_executed_records'] = sum(len(w[name]) for name in ( + 'precondition', 'compensation', 'A', 'cut', 'B', 'restore', 'cleanup')) \ + + len(w['warps']) + len(w['initial_corrections']) + answer['source_reads_and_writes'] = sources + return answer + + +def count_local(gates): + return { + 'adds': len(gates), + 'source_reads': {str(r): sum(g[2] == r for g in gates) for r in (600, 601)}, + 'source_writes': {str(r): sum(g[1] == r for g in gates) for r in (600, 601)}, + 'target_writes': sum(g[1] in TARGETS for g in gates), + } + + +def rejected(action): + try: + action() + except Invalid: + return True + return False + + +def controls(original, candidate, w): + target = expected_matrix() + bad_sign = deepcopy(candidate) + bad_sign[5][3] = -1 + wrong_capture = deepcopy(candidate) + wrong_capture[4][3] = -1 + missing_undo = candidate[:-1] + bad_frame = deepcopy(w) + bad_frame['B'][77:85] = deepcopy(candidate) + bad_frame['B'][81][-1] = [46] + # A fresh ZERO-frame recipient is legal, but its [45]-frame read-only + # source cannot be silently admitted at ZERO. This isolates source access. + control_frames = {700: (), 600: row_basis([45])} + control_gate = ['add', 700, 600, 1, 1, []] + bad_inverse = [g for g in reversed(candidate) if g[1] not in TARGETS] + bad_inverse = deepcopy(bad_inverse) + for g in bad_inverse: + g[3] = -g[3] + bad_inverse[-1][3] *= -1 + only_source_forward = [g for g in candidate if g[1] not in TARGETS] + identity = [[Fraction(i == j) for j in range(6)] for i in range(6)] + result = { + 'wrong_agreeing_target_sign_rejected': local_matrix(bad_sign) != target, + 'wrong_capture_sign_rejected': local_matrix(wrong_capture) != target, + 'missing_undo_rejected_on_arbitrary_dirty_sources': local_matrix(missing_undo) != target, + 'wrong_common_frame_rejected': rejected(lambda: frame_invoice(bad_frame)), + 'unpaid_read_only_source_frame_rejected': rejected( + lambda: audit_gate(control_gate, control_frames, 'control', 0, [])), + 'wrong_cleanup_inverse_sign_rejected': + local_matrix(only_source_forward + bad_inverse) != identity, + 'clean_zero_sources_do_not_detect_missing_undo': + all(row[j] == target[i][j] for i, row in enumerate(local_matrix(missing_undo)) + for j in range(2, 6)), + } + need(all(result.values()), "one defect-sensitive control failed") + return result + + +def load_word(name, manifest): + rel = f'predecessor4061/frozen/WORD-{name}.json.gz' + data = (ROOT / rel).read_bytes() + recs = [s for s in manifest['sources'] if s['local_path'] == rel] + need(len(recs) == 1, "source export does not identify one frozen word") + record = recs[0] + need(sha(data) == EXPECTED[name] == record['sha256'], "frozen word SHA-256") + blob = hashlib.sha1(b'blob ' + str(len(data)).encode() + b'\0' + data).hexdigest() + need(blob == record['git_blob'], "frozen word Git blob") + return json.loads(gzip.decompress(data)), { + 'sha256': sha(data), 'git_blob': blob, 'head': record['head'], + 'original_path': record['original_path'], + } + + +def verify_word(name, manifest): + w, source = load_word(name, manifest) + need(all(rec[1] not in (600, 601) for rec in w['warps']), + "capture helpers have no uncounted native-warp accesses") + need(all(rec['source'] not in (600, 601) for rec in w['initial_corrections']), + "capture helpers have no uncounted initial-correction reads") + original = w['B'][77:85] + candidate = candidate_block(original) + target = expected_matrix() + need(local_matrix(original) == target == local_matrix(candidate), + "complete 36-entry dirty-input rational matrix identity") + source_only = [g for g in candidate if g[1] not in TARGETS] + identity = [[Fraction(i == j) for j in range(6)] for i in range(6)] + need(local_matrix(source_only) == identity, "source subword identity") + literal_old = literal_cleanup(w) + need(normalized_tail(literal_old) == normalized_tail(w['cleanup']), + "source literal inverse recipe") + changed = deepcopy(w) + changed['B'][77:85] = candidate + changed['cleanup'] = literal_cleanup(changed) + reduced_tail, cancellation_index = cancel_added_pair(changed['cleanup'], w['cleanup']) + reduced = deepcopy(changed) + reduced['cleanup'] = reduced_tail + a = frame_invoice(w) + b = frame_invoice(changed) + need(a['profile'] == b['profile'], "full native child profile unchanged") + need(a['widths'] == b['widths'], "all helper widths unchanged") + need(a['starts'] == b['starts'] and a['ends'] == b['ends'], "all external boundaries unchanged") + # Stable sorting groups registers while retaining each chronological path. + paths_a = sorted([[r, rank, old, new] for r, _, _, rank, old, new in a['paid']], + key=lambda rec: rec[0]) + paths_b = sorted([[r, rank, old, new] for r, _, _, rank, old, new in b['paid']], + key=lambda rec: rec[0]) + need(paths_a == paths_b, "every positive native climb remains") + need(a['block_boundaries'] == b['block_boundaries'], "six block boundary frames unchanged") + entry = a['block_boundaries'][77] + exit_frames = a['block_boundaries'][85] + need(all(entry[r] == row_basis([45]) for r in (600, 601)), "block source entry frames") + need(all(entry[r] == () for r in (123, 175, 183, 202)), "block target entry frames") + need(all(exit_frames[r] == row_basis([45]) for r in LOCAL), "block exit frames") + local_paid_a = [rec for rec in a['paid'] if rec[1] == 'B' and 77 <= rec[2] < 85] + local_paid_b = [rec for rec in b['paid'] if rec[1] == 'B' and 77 <= rec[2] < 85] + need(Counter(rec[3] for rec in local_paid_a) == Counter({1: 4}) + == Counter(rec[3] for rec in local_paid_b), "four unavoidable local target climbs") + need(a['profile'] == {int(k): v for k, v in w['report']['local_profile'].items()}, + "independently reconstructed native profile matches frozen report") + need(a['widths'] == {int(k): v for k, v in w['report']['width_inventory'].items()}, + "independently reconstructed helper widths match frozen report") + source_chains = {} + for r in (600, 601): + before = [rec for rec in a['paid'] if rec[0] == r] + after = [rec for rec in b['paid'] if rec[0] == r] + need(before == after, "paid source visits unchanged, including chronological addresses") + need(a['starts'][r] == row_basis([45]) and a['ends'][r] == FULL, + "source entrance and terminal frame") + source_chains[r] = {'entrance': [45], 'terminal': list(FULL), 'paid_visits': before} + tail_pair = changed['cleanup'][cancellation_index:cancellation_index + 2] + need(local_matrix(tail_pair) == identity, "added full-frame inverse pair cancels on dirty inputs") + # These two statements are deliberately distinct: algebraic sufficiency + # after cancellation does not mean equality to the literal recipe. + need(normalized_tail(changed['cleanup']) != normalized_tail(w['cleanup']), + "literal recipe must detect the omitted adjacent pair") + need(normalized_tail(reduced['cleanup']) == normalized_tail(w['cleanup']), + "canceled recipe equals old cleanup exactly") + source_stages = {} + for label, word in [('original', w), ('literal_capture', changed), ('canceled_capture', reduced)]: + source_stages[label] = op_counts(word) + return { + 'source': source, + 'matrix_coordinates': list(LOCAL), + 'matrix_entry_coverage': 36, + 'matrix': [[str(x) for x in row] for row in target], + 'original_block': original, + 'candidate_block': candidate, + 'local_operation_counts': {'before': count_local(original), 'after': count_local(candidate)}, + 'literal_cleanup_records_before': len(w['cleanup']), + 'literal_cleanup_records_after': len(changed['cleanup']), + 'canceled_cleanup_records_after': len(reduced['cleanup']), + 'added_cleanup_pair_index': cancellation_index, + 'added_cleanup_pair': tail_pair, + 'old_cleanup_semantically_sufficient_after_exact_pair_cancellation': True, + 'old_cleanup_equals_unsimplified_literal_recipe': False, + 'native_profile': a['profile'], + 'helper_width_inventory': a['widths'], + 'positive_native_climb_count': len(a['paid']), + 'positive_native_rank_mass': sum(g[3] for g in a['paid']), + 'all_positive_climbs_per_register_unchanged': True, + 'positive_climb_signature_sha256': digest_json(paths_a), + 'all_external_frames_unchanged': True, + 'block_boundary_frames': { + 'entry': {str(k): list(v) for k, v in entry.items()}, + 'exit': {str(k): list(v) for k, v in exit_frames.items()}, + }, + 'block_paid_climbs_before': local_paid_a, + 'block_paid_climbs_after': local_paid_b, + 'block_minimum_profile_under_fixed_monotone_boundaries': {1: 4}, + 'paid_source_visits': source_chains, + 'operation_invoice': source_stages, + 'defect_sensitive_controls': controls(original, candidate, w), + } + + +def report(): + manifest_bytes = (ROOT / 'SOURCE-EXPORT.json').read_bytes() + manifest = json.loads(manifest_bytes) + words = {name: verify_word(name, manifest) for name in EXPECTED} + need(words['base']['matrix'] == words['extra']['matrix'], "both frozen words local matrix") + return { + 'schema_version': 1, + 'result': 'EXACT_PARTIAL_CAPTURE_WITH_ZERO_NATIVE_PROFILE_GAIN', + 'coverage': 'Two pinned finite words; exact rational local operator on arbitrary dirty inputs; complete native-frame and helper-width invoice under the BORROW-WORD contract.', + 'physical_lift': 'All eight replaced ADDs and all eight candidate ADDs use the identical [45] representative; exact logical matrix equality gives exact physical equality for any fixed invertible T_[45].', + 'universal_cost_comparison_scope': 'The explicit rewrite retains every positive native climb and endpoint width, so every price depending on that invoice is unchanged. More generally, monotone scalar rewrites at the same six block-boundary frames require all four ZERO-to-[45] target climbs, hence at least four rank-1 children. The original and explicit capture attain that local minimum. No global claim with changed external boundaries or paid itinerary is made.', + 'unresolved': 'Changed entrances or terminals, larger source sets, cross-block retiming, other child/hosting contracts, and global resynthesis are not excluded. No physical supplier, full recurrence improvement or new kappa is established.', + 'source_export_sha256': sha(manifest_bytes), + 'implementation_sha256': sha(Path(__file__).read_bytes()), + 'contract_reference': 'source4076/vendor/audit_core.py was read for BORROW-WORD frame/cleanup semantics; no project module imported. RREF arithmetic and local matrix evaluation implemented separately.', + 'words': words, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--output', type=Path, help='Write verified JSON to this absolute path; otherwise compare independent/RESULT.json without writing.') + args = parser.parse_args() + result = report() + serialized = json.dumps(result, indent=2, sort_keys=True) + '\n' + if args.output is not None: + need(args.output.is_absolute(), '--output must be absolute') + args.output.write_text(serialized) + else: + expected = (HERE / 'RESULT.json').read_text() + need(serialized == expected, 'current calculation differs from independent/RESULT.json') + print('PASS_PARTIAL_CAPTURE_INDEPENDENT') + + +if __name__ == '__main__': + main() diff --git a/research/partial-helper-capture/predecessor4061/README.md b/research/partial-helper-capture/predecessor4061/README.md new file mode 100644 index 0000000000..0ff1289a3b --- /dev/null +++ b/research/partial-helper-capture/predecessor4061/README.md @@ -0,0 +1,96 @@ +# Signed columns of staged544 helpers 600 and 601 + +**Negative result. No new kappa.** The selected record is unchanged. + +## Scope + +The drawn catalogue card was `p104-side-correction`. Its named experiment, one +collection from #2981 with acquisition times, coefficients and dirty +restoration, is already open for flag 0 in #3915, #3669 and #3683. The same +present-head scan covers flags 1, 9 and 43, so another flag pass is the +card's pending-follow-up trigger. + +The next catalogue suggestion is `complex-rank-shape-decoder`. Its ideal +rank-16 screen already clears 5% in `levers.py`, and repacking the selected +word's idle remainder is a scope-change trigger of that card. The live handoff +in discussion 1166, comment 19038903, names a smaller unclaimed test on the +same alphabet that #4045 just bound: whether the complete consumer columns of +actual helpers 600 and 601 are signed-proportional under one common native +frame. This package runs that test. It does not emit a capture. + +## What is established + +Both frozen PR3945 words used by #4045 (`91afbb643f7f4ccf6f34b685ecd959eb790a0f94`) +carry the same consumer adds for helpers 600, 601, 602 and 604. Each helper is +read by exactly seven `add` events. The only frame common to the 600 and 601 +reads is `(45,)`, and on that frame the consumers are exactly 123, 175, 183 +and 202, each with coefficient ±1. + +In that consumer order the columns are + +| helper | 123 | 175 | 183 | 202 | +| --- | ---: | ---: | ---: | ---: | +| 600 | -1 | +1 | +1 | -1 | +| 601 | +1 | +1 | +1 | +1 | +| 602 | -1 | +1 | +1 | +1 | +| 604 | -1 | -1 | +1 | -1 | + +On both frozen PR3945 words, the frame-(45,) consumer columns of helpers 600 and 601 are neither equal nor opposite. + +The same split holds for every pair among the four helpers: each pair agrees +on some of these consumers and disagrees on others. A capture that needs one +global sign, as in the H6 same-frame sum/difference of #4048, therefore does +not apply to this group. Flipping the two disagreeing entries of column 601 +makes it equal to column 600, so the checker is not rejecting every pattern. + +The two word files are not identical. Their SHA-256 values are +`08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0` and +`d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299`, matching +git blobs `806784bf99d9d15004d2d227d06268556a0726c8` and +`c531be7383ad3ba941600c7ced14e5e10d6d1c67` at the #4045 head. Only the named +consumer columns were compared. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/staged544-helper600-sign-columns +``` + +The direct check also works without Git: + +```sh +python3.12 -B research/staged544-helper600-sign-columns/verify.py +``` + +Expected marker: `PASS_STAGED544_HELPER600_SIGN_COLUMNS`. + +## Limits + +This does not rerun the #4045 support obstruction, the #4031 rank-4 screen, or +the #4048 H6 lattice. It does not price a partial capture, a nonmonomial +encoder, or any other helper pair. Adds where these helpers are destinations +are productions, not consumer columns, and are not part of the sign test. +No supplier, hosting bill, or selected-frontier change is claimed. The selected +baseline replay was not run: this checkout does not contain the assembly roots +that `research_baseline.py` imports. + +## Open next questions + +Can a capture that keeps the disagreeing consumers 123 and 202, and merges +only the agreeing consumers 175 and 183, reduce the complete child and +restoration bill? Those two consumers already share a sign, but the other two +do not, so both helpers stay necessary. A first step is to price one explicit +partial capture of consumers 175 and 183, including cleanup, against the +0.03825 allowance in #4045. No such map is exhibited here. + +## Credit + +Dugongue / #3945 supplies the two words. Chris R / Clear1nsight / #4045 +identifies helpers 600, 601, 602 and 604 and the rank-16 support obstruction. +Tekalign / #4048 supplies the same-frame signed-capture idea that this test +refuses to transfer. Gonzalo Mier / #4031 supplies the zero-charge screen +#4045 already separated from this interface. Riquelme Soares (@hevlyo), with +substantial AI assistance in the extraction, checker and write-up. Apache-2.0. +No independent human review is claimed. diff --git a/research/partial-helper-capture/predecessor4061/SOURCES.json b/research/partial-helper-capture/predecessor4061/SOURCES.json new file mode 100644 index 0000000000..0839f4876a --- /dev/null +++ b/research/partial-helper-capture/predecessor4061/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ] +} diff --git a/research/partial-helper-capture/predecessor4061/TASK.json b/research/partial-helper-capture/predecessor4061/TASK.json new file mode 100644 index 0000000000..40e8cff79c --- /dev/null +++ b/research/partial-helper-capture/predecessor4061/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. 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", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "refined", + "actual_scope": "On the actual PR3945 consumer columns of helpers 600 and 601, is there one common native frame where the two coefficient columns are equal or opposite?", + "scope_change_reason": "The drawn card was p104-side-correction. Its named first experiment, one #2981 collection with times, coefficients and dirty restoration, is already open for flag 0 in #3915, #3669 and #3683, and the same present-head scanner covers flags 1, 9 and 43. Repeating that scan is the card's pending-follow-up trigger. The second suggestion is this rank-shape card. Its ideal rank-16 ceiling already clears the 5% screen in levers.py, and repacking the selected word's idle remainder is a stated scope-change trigger. The live handoff at discussion 1166 comment 19038903 names an unclaimed test on this same alphabet: signed proportionality of the complete consumer columns of actual helpers 600 and 601. This package runs that test and stops.", + "bottleneck_link": "Helpers 600 and 601 are two of the four actual rank-4 climbs whose one-call rank-16 transfer is already blocked. A same-frame signed capture would be a copy saving on that fixed alphabet. If their consumer columns are not equal or opposite, that capture cannot replace either climb, so the group's effective child rank stays four rank-4 calls.", + "budget_minutes": 60, + "stop_rule": "Stop when every consumer add of helpers 600 and 601 on both frozen words is classified at its frame. Do not emit a capture, retimed provider or search of other helpers.", + "outcome": "negative-result", + "evidence": "Both frozen words, SHA-256 08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0 and d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299, give the same frame-(45,) columns. In consumer order 123,175,183,202 the signs are 600=(-1,+1,+1,-1) and 601=(+1,+1,+1,+1). Both ratios +1 and -1 occur, so no single sign matches them. The same split occurs for every pair among 600,601,602,604. A one-entry sign flip of 601 makes it equal to 600, so the checker is not vacuously negative.", + "author": "Riquelme Soares (@hevlyo)", + "ai_assistance": "Substantial AI assistance was used for the overlap check, column extraction, verifier and write-up. No independent human review is claimed.", + "open_questions": [ + { + "question": "Can a capture that keeps the disagreeing consumers 123 and 202, and merges only the agreeing consumers 175 and 183, reduce the complete child and restoration bill?", + "why_it_matters": "Those two consumers already have the same sign on helpers 600 and 601, but the other two do not, so a full-column capture is impossible. A partial merge would still leave both helpers alive.", + "first_step": "Price one explicit partial capture of consumers 175 and 183 only, including its cleanup, and compare it with the 0.03825 allowance recorded by PR4045.", + "blocked_by": "No such partial map is exhibited, and both helpers remain necessary for consumers 123 and 202." + } + ] +} diff --git a/research/partial-helper-capture/predecessor4061/VERIFY.json b/research/partial-helper-capture/predecessor4061/VERIFY.json new file mode 100644 index 0000000000..97440ad70b --- /dev/null +++ b/research/partial-helper-capture/predecessor4061/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Hashes both frozen words, reconstructs every consumer add of helpers 600 and 601, rejects a single sign on frame (45,), and accepts the one-entry sign-flip control." + } + ] +} diff --git a/research/partial-helper-capture/predecessor4061/frozen/WORD-base.json.gz b/research/partial-helper-capture/predecessor4061/frozen/WORD-base.json.gz new file mode 100644 index 0000000000..806784bf99 Binary files /dev/null and b/research/partial-helper-capture/predecessor4061/frozen/WORD-base.json.gz differ diff --git a/research/partial-helper-capture/predecessor4061/frozen/WORD-extra.json.gz b/research/partial-helper-capture/predecessor4061/frozen/WORD-extra.json.gz new file mode 100644 index 0000000000..c531be7383 Binary files /dev/null and b/research/partial-helper-capture/predecessor4061/frozen/WORD-extra.json.gz differ diff --git a/research/partial-helper-capture/predecessor4061/verify.py b/research/partial-helper-capture/predecessor4061/verify.py new file mode 100644 index 0000000000..7a2dd9f306 --- /dev/null +++ b/research/partial-helper-capture/predecessor4061/verify.py @@ -0,0 +1,100 @@ +"""Consumer-column sign test for staged544 helpers 600 and 601.""" + +import gzip +import hashlib +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +HELPERS = (600, 601, 602, 604) +FRAME = (45,) +ORDER = (123, 175, 183, 202) +SIGNS = { + 600: (-1, 1, 1, -1), + 601: (1, 1, 1, 1), + 602: (-1, 1, 1, 1), + 604: (-1, -1, 1, -1), +} +HASHES = { + "WORD-base.json.gz": "08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0", + "WORD-extra.json.gz": "d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299", +} +LEMMA = ( + "On both frozen PR3945 words, the frame-(45,) consumer columns of " + "helpers 600 and 601 are neither equal nor opposite." +) + + +def require(ok, why): + if not ok: + raise SystemExit(why) + + +def load_word(name): + raw = (PACKAGE / "frozen" / name).read_bytes() + require(hashlib.sha256(raw).hexdigest() == HASHES[name], "word hash changed: " + name) + return json.loads(gzip.decompress(raw)) + + +def consumer_adds(word, helper): + found = [] + for section, rows in word.items(): + if not isinstance(rows, list): + continue + for index, row in enumerate(rows): + if not isinstance(row, list) or not row or row[0] != "add": + continue + require(len(row) >= 6, "short add") + if row[2] == helper: + require(isinstance(row[3], int), "non-integer coefficient") + require(isinstance(row[5], list), "frame is not a list") + found.append((section, index, row[1], row[3], tuple(row[5]))) + return found + + +def frame_column(adds, frame): + column = {} + for _section, _index, destination, coefficient, row_frame in adds: + if row_frame == frame: + column[destination] = column.get(destination, 0) + coefficient + require(set(column) == set(ORDER), "frame-(45,) consumers changed") + return tuple(column[destination] for destination in ORDER) + + +def single_sign(left, right): + ratios = [] + for x, y in zip(left, right): + require(x != 0 and y != 0 and abs(x) == abs(y), "column is not a sign pattern") + ratios.append(y // x) + return len(set(ratios)) == 1 + + +def main(): + require(LEMMA in (PACKAGE / "README.md").read_text(encoding="utf-8"), "README dropped the lemma") + columns = [] + for name in HASHES: + word = load_word(name) + one = {} + for helper in HELPERS: + adds = consumer_adds(word, helper) + require(len(adds) == 7, "expected 7 consumer adds for " + str(helper)) + column = frame_column(adds, FRAME) + require(column == SIGNS[helper], "frame column changed for " + str(helper)) + one[helper] = column + columns.append(one) + require(columns[0] == columns[1], "the two words disagree on these columns") + require(not single_sign(SIGNS[600], SIGNS[601]), "600 and 601 unexpectedly match") + for left in HELPERS: + for right in HELPERS: + if left < right: + require(not single_sign(SIGNS[left], SIGNS[right]), "pair unexpectedly matches") + flipped = (1, 1, 1, -1) + # Consumers 123 and 202 are the disagreements. Flipping both makes 601 equal 600. + repaired = (-1, 1, 1, -1) + require(repaired == SIGNS[600] and single_sign(SIGNS[600], repaired), "sign-flip control failed") + require(not single_sign(SIGNS[600], flipped), "partial flip must stay unmatched") + print("PASS_STAGED544_HELPER600_SIGN_COLUMNS") + + +if __name__ == "__main__": + main() diff --git a/research/partial-helper-capture/source4076/NOTICE.md b/research/partial-helper-capture/source4076/NOTICE.md new file mode 100644 index 0000000000..9ccffcfb7d --- /dev/null +++ b/research/partial-helper-capture/source4076/NOTICE.md @@ -0,0 +1,33 @@ +# Attribution and scope + +New work: the three staged entries (helpers 608, 609, 600) on PR3945's words, their literal records and generalized +applier/review, the class-level Hall integer selection and per-width interval transports for the literal T360 fill, +the adapted owner/frame/root checkers and the admission integration. Prepared by Rohan Arun with Anthropic Claude +assistance. Apache-2.0. AI assistance is not independent human review. + +Retain the following predecessor credit and every native/vendor notice: + +- Dugongue (with substantial OpenAI Codex assistance), PR3945: terminal-width5 words (our source words, byte for byte in + `inputs/OLD-*`), literal owner fill (`owner/inputs/PR3945-FILL.json.gz`), owner walk, independent GF(2) frame walker, + rational root enclosures, native runner closure and the admission reconstruction/adaptation that `admission/` extends. +- dataisfire, PR3734: the actual staged544 supplier, retained full source closure and `stage544_applier`, which + `recipe/staged_entries_applier.py` generalizes. zxv, PR3682: staged pair and the inherited comparison claim. Ross + Richardson, PR3605: staged entrance, literal cleanup (`vendor/staged_pair.py`, byte for byte) and residual checks. +- Erwan Secousses / ChaloupeMusic: PR3949 staged-entry census and assembler (the general staged entry used here, + extended to releases into any register); PR3815 attained T360 clock and owner placement, with retained PR3638 lineage. +- Marius-Paul Dumitrean: exact frame solver `research/rank7-skip-restore-optimum/frames_exact.py`, used to write the + optimal frames. +- Sagar Thakrar, PR3687: `audit_core.py` (byte for byte), crediting Arham Tahir's coupled-carrier audit; roger-sato, + PR3693: whole-word audit adapter `audit_verify.py` (byte for byte). +- hexapode, PR3802 and PR3875; Jeremy Kothe (frame/preload machinery, PR2833 native rewrite); Cinna Davis + (@1337isnot1337), PR2226 native exact Clifford/operator machinery; icekylinx, PR514/433; Tekalign (@tekuuu) sparse + native acceleration with its retained notices; DreamingOfClouds with Claude Opus 5.5 (wrapper/outer machinery); + chafreaky, PR458; and all retained provider, owner, native, admission and outer contributors. +- Independent audits of PR3945 read before building on it: #3969, #3987, #3994. Related staged544 work compared: + #3886/#3941/#3942/#3957/#3964/#3970 (retiming obstructions), #3988 (terminal-only barrier), #3998/#4019 (A2 + contractions, unchanged histogram), #4045/#4061 (helper 600/601 consumer structure; no capture applies), #4016, + #4017. None of them stages these helpers or changes this fill. + +The OR-tools and HiGHS solvers are used only to find the moves (`owner/build/`). Every checked artifact is literal data +verified by standard-library code. No broad mathematical novelty, unconditional all-size multiplication bound, +selected-frontier change, Lean/kernel certification or independent human approval is claimed. diff --git a/research/partial-helper-capture/source4076/vendor/audit_core.py b/research/partial-helper-capture/source4076/vendor/audit_core.py new file mode 100644 index 0000000000..8b5e1d5f2a --- /dev/null +++ b/research/partial-helper-capture/source4076/vendor/audit_core.py @@ -0,0 +1,480 @@ +"""Independent exact semantics and binary-frame bill for the BORROW-WORD format. + +Standard library only. Nothing is imported from the audited authors' code +(PR3133/PR3605 producers, cleanup generator, evaluator or frame solver); the word +format and its semantic contract were read from those pinned sources and are +credited there. The frame-bill and free-word structure (point-set spans, warp +frame and lifted-frame checks, target levels keyed by register, dual symbol +naming) re-implements, without importing, Arham Tahir's +research/coupled-carrier-independent-audit/verify.py (Apache-2.0) and shares its +reading of the contract, so this module is not independent of that audit. + +Sagar Thakrar (thakrarsagar), with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q + +V, N, H = 112, 704, 9 # sources 0..111, targets 112..223, helpers 224..703 +DUAL = 10 ** 6 # offset naming the independent dual symbols D_k = K_k^(-T) + + +class AuditFailure(Exception): + """Explicit failure; never disabled by python -O.""" + + +def need(ok, *why): + if not ok: + raise AuditFailure(' '.join(map(str, why))) + + +def is_target(r): + return V <= r < 2 * V + + +def touched(g): + return g[1:3] if g[0] == 'add' else g[1:2] + + +# ---------------------------------------------------------------------------- +# Binary frames: a subspace of F_2^9 is stored as a 512-bit point-set mask +# (bit x set iff x lies in the subspace). Containment is mask inclusion. +# ---------------------------------------------------------------------------- +_SPAN = {} + + +def span(vectors): + key = tuple(vectors) + mask = _SPAN.get(key) + if mask is None: + points = {0} + for u in key: + need(type(u) is int and 0 <= u < 512, 'frame vector out of range', u) + if u not in points: + points |= {p ^ u for p in points} + mask = sum(1 << p for p in points) + _SPAN[key] = mask + return mask + + +def points(mask): + return [x for x in range(512) if mask >> x & 1] + + +def dim(mask): + size = bin(mask).count('1') + need(size and size & (size - 1) == 0, 'not a subspace point set') + return size.bit_length() - 1 + + +FULL = (1 << 512) - 1 +ZERO = 1 + + +def hyperplane(port): + return sum(1 << x for x in range(512) if bin(x & port).count('1') % 2 == 0) + + +def warp_images(columns): + """Images of all 512 vectors under the F_2-linear map with columns G e_i.""" + need(len(columns) == H and all(type(c) is int and 0 <= c < 512 for c in columns), 'warp columns') + images = [0] * 512 + for x in range(1, 512): + low = x & -x + images[x] = images[x ^ low] ^ columns[low.bit_length() - 1] + need(len(set(images)) == 512, 'singular warp') + return images + + +def image_mask(images, mask): + return sum(1 << images[x] for x in points(mask)) + + +def lagrangian_action_ok(images, U, E): + """K_G(x,z)=(Gx, Gx+G^{-T}(x+z)) is symplectic and maps L_U to L_E, L_0 and L_FULL to themselves. + + L_U={(x,x+p): x in U, p in U^perp}. This is the binary frame action only; it + is not a Clifford phase or Gaussian-product certificate. For invertible G with + G(U)=E it is implied by the frame-map check ( = ), so it is a + consistency check of the implementation, not extra evidence. + """ + inverse = [0] * 512 + for x, y in enumerate(images): + inverse[y] = x + # G^{-T} z: bit j of the result is . + git = lambda z: sum((bin(inverse[1 << j] & z).count('1') & 1) << j for j in range(H)) + lift = lambda x, z: (images[x], images[x] ^ git(x ^ z)) + pair = lambda a, b: (bin(a[0] & b[1]).count('1') + bin(a[1] & b[0]).count('1')) & 1 + basis = [(1 << i, 0) for i in range(H)] + [(0, 1 << i) for i in range(H)] + lifted = [lift(*b) for b in basis] + if any(pair(lifted[i], lifted[j]) != pair(basis[i], basis[j]) for i in range(18) for j in range(i + 1, 18)): + return False + + def frame(mask): + us = points(mask) + perp = [p for p in range(512) if all(bin(p & u).count('1') % 2 == 0 for u in us)] + return {(u, u ^ p) for u in us for p in perp} + return all({lift(*pt) for pt in frame(a)} == frame(b) for a, b in ((ZERO, ZERO), (FULL, FULL), (U, E))) + + +# ---------------------------------------------------------------------------- +# Chronological binary-frame bill (BORROW-WORD contract) +# ---------------------------------------------------------------------------- +def frame_bill(w, lagrangian=False): + rep = w['report'] + need((rep['v'], 2 * rep['v'] + rep['R'], rep['h']) == (V, N, H), 'word geometry') + removed = set(w['removed']) + need(len(removed) == len(w['removed']) and all(2 * V <= r < N for r in removed), 'removed helpers') + live = [r for r in range(N) if r not in removed] + liveset = set(live) + B, warps = w['B'], w['warps'] + for k, (pos, lender, cols, U, E) in enumerate(warps, 1): + need(0 <= pos <= len(B), 'warp position', k) + need(lender in liveset and not is_target(lender), 'warp lender', k) + images = warp_images(cols) + su, se = span(U), span(E) + need(dim(su) == len(U) == len(E) == dim(se), 'warp frame bases', k) + need(image_mask(images, su) == se, 'warp does not map its frame', k) + if lagrangian: + need(lagrangian_action_ok(images, su, se), 'lifted frame action', k) + for name in ('A', 'B', 'restore'): + for g in w[name]: + if g[0] != 'warp': + need(all(r in liveset for r in touched(g)), 'removed/out-of-range register', name, g) + if g[0] == 'add' and not is_target(g[1]): + need(not is_target(g[2]), 'non-target reads a target', name, g) + need(all(g[-1] is None and is_target(g[1]) and g[0] == 'add' for g in w['cut']), 'cut gates') + need(all(g[-1] == [] and is_target(g[1]) for g in w['precondition'] + w['compensation']), 'zero-frame wrapper writes') + need(all(not is_target(g[1]) for g in w['restore']), 'restore writes a target') + + ports = w['ports'] + start, end = {}, {} + for r in live: + if r < V: + start[r], end[r] = span((ports[r],)), FULL + elif r < 2 * V: + start[r], end[r] = ZERO, hyperplane(ports[r - V]) + else: + start[r], end[r] = ZERO, FULL + for q, U in w['start_extra'].items(): + need(int(q) in liveset and int(q) >= 2 * V, 'entrance names a live helper', q) + start[int(q)] = span(U) + for q, U in w['helper_final'].items(): + need(int(q) in liveset and int(q) >= 2 * V, 'terminal names a live helper', q) + end[int(q)] = span(U) + + current, bill, chain = dict(start), Counter(), {} + + def climb(r, mask, where): + need(current[r] & ~mask == 0, 'frame containment fails', where, r) + d = dim(mask) - dim(current[r]) + if d: + bill[d] += 1 + chain.setdefault(r, []).append((where, d, mask)) + current[r] = mask + + npre = w['prelude_events'] + for i, g in enumerate(w['A']): + if g[0] == 'warp': + need(i < npre and len(g) == 5, 'warp outside the prelude', i) + _, r, op, fr, to = g + need(op != 0 and abs(op) <= len(warps) and warps[abs(op) - 1][1] == r, 'prelude warp lender', i) + images = warp_images(warps[abs(op) - 1][2]) + if op < 0: + inverse = [0] * 512 + for x, y in enumerate(images): + inverse[y] = x + images = inverse + need(image_mask(images, span(fr)) == span(to), 'prelude warp frame action', i) + need(current[r] == span(fr), 'prelude warp entry frame', i, r) + current[r] = span(to) + chain.setdefault(r, []).append((('A', i), 'warp', span(to))) + else: + if i < npre: + need(is_target(g[1]), 'prelude scalar writes a non-target', i) + for r in touched(g): + climb(r, span(g[-1]), ('A', i)) + levels = {V + int(t): span(U) for t, U in w['target_levels'].items()} + need(all(current[t] == levels.get(t, ZERO) for t in range(V, 2 * V)), 'target cut levels') + for q, U in zip(w['centers'], w['center_frames']): + U = span(U) + need(current[q] == U, 'centre entry frame', q) + served = {levels.get(g[1], ZERO) for g in w['cut'] if g[2] == q} + for T in sorted(served, key=lambda m: -dim(m)): + need(T & ~U == 0, 'centre descent not nested', q) + d = dim(U) - dim(T) + if d: + bill[d] += 1 + chain.setdefault(q, []).append((('centre',), d, T)) + U = T + at = {} + for k, rec in enumerate(warps, 1): + at.setdefault(rec[0], []).append(k) + for p in range(len(B) + 1): + for k in at.get(p, ()): + _, lender, _, U, E = warps[k - 1] + need(current[lender] == span(U), 'native warp entry frame', k, lender) + current[lender] = span(E) + chain.setdefault(lender, []).append((('warp', k), 'warp', span(E))) + if p < len(B): + for r in touched(B[p]): + climb(r, span(B[p][-1]), ('B', p)) + for i, g in enumerate(w['restore']): + for r in touched(g): + climb(r, span(g[-1]), ('restore', i)) + for r in live: + climb(r, end[r], ('end',)) + restored = set(map(int, w['helper_final'])) + need(all(end[r] == FULL for r in live if r not in restored and not is_target(r)), 'a FULL-cleanup register ends low') + widths = Counter(dim(end[r]) - dim(start[r]) for r in live if r >= 2 * V) + return dict(sorted(bill.items())), dict(sorted(widths.items())), chain, start, end + + +def hygiene(w): + """Inherited structural contract: dyadic scalars, power-of-two scales, wrapper and correction access.""" + entering = set(map(int, w['start_extra'])) + restored = set(map(int, w['helper_final'])) + live = set(range(N)) - set(w['removed']) + for name in ('precondition', 'compensation', 'A', 'cut', 'B', 'restore', 'cleanup'): + for g in w[name]: + if g[0] == 'warp': + continue + q = Q(g[3], g[4]) if g[0] == 'add' else Q(g[2], g[3]) + need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'non-dyadic scalar', name, g) + if g[0] == 'scale': + need(abs(q.numerator) & (abs(q.numerator) - 1) == 0, 'non power-of-two scale', name, g) + for g in w['precondition'] + w['compensation']: + need(not any(r in entering | restored for r in touched(g)), 'wrapper touches an entering or restored helper', g) + for c in w['initial_corrections']: + word = c['operator_word'] + need(is_target(c['target']) and c['source'] in live and c['source'] >= 2 * V + and c['source'] not in entering, 'correction access', c) + need(word and all(w['warps'][abs(o) - 1][1] == c['source'] for o in word), 'correction operator lender', c) + q = Q(c['coefficient']) + need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'correction coefficient', c) + return True + + +# ---------------------------------------------------------------------------- +# Literal inverse cleanup, derived from the contract +# ---------------------------------------------------------------------------- +def ordinary_forward(w): + """Chronological non-wrapper actions whose inverse forms cleanup.""" + out = [g for g in w['A'][w['prelude_events']:]] + at = {} + for k, rec in enumerate(w['warps'], 1): + at.setdefault(rec[0], []).append(['warp', rec[1], k]) + for p in range(len(w['B']) + 1): + out += at.get(p, []) + if p < len(w['B']): + out.append(w['B'][p]) + return out + list(w['restore']) + + +def derive_cleanup(w): + restored = set(map(int, w['helper_final'])) + buf = lambda r: r + N if r in restored else r + full = [256, 128, 64, 32, 16, 8, 4, 2, 1] + out = [] + for g in reversed(ordinary_forward(w)): + if g[0] == 'warp': + out.append(['warp', buf(g[1]), -g[2], full]) + elif is_target(g[1]): + continue + elif g[0] == 'add': + out.append(['add', buf(g[1]), buf(g[2]), -g[3], g[4], full]) + else: + need(g[0] == 'scale', 'unknown primitive', g) + out.append(['scale', buf(g[1]), g[3], g[2], full]) + return out + + +def same_cleanup(a, b): + norm = lambda c: [(g[:-1], span(g[-1])) for g in c] + return len(a) == len(b) and norm(a) == norm(b) + + +# ---------------------------------------------------------------------------- +# Exact free-operator semantics. A value is a dict {(input, word): Fraction}; +# word is a reduced tuple of signed operator ids (leftmost = applied last). +# ---------------------------------------------------------------------------- +def program(w, cleanup=None): + """Literal executed sequence: corrections, wrapper, A, cut, B+warps, restore | cleanup.""" + items = [('corr', c['target'], c['source'], tuple(c['operator_word']), Q(c['coefficient'])) + for c in w['initial_corrections']] + items += w['precondition'] + w['compensation'] + w['A'] + w['cut'] + at = {} + for k, rec in enumerate(w['warps'], 1): + at.setdefault(rec[0], []).append(['warp', rec[1], k]) + for p in range(len(w['B']) + 1): + items += at.get(p, []) + if p < len(w['B']): + items.append(w['B'][p]) + items += w['restore'] + return items, list(w['cleanup'] if cleanup is None else cleanup) + + +def dual_op(op): + return (1 if op > 0 else -1) * (abs(op) + DUAL) + + +def _left(op, word): + return word[1:] if word and word[0] == -op else (op,) + word + + +def _right(word, op): + return word[:-1] if word and word[-1] == -op else word + (op,) + + +def _axpy(dst, src, q): + for key, x in src.items(): + y = dst.get(key, 0) + q * x + if y: + dst[key] = y + else: + dst.pop(key, None) + + +def forward_rows(w, cleanup=None, dual=False, symbolic_buffers=True, snapshot=None): + """Schrodinger pass: every register's value as a combination of initial inputs. + + Live inputs are independent symbols. Private buffers are independent symbols + when symbolic_buffers is set (dirty), otherwise zero. The optional snapshot + callback sees the rows at the cleanup boundary. + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + rows = {r: {(r, ()): Q(1)} for r in live} + for c in restored: + rows[c + N] = {(c + N, ()): Q(1)} if symbolic_buffers else {} + prefix, tail = program(w, cleanup) + + def apply(g): + kind = g[0] + if kind == 'add': + t, s, q = g[1], g[2], Q(g[3], g[4]) + need(t != s and q, 'add gate', g) + if dual: + t, s, q = s, t, -q + _axpy(rows[t], rows[s], q) + elif kind == 'scale': + q = Q(g[2], g[3]) + need(q != 0, 'zero scale', g) + if dual: + q = 1 / q + rows[g[1]] = {k: q * x for k, x in rows[g[1]].items()} + elif kind == 'warp': + op = dual_op(g[2]) if dual else g[2] + rows[g[1]] = {(var, _left(op, word)): x for (var, word), x in rows[g[1]].items()} + elif kind == 'corr': + _, t, s, word, c = g + if dual: + src, ops, dst, c = rows[t], [-dual_op(o) for o in word], s, -c + else: + src, ops, dst = rows[s], list(reversed(word)), t + moved = {} + for (var, wd), x in src.items(): + for o in ops: + wd = _left(o, wd) + moved[var, wd] = x + _axpy(rows[dst], moved, c) + else: + raise AuditFailure('unknown primitive ' + repr(g)) + + for g in prefix: + apply(g) + if snapshot is not None: + snapshot(rows) + for g in tail: + apply(g) + return rows + + +def reverse_columns(w, cleanup=None, upto_cleanup=False): + """Heisenberg pull-back: process the forward program backwards. + + cols[s] = {(output, word): coefficient}: the final output register 'output' + contains coefficient*word*x_s. Words grow on the right. Every live input and + every private buffer is an independent symbol. + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + regs = live + [c + N for c in restored] + cols = {r: {(r, ()): Q(1)} for r in regs} + prefix, tail = program(w, cleanup) + seq = prefix if upto_cleanup else prefix + tail + for g in reversed(seq): + kind = g[0] + if kind == 'add': + t, s, q = g[1], g[2], Q(g[3], g[4]) + need(t != s and q, 'add gate', g) + _axpy(cols[s], cols[t], q) + elif kind == 'scale': + q = Q(g[2], g[3]) + need(q != 0, 'zero scale', g) + cols[g[1]] = {k: q * x for k, x in cols[g[1]].items()} + elif kind == 'warp': + op = g[2] + cols[g[1]] = {(out, _right(word, op)): x for (out, word), x in cols[g[1]].items()} + elif kind == 'corr': + _, t, s, word, c = g + moved = {} + for (out, wd), x in cols[t].items(): + for o in word: + wd = _right(wd, o) + moved[out, wd] = x + _axpy(cols[s], moved, c) + else: + raise AuditFailure('unknown primitive ' + repr(g)) + return cols + + +def transpose(cols): + rows = {} + for s, col in cols.items(): + for (r, word), x in col.items(): + rows.setdefault(r, {})[s, word] = x + return rows + + +def endpoint_defects(w, rows, dual=False): + """Compare final rows with the contract on the zero-buffer (live-input) domain. + + Returns (bad live registers, dirty buffers, buffer->live leaks, buffer self-map identity). + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + bad = [] + for r in live: + expect = {(r, ()): Q(1)} + if dual and r < V: + expect[r + V, ()] = Q(-1) + if not dual and is_target(r): + expect[r - V, ()] = Q(1) + got = {k: x for k, x in rows.get(r, {}).items() if k[0] < N} + if got != expect: + bad.append(r) + dirty = [c for c in restored if any(k[0] < N for k in rows.get(c + N, {}))] + leaks = sorted({r for r in live for k in rows.get(r, {}) if k[0] >= N}) + buffer_identity = all({k: x for k, x in rows.get(c + N, {}).items() if k[0] >= N} == {(c + N, ()): Q(1)} + for c in restored) + return bad, dirty, leaks, buffer_identity + + +def boundary_defects(w, rows): + """Contract at the cleanup boundary (forward): targets sheared, restored helpers clean and isolated.""" + restored = set(map(int, w['helper_final'])) + out = [] + for t in range(V, 2 * V): + if {k: x for k, x in rows[t].items() if k[0] < N} != {(t, ()): Q(1), (t - V, ()): Q(1)}: + out.append(('target', t)) + for c in restored: + if rows[c] != {(c, ()): Q(1)}: + out.append(('restored', c)) + for r, row in rows.items(): + if r < N and r not in restored and any(k[0] in restored for k in row): + out.append(('restored input read', r)) + return out