diff --git a/research/p104-rank8-retimed-split/DISCOVERY.json b/research/p104-rank8-retimed-split/DISCOVERY.json new file mode 100644 index 0000000000..faeb14aac7 --- /dev/null +++ b/research/p104-rank8-retimed-split/DISCOVERY.json @@ -0,0 +1,26 @@ +{ + "initial": { + "source_canonical_sha256": "10b24ef20650bce0423c66abf5bd43a837e6d5dbe50c9ac973f17eae295ad62b", + "script": "inputs/pr7105.tar:research/p104-causal-retimed-step/discover.py", + "boundary_group": [ + 3, + 127 + ], + "screen_kappa": "0.00363206219", + "result": "INITIAL-SCREEN-HITS.json", + "log": "INITIAL-SCREEN-LOG.txt", + "scope": "Floating filter plus exact basis pairs; finite one-role retiming screen only, not an optimality certificate." + }, + "rank8": { + "script": "discover.py", + "boundary_group": [ + 3, + 245 + ], + "screen_kappa": "0.00363216151", + "result": "SCREEN-HITS.json", + "log": "SCREEN-LOG.txt", + "chosen_hit": 0, + "pivot_override": 1468 + } +} diff --git a/research/p104-rank8-retimed-split/ENVIRONMENT.json b/research/p104-rank8-retimed-split/ENVIRONMENT.json new file mode 100644 index 0000000000..11dd3ab03f --- /dev/null +++ b/research/p104-rank8-retimed-split/ENVIRONMENT.json @@ -0,0 +1,18 @@ +{ + "python": "3.14.7 (main, Aug 5 2026, 10:29:49) [Clang 21.0.0 (clang-2100.1.1.101)]", + "executable": "/opt/homebrew/opt/python@3.14/bin/python3.14", + "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "machine": "arm64", + "recorded_at": "2026-11-10T14:15:46.848669+00:00", + "command": [ + "python3", + "-I", + "-B", + "research/p104-rank8-retimed-split/verify.py" + ], + "stdout_sha256": "a5e2c209121dd66d1732facd3c33a31771069c8c480175872168b391e22f6c62", + "status": "PASS_P104_RANK8_RETIMED_SPLIT", + "registered_python": "3.12", + "registered_python_local": "unavailable", + "source_archive_git_members_checked": 24 +} diff --git a/research/p104-rank8-retimed-split/INITIAL-SCREEN-HITS.json b/research/p104-rank8-retimed-split/INITIAL-SCREEN-HITS.json new file mode 100644 index 0000000000..fe51488c70 --- /dev/null +++ b/research/p104-rank8-retimed-split/INITIAL-SCREEN-HITS.json @@ -0,0 +1 @@ +[] diff --git a/research/p104-rank8-retimed-split/INITIAL-SCREEN-LOG.txt b/research/p104-rank8-retimed-split/INITIAL-SCREEN-LOG.txt new file mode 100644 index 0000000000..1b20d0fb61 --- /dev/null +++ b/research/p104-rank8-retimed-split/INITIAL-SCREEN-LOG.txt @@ -0,0 +1,33 @@ +windows 17980 +forward 0 systems 0 saved 0 sec 0.0 +forward 5000 systems 0 saved 0 sec 0.53 +forward 10000 systems 0 saved 0 sec 1.14 +forward 15000 systems 0 saved 0 sec 1.67 +forward 20000 systems 12 saved 0 sec 1.98 +forward 25000 systems 72 saved 13 sec 2.15 +forward 30000 systems 4109 saved 634 sec 3.22 +forward 35000 systems 13439 saved 3833 sec 11.18 +forward 40000 systems 25855 saved 7065 sec 21.04 +forward 45000 systems 35570 saved 9130 sec 48.11 +forward 50000 systems 37185 saved 9744 sec 50.16 +forward 55000 systems 37342 saved 9830 sec 50.58 +forward 60000 systems 37382 saved 9849 sec 50.95 +forward 65000 systems 37382 saved 9849 sec 51.74 +forward 70000 systems 37382 saved 9849 sec 52.29 +prefix done 37382 saved 9849 sec 52.34245204925537 +reverse 70000 pairs 0 hits 0 sec 52.35 +reverse 65000 pairs 0 hits 0 sec 52.41 +reverse 60000 pairs 0 hits 0 sec 52.57 +reverse 55000 pairs 0 hits 0 sec 52.81 +reverse 50000 pairs 0 hits 0 sec 53.34 +reverse 45000 pairs 160 hits 0 sec 58.29 +reverse 40000 pairs 38947 hits 0 sec 122.78 +reverse 35000 pairs 41156 hits 0 sec 132.97 +reverse 30000 pairs 43314 hits 0 sec 152.14 +reverse 25000 pairs 43344 hits 0 sec 155.43 +reverse 20000 pairs 43344 hits 0 sec 156.57 +reverse 15000 pairs 43344 hits 0 sec 157.41 +reverse 10000 pairs 43344 hits 0 sec 157.92 +reverse 5000 pairs 43344 hits 0 sec 158.06 +reverse 0 pairs 43344 hits 0 sec 158.1 +paired 43344 hits 0 seconds 158.10312795639038 diff --git a/research/p104-rank8-retimed-split/INPUTS.json b/research/p104-rank8-retimed-split/INPUTS.json new file mode 100644 index 0000000000..dcd7eab37e --- /dev/null +++ b/research/p104-rank8-retimed-split/INPUTS.json @@ -0,0 +1,152 @@ +{ + "source_pr": 7105, + "source_head": "92b09a2bd2a8f6f2e0fb502068c1259350c2a8c8", + "source_canonical_sha256": "10b24ef20650bce0423c66abf5bd43a837e6d5dbe50c9ac973f17eae295ad62b", + "archive_sha256": "aad77bad6aa1b8a1518ddff44c8bef8ca93ebaaf6d25bed5ac4acf7fa9dec317", + "files": [ + { + "path": "research/p104-causal-retimed-step/ENVIRONMENT.json", + "size": 753, + "sha256": "a5dead5b6e45a5ab2c19c25e7af535ed9dd57df3308b86c11f55e665ffd1f0b2", + "git_blob": "13e51eb499ff6eec2fcef8a87154874625c21032" + }, + { + "path": "research/p104-causal-retimed-step/INPUTS.json", + "size": 17505, + "sha256": "a654c5959d01f8c991dfe38e2d1249fa20af919956a0903e8311199c0f86fb4a", + "git_blob": "504f4e425b652d8c84e90aa759ee66df69f65ce7" + }, + { + "path": "research/p104-causal-retimed-step/LICENSE", + "size": 11357, + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64" + }, + { + "path": "research/p104-causal-retimed-step/NOTICE", + "size": 692, + "sha256": "57ea05bb8a8d5474012e3d9d287a020b1f91366aa943532b4d7033b0a0abef50", + "git_blob": "b2fe2f69bed395136add0c5a5cd6c62c664896f7" + }, + { + "path": "research/p104-causal-retimed-step/README.md", + "size": 9250, + "sha256": "243a315262c401913c7e0230b157e612197fe08b1c5f7f1cbd1f2cc1a882c96b", + "git_blob": "dcec9468600ac0678af66deed64578c69247f201" + }, + { + "path": "research/p104-causal-retimed-step/REPLAY.txt", + "size": 1160, + "sha256": "5548b85bfc18ea37528cd3fb2688dde3772330d6cf8b9401d893a33c7292f7d7", + "git_blob": "07384c7ce5ba31f839b560d30f8261a16bbc72a5" + }, + { + "path": "research/p104-causal-retimed-step/RESULT.json", + "size": 26675, + "sha256": "9c1f15dc5f2ddde9c42233fa22fafd83b2b2ff13ae3ec177ce3c4d8ad6ab139e", + "git_blob": "a1ba81ab2d8dfadde904c786721447a29b0c0d08" + }, + { + "path": "research/p104-causal-retimed-step/ROUND1-HITS.json", + "size": 2025, + "sha256": "fe64b549374230ac70c834dc9cd1cdfd9ab30c2d4223fb5f6738d638b8435a33", + "git_blob": "f778973dee4debf4d52368e14cfd334f226c3561" + }, + { + "path": "research/p104-causal-retimed-step/ROUND1-LOG.txt", + "size": 2105, + "sha256": "a688476058304d57488084d1b8235bc68841c942852c2175b0278b50efe55031", + "git_blob": "c4b68ec1cebcc50c3530fcf57124eb036130568f" + }, + { + "path": "research/p104-causal-retimed-step/SCREEN-HITS.json", + "size": 2022, + "sha256": "2a8982e3034b18d985cc29f8e8a4c607177a71e021ca31792c7c37018d1eac8f", + "git_blob": "5f88aaf1128debfb83caf684de4cf57ad03c1a64" + }, + { + "path": "research/p104-causal-retimed-step/SCREEN-LOG.txt", + "size": 2272, + "sha256": "0b4d37dc31454418eb04fd994b47401e3b0825316b6bd324bfddc650771408b0", + "git_blob": "c26ca2cade2a58cb9ce51616ecd43715fe9d467a" + }, + { + "path": "research/p104-causal-retimed-step/SOURCES.json", + "size": 584, + "sha256": "007167ec14efa96e51840bb49f75c61e05fbfebb9e8c9a33f68d94e3dc5cacbf", + "git_blob": "b06c2f774eb6010ed89a251aa4313c970e87b3a7" + }, + { + "path": "research/p104-causal-retimed-step/TASK.json", + "size": 9892, + "sha256": "2277782105ea1a3c27180b1c3704fe75b105d5d06f86f372e2b590cf68271de3", + "git_blob": "e908c586a83b9f3753752f5e60add5bdfba9e42f" + }, + { + "path": "research/p104-causal-retimed-step/VALIDATION.md", + "size": 1995, + "sha256": "343fcafcfdb14afcccad8fc2c5576220cf6d2f3fd6efc8edc8d6dc2c71077d87", + "git_blob": "a769924740ddb38e13050029b7aa5d7b7784043f" + }, + { + "path": "research/p104-causal-retimed-step/VERIFY.json", + "size": 664, + "sha256": "5d726a2ab788428741b57356f29c68435b49bf607c271b45b8d6d607efd99c7a", + "git_blob": "f1330ca857a907ebbed0ec2bfffa277a07a223d2" + }, + { + "path": "research/p104-causal-retimed-step/WITNESS.json", + "size": 515, + "sha256": "1b7bf9719c2b780322876c0b2d7ab94b864008ce083fd5944f82ff54a24e44c8", + "git_blob": "a7359edd589e08a3a8a6b90ebd28cddc3d6259aa" + }, + { + "path": "research/p104-causal-retimed-step/WORD.json.gz", + "size": 350523, + "sha256": "568419d0eca2c5ff7d2f5fde9be66eca9cde109d3d285a6db3c153a530b9f24f", + "git_blob": "704a49dbf9d637471fd2ed8eb92a469812716c04" + }, + { + "path": "research/p104-causal-retimed-step/construct.py", + "size": 1913, + "sha256": "efe9b2dd791edc986f1c0e3dc84a5fca68a291cca0607212eb2aa9a267c7678b", + "git_blob": "1d816292f3313dfb5c24a3f425f555250c41425a" + }, + { + "path": "research/p104-causal-retimed-step/discover.py", + "size": 7077, + "sha256": "184b46485ea33c1144fae301b2c91ff37a302f74d9fad43b441dcb94b81b47ad", + "git_blob": "0bff0e5ae95742286e0f8032c192ab1168ecc512" + }, + { + "path": "research/p104-causal-retimed-step/inputs/pr7004.tar", + "size": 1976320, + "sha256": "25f3952808ade8642cdd66425d6963fe8639adafef1cab33e213f0736fd68287", + "git_blob": "ba8815bae15fd77efc628cf445f7064acacda5b0" + }, + { + "path": "research/p104-causal-retimed-step/source.py", + "size": 3052, + "sha256": "e33164d1f445bcd203be1fec16c8bbde6db11a7221feeb96bcc894082b1092a9", + "git_blob": "0e405e55702e38fe5c958e954024630fb3d206a0" + }, + { + "path": "research/p104-causal-retimed-step/split.py", + "size": 6020, + "sha256": "809b2fc15db992a93d561220d93684b7f77e766834024e7fe9d6704a4a76e83d", + "git_blob": "3260b2a0a38586d5744a818f4c1474819111ce60" + }, + { + "path": "research/p104-causal-retimed-step/support.py", + "size": 606, + "sha256": "f3e6eeb879480715c5c32c1a390a63c57d26ea1c9a9cbdb89b83ca34260e47f6", + "git_blob": "192cd38d27e4b732981b98730459a041dcfb52e7" + }, + { + "path": "research/p104-causal-retimed-step/verify.py", + "size": 9767, + "sha256": "cc5be16c79f9e73c04eab880eae644c5de51af1dea46427b4aa3b79388588394", + "git_blob": "67c89d2b3abd1bac59c6be6bfd54cd3869e56c68" + } + ] +} diff --git a/research/p104-rank8-retimed-split/LICENSE b/research/p104-rank8-retimed-split/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/p104-rank8-retimed-split/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/p104-rank8-retimed-split/NOTICE b/research/p104-rank8-retimed-split/NOTICE new file mode 100644 index 0000000000..4d6d5abb50 --- /dev/null +++ b/research/p104-rank8-retimed-split/NOTICE @@ -0,0 +1,5 @@ +Prepared for dillona with substantial OpenAI Codex assistance. Apache-2.0. + +Ali Romman supplied the independent-helper split and basis construction. Jerry Chen / CubeJerry supplied counted owned inventories, paid retiming, shared-wire composition, caller and precision engines. DreamingOfClouds supplied the native word chain. ToikY supplied #7003/#7004 MOVE fusion and peer retiming. The archived #7105 package retains these source notices, including credit to Cinna Davis, Pierre-Loic Doulcet, Mason Hale, Jacob Alan Sussman, zxv, thu-nmrc and all retained native/compiler/precision/analytic authors. + +New work: parameterized boundary-group discovery and one exact rank-eight helper split on #7105, with a lower-operation pivot and source-bound full verification. The split mechanism, constructors and imported verification engines retain their predecessor authorship. No independent human or proof-kernel review is claimed. diff --git a/research/p104-rank8-retimed-split/README.md b/research/p104-rank8-retimed-split/README.md new file mode 100644 index 0000000000..e6e18781f9 --- /dev/null +++ b/research/p104-rank8-retimed-split/README.md @@ -0,0 +1,96 @@ +# Conditional κ = 0.00363233825: one rank-eight helper split + +This changes the complete invoice of [#7105](https://github.com/CrocSwap/integer-mult-bounds/pull/7105), raising its conditional claim from **0.00363216151** to **0.00363233825**, a gain of **0.00000017674**. One paid retiming exposes an independent rank-eight helper direction that splits into ranks three and five. The emitted word adds one MOVE and fourteen integer ADDs. The caller and BIT inputs are the exact predecessor bytes. + +This is an author-checked conditional construction, with source-aware reuse of attributed engines. It is not supplier admission, an unconditional multiplication theorem, or a selected-frontier update. + +## Exact source and construction + +The source is #7105 at public head `92b09a2bd2a8f6f2e0fb502068c1259350c2a8c8`, canonical word SHA256 `10b24ef20650bce0423c66abf5bd43a837e6d5dbe50c9ac973f17eae295ad62b`. Canonical main was refreshed at entry and before submission to `f16923d466a6aba912299882e0545564d2ba7bb2`; priority revision 8 and selected #6030 are unchanged. The exact predecessor package, including its source closure and notices, is archived in `inputs/pr7105.tar`. `INPUTS.json` authenticates every member by size, SHA256 and Git blob. The verifier reconstructs #7004, then #7105, before constructing this successor. + +All indices below refer to the source word and are zero-based. Role 533 has no scalar contact in the half-open interval `[37411,39699)`. Its sole event there is `MOVE(533,3,747,false)` at index 38792. Replace it with 3→745→747 at cut 37420, immediately before source event 37420. The spaces strictly nest, with dimensions 0, 3 and 6. This replaces one rank-six payment with two rank-three payments. With chart operator C_f, normalized coordinates C_f^-1 v are unchanged by MOVE. No read or write of role 533 is crossed, so the retiming preserves the normalized scalar operator. + +Let P be the full retimed prefix and S its suffix at the intermediate frame 745. The exact row and column vectors are: + +| Vector | Nonzero coordinates | +|---|---| +| a | e533ᵀ − 2 e1454ᵀ | +| b | e533 + e1468 − e843 | +| c | e533ᵀ + 4 e1251ᵀ + e1468ᵀ − 2 e1454ᵀ | +| d | e1468 | + +The verifier checks `aP=c`, `Sb=d`, and `ab=cd=1` over the rationals, including all other public inputs/outputs and every owned row. Roles 533, 843, 1454 and 1468 are at frame 745 at the cut. The support of c and d belongs entirely to the independent helper group with boundary frames `(3,245)`, of dimensions 0 and 8. The two productive ranks are therefore 3 and 5. + +Apply Ali Romman's helper-split criterion with pivot 1468. The boundary basis G has row 1468 equal to c and sends d to e1468. It consists of three ADDs at frame 3: add roles 533, 1251 and 1454 into 1468 with coefficients 1, 4 and −2. The cut basis J has row 1468 equal to a and sends b to e1468. It consists of four ADDs at frame 745: + +``` +ADD(533,1468,−1), ADD(843,1468,+1), +ADD(1468,533,+1), ADD(1468,1454,−2). +``` + +Emit G^-1 at the input, J at the cut, and J^-1 followed by the complete suffix using new role 1481 wherever pivot 1468 formerly appeared. Emit G at final frame 245 with the same substitution. The old pivot now returns at 745; the new arbitrary helper starts at 745 and finishes at 245. This is fourteen explicit scalar instructions, with no implicit free basis operation. Owned labels shift by one; their logical lifetimes and rise inventory are preserved. + +For completeness, after the input basis, the retained pivot coordinate at the cut is the independent input x1468. Replacing it by fresh input z changes the suffix input along b. Since Sb=d and Gd=e1468, the final boundary basis sends this difference only to the renamed successor output. That output returns z, the retained pivot returns x1468, and all other helper and main outputs remain unchanged. This uses two independent input coordinates; it does not duplicate productive credit from one input. Every correction occurs at one physical chart. The source all-column contract supplies the width lift, while this package checks exact phases and all 512 columns of every affected chart pair. + +The complete emitted word has canonical SHA256 `a3bffcd29d5e7040d91a439d2fecfaa17a3c15a373da03099d44fd9c1261622a`. + +## Complete accounting and fixed-invoice ceiling + +Per LOCAL, the paid delta is `{3:+2,6:−1}` and the target delta is `{3:+1,5:+1,8:−1}`. Across the unchanged eighteen LOCALs, all counts multiply by eighteen. Thus for `0 0. +``` + +Strict concavity proves the inequality: the increment from 3 to 5 exceeds that from 6 to 8. Both rank-three payments are charged; one cancels the rank-three target in this displayed signed difference. This is a changed complete profile, not additional digits of the old root. + +The word has 71,273 events, 1,482 public fields (400 main and 1,082 independent helpers), 51 owned labels, 54 owned lifetimes and peak 43. Its 23 owned rises have total mass 56. Complete rank surplus remains 1,520, and no empty-root credit is used. The conservative ordinary bill is **826,799,424 < 10^9**, including helper boundaries, input conversion and the inherited second LAMBDA charge. + +Two rational interval engines certify the changed raw crossing. The independent enclosure is + +``` +(0.00363233825927247587361768759941604, + 0.00363233825927247587361768759941605). +``` + +The conservative claim is `14529353/4000000000 = 0.00363233825`. Tested price is `0.00363233825007`, compiler gap is `10^-14`, written logarithm power is 2229, and H is `14181100000000000000`. The fixed-invoice headroom above the claim is about `9.27e-12`; its negative derivative bound and exact brackets are in `RESULT.json`. Refining this root alone is not another construction step. The old complete invoice rejects the new claim. + +## Verification and reproduction + +The full verifier checks source reconstruction, exact cut identities, the complete arbitrary-input adjoint, an independently implemented forward integer-grid replay, the formal paired QUERY-only caller, both complete invoices, ordinary costs, two rational price engines, strictification, input lift, compiler and 54+4 outer inequalities. It reuses the attributed common-grid and rounded-envelope engines, checks the E-free paired BIT artifact binding, and runs the source's relaxed native and full width-512 finite physical replays. Five named chart pairs include the two new pairs 745→245 and 745→747; all 512 columns and absolute phases pass. Wrong phase, cut direction, contact window, deleted cut corrections, wrong successor frame, undersized grids and the new claim on the old invoice reject. + +``` +python3 -I -B research/p104-rank8-retimed-split/verify.py +python3.12 -B scripts/research_package.py --package research/p104-rank8-retimed-split +``` + +Expected final line: `PASS_P104_RANK8_RETIMED_SPLIT 14529353/4000000000`. +The standalone scientific command needs no Git or network. Ordinary replay compares every receipt field to `RESULT.json`; `--out UNUSED_PATH` emits a new receipt. Regenerated gzip artifacts are compared by their complete decompressed payload. Optimized mode is deliberately rejected because retained engines use assertions. `VALIDATION.md`, `REPLAY.txt` and `ENVIRONMENT.json` identify the execution evidence and its limits. + +The optional discovery screen is separate from the verifier: + +``` +python3 research/p104-rank8-retimed-split/source.py --output /tmp/source7105.json.gz +python3 research/p104-rank8-retimed-split/discover.py /tmp/source7105.json.gz /tmp/rank8-hits.json 3 245 +``` + +`SCREEN-HITS.json` contains three nominations, not three independent gains. The certificate takes the first with pivot changed from 533 to 1468, reducing the total basis length from ten to seven before inverse copies. Discovery uses floating arithmetic only as a filter; acceptance reconstructs the complete exact candidate. The initial whole-boundary `(3,127)` screen on #7105 found zero hits; its exact script pin, floating threshold and retained log are in `DISCOVERY.json`. That finite failure is not an optimality result. This rank-eight witness does not require claiming that #7105 newly created its entire boundary group. + +## Scope and outstanding obligations + +The five retained framework assumptions remain: `native_all_columns`, `owned_erasure`, `compiler`, `precision_tape`, and `analytic_recovery`. Retain the source's exact odd-scalar complete child returns, owned movement, hosted/per-port and one-field-idle caller, LAMBDA/ordinary tariff and paired BIT contracts. This edit adds only integer ADDs and no owned ascent. A materialized uniform word or complete rounded multiplier is not supplied. + +The new canonical-main [#7000 admission review](https://github.com/CrocSwap/integer-mult-bounds/blob/f16923d466a6aba912299882e0545564d2ba7bb2/docs/research/pr-intake-evidence/pr7000-admission/PROOF-REVIEW.md) repairs BIT working ambient rank to 134 and logarithm power to 617 while preserving the available saving. Our frozen numerical source engines are unchanged and their BIT binding check is not a replay of that supplement or a complete BIT admission proof. That review discharges narrow owned-ascent and LAMBDA clauses for its exact source; it still requires the complete occurrence/interface map, physical upper-cost conversion, storage/root boundary and resulting outer-threshold application. Those outstanding obligations are explicitly retained here. The passing source-unit ordinary bill must not be identified with a literal machine-step count. + +## Credit + +Prepared for dillona with substantial OpenAI Codex assistance; no subagents. New work is this source-bound rank-eight retiming/split composition, parameterized discovery, choice of a shorter basis, and verification package. Apache-2.0. + +Credit Ali Romman for independent-helper basis splitting; Jerry Chen / CubeJerry for counted inventories, paid retiming, shared wires, #7000 composition, paired BIT/caller and precision engines; DreamingOfClouds for #6931/#6936/#6937 and the native chain; ToikY for #7003/#7004; and #7105 for the immediate source and reusable source-bound replay. Retain the original notices and attribution to Cinna Davis, Pierre-Loic Doulcet, Mason Hale, Jacob Alan Sussman, zxv, thu-nmrc and all credited native/compiler/precision/analytic authors. Separate algorithmic implementations here are not independent human or kernel review. + +## Open next questions + +- Can the other two rank-eight nominations compose with this split? Recompute exact capacity on the emitted successor and price the joint corrections; overlapping boundary vectors prevent assuming independence. +- Can the exact source be admitted under the retained framework with an explicit physical upper-cost conversion? Start from the #7000 review's occurrence/interface and corrected BIT geometry requirements; finite replay leaves those supplier obligations open. + +Structured questions and blockers are in `TASK.json`. The canonical [investigation post](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19520521) records the expansion decision, source pins, overlap coverage and final artifact. Existing frozen packages and the selected result remain unchanged. diff --git a/research/p104-rank8-retimed-split/REPLAY.txt b/research/p104-rank8-retimed-split/REPLAY.txt new file mode 100644 index 0000000000..337e7b41ad --- /dev/null +++ b/research/p104-rank8-retimed-split/REPLAY.txt @@ -0,0 +1,19 @@ +PASS source reconstruction, exact split prefix/suffix, complete adjoint and frame law +caller 0 terms 77 +caller 500 terms 1044 +caller 1000 terms 761 +caller 1500 terms 1868 +caller 2000 terms 2524 +caller 2500 terms 384 +caller 3000 terms 151 +PASS complete invoice, ordinary bill, BIT binding, two exact price engines, compiler and 54+4 outer gates +events 71273 public 1482 owned roles 51 paid {1: 4068, 2: 830, 3: 813, 4: 238, 5: 323, 6: 16, 7: 12, 8: 6} owned UP {1: 10, 2: 4, 3: 1, 4: 6, 5: 1, 6: 1} helpers {1: 14, 2: 18, 3: 45, 4: 215, 5: 69, 6: 42, 7: 18, 8: 67, 9: 594} +endpoint bad rows 0 odd certificate S 1125 +PASS_HOST3 decoupled ports 96 hosted ports 8 +gate interpreter agrees with the library on 4 exact state vectors +replayed 71273 events, 2969 chart pairs, 24s +prime 1000000009 seed 11: helper rows bad 0 (of 1082), X rows bad 0, Y rows bad 0, X2 rows bad 0, Y2 rows bad 0 (of 104 ports; 96 with second mains) +tableau on 104 ports: XX!=D 0 YY!=D 0 YX!=Q^-1D 0 XY!=QD 0 | controls matching (must be 0): 0 0 +PASS_PHYSICAL 32s +PASS exact Gaussian columns, prefix precision and physical finite replay +PASS_P104_RANK8_RETIMED_SPLIT 14529353/4000000000 diff --git a/research/p104-rank8-retimed-split/RESULT.json b/research/p104-rank8-retimed-split/RESULT.json new file mode 100644 index 0000000000..55796af836 --- /dev/null +++ b/research/p104-rank8-retimed-split/RESULT.json @@ -0,0 +1,702 @@ +{ + "caller": { + "bad_outputs": [], + "caller_denominator_height_bound": 163, + "caller_mass_bound": "16246698892210214036146399419475929893435/256", + "caller_mass_ceiling_bits": 126, + "max_terms": 2713 + }, + "charts": { + "new_pairs": [ + [ + 745, + 245 + ], + [ + 745, + 747 + ] + ], + "rechecked_pairs": [ + { + "columns": 512, + "pair": [ + 3, + 245 + ], + "rank": 8 + }, + { + "columns": 512, + "pair": [ + 3, + 745 + ], + "rank": 3 + }, + { + "columns": 512, + "pair": [ + 3, + 747 + ], + "rank": 6 + }, + { + "columns": 512, + "pair": [ + 745, + 245 + ], + "rank": 5 + }, + { + "columns": 512, + "pair": [ + 745, + 747 + ], + "rank": 3 + } + ], + "wrong_phase_rejected": true + }, + "controls": { + "intervening_contact": true, + "missing_cut_correction": true, + "missing_successor_correction": true, + "wrong_successor_frame": true, + "wrong_suffix": true + }, + "diagnostic_crossing": "0.00363233825927247587361768759941604531395607912447998029099635792392", + "forward": { + "coefficient_positions": 2350089, + "fractional_bits": 24, + "grid": 1125, + "rows": 1533 + }, + "gain": { + "claim_gain": "8837/50000000000", + "claim_vs_old_raw_upper": "8836726568067376426906177/50000000000000000000000000000000", + "new_margin_at_old_upper": [ + "3670280777134011270258061047974770159066112811681339128970106292711006286793591/50000000000000000000000000000000000000000000000000000000000000000000000000000000", + "734056155426802254051612209594954031813222562336267825794021258542201261554189/10000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "raw_gain_interval": [ + "3534876076744422924514459/20000000000000000000000000000000", + "17674380383722114622572297/100000000000000000000000000000000" + ] + }, + "gate": { + "BIT_margin": "13435174993/100000000000000", + "BIT_pin": "376669/100000000", + "H": "14181100000000000000", + "alpha": [ + 0.9999999999879692, + 0.9999999999879692 + ], + "claim": "14529353/4000000000", + "compiler_gap": "1/100000000000000", + "delta": [ + 0.8772849945367347, + 0.8772849945367347 + ], + "derivative_upper": -408349.77005214995, + "gamma": [ + 0.9497474106778799, + 0.9497474106778799 + ], + "input_lift": { + "derivative_upper_on_required_interval": "-2299831290525933154178526076272396899996972093654613095735772838275432653960006518819/2500000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "interval_kappa_cap": "376669/100000000", + "margins": { + "14529353/4000000000": [ + "123946128526723849291705050075587597806279065843206398338459048598946580769499/100000000000000000000000000000000000000000000000000000000000000000000000000000000", + "15493266065840481161463131259448449725784883230400799792307381074868322596429/12500000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "363233825007/100000000000000": [ + "123946128529010910505576771649459320897610280416766712720299468985201563544413/100000000000000000000000000000000000000000000000000000000000000000000000000000000", + "30986532132252727626394192912364830224402570104191678180074867246300390886589/25000000000000000000000000000000000000000000000000000000000000000000000000000000" + ] + }, + "source_BIT_wide_crude_bound_would_be": "-2299831290525933154178526076272396899996972093654613095735772838275432653960006518819/2500000000000000000000000000000000000000000000000000000000000000000000000000000000000000" + }, + "minimum_log_power": 2228, + "moment_margin_float": { + "181616912963623793680884379971/50000000000000000000000000000000": [ + -1.6424680850767923e-27, + -1.6424680850767923e-27 + ], + "363233825007/100000000000000": [ + 3.821990610260616e-06, + 3.821990610260616e-06 + ], + "363233825927247587361768759941/100000000000000000000000000000000": [ + 2.510751833863616e-27, + 2.510751833863616e-27 + ] + }, + "moment_margins": { + "181616912963623793680884379971/50000000000000000000000000000000": [ + "-82123404253839611808618449033443590209272280965377591/50000000000000000000000000000000000000000000000000000000000000000000000000000000", + "-82123404253839611808618449033443590209272280944413253/50000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "363233825007/100000000000000": [ + "191099530513030832274690180888386298477803417934042357987953921854468387993/50000000000000000000000000000000000000000000000000000000000000000000000000000000", + "191099530513030832274690180888386298477803417934042357987953921854489449423/50000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "363233825927247587361768759941/100000000000000000000000000000000": [ + "125537591693180807395436954729360353952328996918335569/50000000000000000000000000000000000000000000000000000000000000000000000000000000", + "25107518338636161479087390945872070790465799387864467/10000000000000000000000000000000000000000000000000000000000000000000000000000000" + ] + }, + "outer": { + "BIT_just_below_effective_rejected": true, + "functional_count": 4, + "minimum_margin": "1/1000000000000000", + "strict_count": 54 + }, + "raw_bracket": [ + "363233825927247587361768759941/100000000000000000000000000000000", + "181616912963623793680884379971/50000000000000000000000000000000" + ], + "tested": "363233825007/100000000000000", + "written_log_power": 2229 + }, + "grid": { + "dyadic_height": 24, + "maximum_scaled_mass": "1636346757402225/16384", + "odd_divisions": { + "ADD": 4079, + "SCALE": 64 + }, + "odd_grid_lcm": 1125, + "opcodes": { + "ADD": 61196, + "CLEAR": 54, + "COPY": 1, + "INIT": 54, + "MOVE": 6306, + "SCALE": 3662 + }, + "owned_lifetimes": 54, + "owned_peak": 43, + "owned_rise_mass": 56, + "owned_rises": { + "1": 10, + "2": 4, + "3": 1, + "4": 6, + "5": 1, + "6": 1 + }, + "paid": { + "1": 4068, + "2": 830, + "3": 813, + "4": 238, + "5": 323, + "6": 16, + "7": 12, + "8": 6 + } + }, + "independent_raw_bracket": [ + "90808456481811896840442189985401/25000000000000000000000000000000000", + "72646765185449517472353751988321/20000000000000000000000000000000000" + ], + "invoice": { + "P": { + "1": 73640, + "16": 416, + "2": 14940, + "24": 416, + "3": 14634, + "32": 416, + "4": 4284, + "40": 416, + "48": 416, + "5": 5814, + "56": 416, + "6": 288, + "64": 416, + "7": 216, + "8": 812 + }, + "S": 1520, + "T": { + "1": 252, + "145": 208, + "17": 416, + "2": 324, + "25": 416, + "3": 810, + "33": 416, + "4": 3870, + "41": 416, + "49": 416, + "5": 1242, + "57": 416, + "6": 756, + "65": 416, + "7": 324, + "73": 416, + "8": 1206, + "9": 11108 + }, + "empty_root_credits": 0, + "no_E_credit_crossing": "0.0036323382592724758736176875994160453139560791005409957376715654733", + "raw_crossing": "0.0036323382592724758736176875994160453139560791005409957376715654733" + }, + "limitations": [ + "Source-aware attributed engine reuse, not independent human or kernel review.", + "All inherited five assumptions and #7105 inherited exact odd-return, owned-ascent, caller, BIT and physical-tariff contracts remain.", + "No materialized uniform rounded multiplier or selected-frontier change." + ], + "native": { + "bad_inputs": [], + "events": 71273, + "helpers": { + "1": 14, + "2": 18, + "3": 45, + "4": 215, + "5": 69, + "6": 42, + "7": 18, + "8": 67, + "9": 594 + }, + "lifetimes": 54, + "owned_peak": 43, + "paid": { + "1": 4068, + "2": 830, + "3": 813, + "4": 238, + "5": 323, + "6": 16, + "7": 12, + "8": 6 + }, + "public": 1482, + "rises": { + "1": 10, + "2": 4, + "3": 1, + "4": 6, + "5": 1, + "6": 1 + } + }, + "ordinary": { + "caller_items": { + "A": { + "envelope": 124674048, + "field_boundary": 94848, + "idle_routes": 185472000, + "output_routes": 229056000, + "query_routes": 1152000, + "thin": 6144 + }, + "B": { + "envelope": 19893760, + "field_boundary": 7904, + "idle_routes": 20064000, + "output_routes": 19088000, + "query_routes": 96000, + "thin": 512 + } + }, + "caller_total": 599605216, + "conservative_total": 826799424, + "init_clear_allowance": 216, + "lambda_paid_rank1_would_reduce_S_by": 14480, + "lambda_second_charge": 14480000, + "margin_to_billion": 173200576, + "odd_divisions": { + "ADD": 4079, + "SCALE": 64 + }, + "per_input_conversion": 2774304, + "raw_upper": 809545120, + "route_items": { + "first_main_adapter": 416, + "first_main_boundary": 208, + "helper_boundary": 2164, + "moves": 6306, + "owned_lifetime": 216, + "second_main_adapter": 384, + "second_main_boundary": 192 + }, + "routing": 9886000, + "scalar_upper": 1777328 + }, + "physical_checks": [ + "verify_host3_odd.py", + "physical.py" + ], + "precision": { + "common_grid": { + "caller": { + "denominator_height": 163, + "maximum_mass": "16246698892210214036146399419475929893435/256", + "pre_joint_height": 154, + "pre_joint_mass": "758143798823020519902612486795530419693/64" + }, + "context_c": 356, + "context_height": 178, + "context_mass_bits": 161, + "word": { + "coefficient_visits": 14087858, + "dyadic_height": 24, + "mass_witness": [ + 63474, + "stored add" + ], + "maximum_scaled_mass": "1636346757402225/16384", + "numerator_bits": 24, + "odd_scale_lcm": 1125 + } + }, + "helper_census_substitutions": [ + [ + "word[\"public\"] - len(mains) == 1061", + "word[\"public\"] - len(mains) == 1082" + ], + [ + "fresh_arbitrary_helpers=18 * 1061", + "fresh_arbitrary_helpers=18 * 1082" + ] + ], + "method": "attributed source-engine reuse", + "negative_grid_controls": { + "S1125_f23": "integer grid rejection at event 61575: denominator 64", + "S225_f24": "integer grid rejection at event 1121: denominator 250", + "S375_f24": "integer grid rejection at event 36839: denominator 48" + }, + "rounded_envelope": { + "caller": { + "bounds": { + "E_joint_entrance": { + "exact": "326155049787256155157832340134847384764735629531953501631388760516641021999646985360258683049043029091571551527324903978689681205577462992724431/272008309413291564308889600000000000000000", + "strict_power_of_two": 340, + "witness": { + "cut": 2958, + "event": 2958, + "factor": "1", + "kind": "stored", + "register": 39 + } + }, + "Gamma_context": { + "exact": "15259614246461931659309736794620779902271861133313062988612435126509213790586168872604898507585385733765513676582475908282056414302819372804609281/78338393111027970520960204800000000000000000", + "strict_power_of_two": 337, + "witness": { + "cut": 3095, + "factor": "1", + "kind": "public-return", + "register": 75 + } + }, + "M_caller": { + "exact": "1683307283016999532839217702665847040", + "strict_power_of_two": 121, + "witness": { + "cut": 3050, + "event": 3049, + "factor": "1", + "kind": "stored", + "register": 38 + } + }, + "M_context": { + "exact": "41102872446205142735437430546015485583317670960340182874015713769290189707295861749261430023415884041067801515671536703280961749529489018333644385181/816024928239874692926668800000000000000000", + "strict_power_of_two": 355, + "witness": { + "cut": 2959, + "event": 2958, + "factor": "1", + "kind": "stored", + "register": null + } + }, + "M_joint_entrance": { + "exact": "363421601940370671219209686545270656", + "strict_power_of_two": 119, + "witness": { + "cut": 2958, + "event": 2958, + "factor": "1", + "kind": "stored", + "register": 39 + } + }, + "Sigma_caller": { + "exact": "8157752610051527181179756772539507154773741043488805711776639249105573905795360887931494583164222855649110711012240079449883910365199677177007431/1468844870831774447268003840000000000000000", + "strict_power_of_two": 342, + "witness": { + "cut": 3050, + "event": 3049, + "factor": "1", + "kind": "stored", + "register": 38 + } + }, + "Sigma_context": { + "exact": "4721668704341998520596051155693512848854299090511739810410757477583892306530273980423601953984992063088231402858033959015621421769795417052599436025951781630775967452072931877122083703457867604419163974561064193069614521546984632740445481692950348024450294493/28411591829712752729879633148004541902111328635453440000000000000000000000000000000000", + "strict_power_of_two": 576, + "witness": { + "cut": 2959, + "event": 2958, + "factor": "1", + "kind": "stored", + "register": null + } + } + }, + "fresh_arbitrary_helpers": 19476, + "helper_allocation_premise": "distinct (stage, helper) public inputs as in frozen caller proof", + "independent_adjoint": { + "E_joint_entrance": { + "entrance_mass": "363421601940370671219209686545270656", + "joint_coefficient": "59336854494143543914675236360327/2", + "primitive_coefficient": "22622085086540611235550148326673690", + "residual_mass": "326155049787256155157832340134847384764735629531953501631388760516641021999646985360258683049043029091571551527324903978689681205577462992724431/272008309413291564308889600000000000000000" + }, + "Gamma_context": { + "entrance_mass": "59038824075417799032780136585499589", + "joint_coefficient": "308461849925427171118076353794753/64", + "primitive_coefficient": "117600608836679351835159084859338679/32", + "residual_mass": "15259614246461931659309736794620779902271861133313062988612435126509213790586168872604898507585385733765513676582475908282056414302819372804609281/78338393111027970520960204800000000000000000" + }, + "M_caller": { + "entrance_mass": "1683307283016999532839217702665847040", + "joint_coefficient": "274838256141142176415070287809505/2", + "primitive_coefficient": "104781665096099932454228246133920343", + "residual_mass": "8157752610051527181179756772539507154773741043488805711776639249105573905795360887931494583164222855649110711012240079449883910365199677177007431/1468844870831774447268003840000000000000000" + }, + "M_joint_entrance": { + "entrance_mass": "363421601940370671219209686545270656", + "joint_coefficient": "59336854494143543914675236360327/2", + "primitive_coefficient": "22622085086540611235550148326673690", + "residual_mass": "326155049787256155157832340134847384764735629531953501631388760516641021999646985360258683049043029091571551527324903978689681205577462992724431/272008309413291564308889600000000000000000" + }, + "Sigma_caller": { + "entrance_mass": "1683307283016999532839217702665847040", + "joint_coefficient": "274838256141142176415070287809505/2", + "primitive_coefficient": "104781665096099932454228246133920343", + "residual_mass": "8157752610051527181179756772539507154773741043488805711776639249105573905795360887931494583164222855649110711012240079449883910365199677177007431/1468844870831774447268003840000000000000000" + } + }, + "joint_entries": [ + { + "entrance_defect": "1", + "entrance_mass": "3328", + "event": 21, + "stage": 1 + }, + { + "entrance_defect": "148410063514995949252033673132766658208788205370718967281003757134413789968247576890123412411417360771002399438531/1468844870831774447268003840000000000000000", + "entrance_mass": "34560", + "event": 66, + "stage": 2 + }, + { + "entrance_defect": "6381632731144825817837447944708966302977892830940915593083161556779792032980463086434983823972500433153103175856833/7344224354158872236340019200000000000000000", + "entrance_mass": "267520", + "event": 117, + "stage": 3 + }, + { + "entrance_defect": "48826910896433667303919078460680230550691319566966540235450236097222128474259273705792373154086285453659789415276699/7344224354158872236340019200000000000000000", + "entrance_mass": "2019072", + "event": 168, + "stage": 4 + }, + { + "entrance_defect": "368502187707734941992799610388659612332421113935495195758732328964749375895767848849231565512544435114398957805872473/7344224354158872236340019200000000000000000", + "entrance_mass": "15211776", + "event": 219, + "stage": 5 + }, + { + "entrance_defect": "185067349203199948717285990396560022786358892097286552199411685146613963574096207822049031289480441521439992099848157/489614956943924815756001280000000000000000", + "entrance_mass": "114566912", + "event": 270, + "stage": 6 + }, + { + "entrance_defect": "167258141581400434807041949620628023801304307452800276125691234290484311898457634378200156524669396283319704167224437/58753794833270977890720153600000000000000", + "entrance_mass": "862823680", + "event": 321, + "stage": 7 + }, + { + "entrance_defect": "52485367372141832448930960537076061442196157617560133497894259714342562011346744543603674618197532891465769563835926681/2448074784719624078780006400000000000000000", + "entrance_mass": "6498041600", + "event": 372, + "stage": 8 + }, + { + "entrance_defect": "395274324295395606266221720786098788106679044666935302423454439725497677831984827895113396754206979765882393647787395683/2448074784719624078780006400000000000000000", + "entrance_mass": "48937594112", + "event": 423, + "stage": 9 + }, + { + "entrance_defect": "34770148088268771123885638240582467875882870443862902474381161091381758183066044338445826245881726539112377437284173031282304172352873/3672112177079436118170009600000000000000000", + "entrance_mass": "2869851357661739006410624", + "event": 2166, + "stage": 10 + }, + { + "entrance_defect": "2132061314240615153963022002271372481864554550468185662116016915280957335371122066637196629786554796087683454080420471785443488518017871/7344224354158872236340019200000000000000000", + "entrance_mass": "87987819921824138957327936", + "event": 2299, + "stage": 11 + }, + { + "entrance_defect": "59294726363064922404621789792393824053641411624604231043152286361785887856547676020898247107168626281266089208191554336162878501528150267/7344224354158872236340019200000000000000000", + "entrance_mass": "2447027986812579413618418560", + "event": 2399, + "stage": 12 + }, + { + "entrance_defect": "1370442949490220658284117798109508244525288898764121312374304391903452843809231340294529097650081500353041222007493379363997059474011582831/7344224354158872236340019200000000000000000", + "entrance_mass": "56556669663990103089614108160", + "event": 2497, + "stage": 13 + }, + { + "entrance_defect": "10503316835277737472467818262779767183093508280117758483550393268697721167869964374834861002210885450305614830915194119326992544423973420583/2448074784719624078780006400000000000000000", + "entrance_mass": "1300380918848168161545814930560", + "event": 2593, + "stage": 14 + }, + { + "entrance_defect": "144898222987395514294262086496985033238868914132040587731913463221003023966933046051724595769679179510295059136019808464377754517290927477167/1468844870831774447268003840000000000000000", + "entrance_mass": "29898949589421721863235314186112", + "event": 2687, + "stage": 15 + }, + { + "entrance_defect": "5552604434653404492326202146632648555645894906058802502859978244800754925235135631121289535738651160785164468286369899500947044684216428143859/2448074784719624078780006400000000000000000", + "entrance_mass": "687449590445880987173716162586496", + "event": 2779, + "stage": 16 + }, + { + "entrance_defect": "383003665621269193739885837364643137711583221942238243718883845794553061807877316152810655052816963838773728158789271850484046376471557422298831/7344224354158872236340019200000000000000000", + "entrance_mass": "15806139033147704339825284871898752", + "event": 2869, + "stage": 17 + }, + { + "entrance_defect": "326155049787256155157832340134847384764735629531953501631388760516641021999646985360258683049043029091571551527324903978689681205577462992724431/272008309413291564308889600000000000000000", + "entrance_mass": "363421601940370671219209686545270656", + "event": 2958, + "stage": 18 + } + ], + "physical_main_inputs": 3952, + "sites": { + "ADD": 2108, + "IDLE_ONE": 100, + "J": 18, + "LAMBDA": 226, + "QUERY": 8, + "SCALE": 180, + "SWAP": 455, + "noninteger_scalar": 297 + } + }, + "native": { + "bounds": { + "Gamma": { + "exact": "148410063514995949252033673132766658208788205370718967281003757134410963910716096556086868772029200771002399438531/3672112177079436118170009600000000000000000", + "strict_power_of_two": 235, + "witness": { + "cut": 71273, + "factor": "1", + "kind": "public-return", + "register": 1443 + } + }, + "M": { + "exact": "14476760998861861302944912510523645403533730458331551801951984348669962992247520957465861449097781106116821932685203/104451190814703960694613606400000000000000000", + "strict_power_of_two": 237, + "witness": { + "cut": 71234, + "factor": "1", + "kind": "stored", + "register": 1443 + } + }, + "Sigma": { + "exact": "148410063514995949252033673132766658208788205370718967281003757134410963910716096556086868772029200771002399438531/3672112177079436118170009600000000000000000", + "strict_power_of_two": 235, + "witness": { + "cut": 71234, + "factor": "1", + "kind": "stored", + "register": 1443 + } + } + }, + "census": { + "denominator_bits": 19, + "events": 71273, + "lifetimes": 54, + "max_denominator": 393216, + "max_numerator": 14729531, + "numerator_bits": 24, + "opcodes": { + "ADD": 61196, + "CLEAR": 54, + "COPY": 1, + "INIT": 54, + "MOVE": 6306, + "SCALE": 3662 + }, + "owned_labels": 51, + "peak_owned": 43, + "public": 1482, + "scalars": { + "dyadic": 60716, + "integer": 38918, + "noninteger": 25941, + "odd": 4143 + } + }, + "independent_adjoint": { + "Gamma": { + "active_residual_sites": 24532, + "entrance_mass": "14476760998861861302944912510523645403533730458331551801951984348669962992247520957465861449097781106116821932685203/104451190814703960694613606400000000000000000", + "residual_mass": "148410063514995949252033673132766658208788205370718967281003757134410963910716096556086868772029200771002399438531/3672112177079436118170009600000000000000000" + }, + "M": { + "active_residual_sites": 24532, + "entrance_mass": "14476760998861861302944912510523645403533730458331551801951984348669962992247520957465861449097781106116821932685203/104451190814703960694613606400000000000000000", + "residual_mass": "148410063514995949252033673132766658208788205370718967281003757134410963910716096556086868772029200771002399438531/3672112177079436118170009600000000000000000" + }, + "Sigma": { + "active_residual_sites": 24532, + "entrance_mass": "14476760998861861302944912510523645403533730458331551801951984348669962992247520957465861449097781106116821932685203/104451190814703960694613606400000000000000000", + "residual_mass": "148410063514995949252033673132766658208788205370718967281003757134410963910716096556086868772029200771002399438531/3672112177079436118170009600000000000000000" + } + } + } + }, + "scope": "Exact children for common grid. Total RDiv plus complete-fibre unitary contracts for rounded envelopes. Neither is a physical provider admission.", + "threshold": { + "H": 14181100000000000000, + "Kstar_bits": 14073, + "LP": 2229, + "scaled4096_Kstar_bits": 14085 + } + }, + "source_head": "92b09a2bd2a8f6f2e0fb502068c1259350c2a8c8", + "status": "PASS_P104_RANK8_RETIMED_SPLIT", + "word_canonical_sha256": "a3bffcd29d5e7040d91a439d2fecfaa17a3c15a373da03099d44fd9c1261622a" +} diff --git a/research/p104-rank8-retimed-split/SCREEN-HITS.json b/research/p104-rank8-retimed-split/SCREEN-HITS.json new file mode 100644 index 0000000000..08710c3918 --- /dev/null +++ b/research/p104-rank8-retimed-split/SCREEN-HITS.json @@ -0,0 +1,152 @@ +[ + { + "frame": 745, + "pivot": 533, + "cut": 37420, + "ranks": [ + 3, + 5 + ], + "gain": 0.004078089746290203, + "paths": [ + { + "role": 533, + "lo": 37411, + "hi": 39699, + "frame": 745, + "old": 3, + "new": 747, + "moves": [ + 38792 + ], + "old_paid": [ + 6 + ], + "new_paid": [ + 3, + 3 + ], + "cost": 0.015026654526360872, + "private": false + } + ], + "a": { + "533": "1", + "1454": "-2" + }, + "b": { + "533": "1", + "1468": "1", + "843": "-1" + }, + "c": { + "533": "1", + "1251": "4", + "1468": "1", + "1454": "-2" + }, + "d": { + "1468": "1" + } + }, + { + "frame": 745, + "pivot": 1251, + "cut": 37420, + "ranks": [ + 3, + 5 + ], + "gain": 0.004078089746290203, + "paths": [ + { + "role": 1251, + "lo": 37412, + "hi": 38563, + "frame": 745, + "old": 3, + "new": 747, + "moves": [ + 37412 + ], + "old_paid": [ + 6 + ], + "new_paid": [ + 3, + 3 + ], + "cost": 0.015026654526360872, + "private": false + } + ], + "a": { + "1251": "1", + "1468": "-1" + }, + "b": { + "1251": "1/4", + "1468": "-3/4", + "1454": "1/2", + "843": "1" + }, + "c": { + "1468": "-1" + }, + "d": { + "1251": "1/4", + "1468": "-1", + "1454": "1/2" + } + }, + { + "frame": 745, + "pivot": 1251, + "cut": 37419, + "ranks": [ + 3, + 5 + ], + "gain": 0.004078089746290203, + "paths": [ + { + "role": 1251, + "lo": 37412, + "hi": 38563, + "frame": 745, + "old": 3, + "new": 747, + "moves": [ + 37412 + ], + "old_paid": [ + 6 + ], + "new_paid": [ + 3, + 3 + ], + "cost": 0.015026654526360872, + "private": false + } + ], + "a": { + "1251": "1", + "1468": "-1" + }, + "b": { + "1251": "1/4", + "1468": "-3/4", + "1454": "1/2", + "843": "3/4" + }, + "c": { + "1468": "-1" + }, + "d": { + "1251": "1/4", + "1468": "-1", + "1454": "1/2" + } + } +] diff --git a/research/p104-rank8-retimed-split/SCREEN-LOG.txt b/research/p104-rank8-retimed-split/SCREEN-LOG.txt new file mode 100644 index 0000000000..e8062b5acf --- /dev/null +++ b/research/p104-rank8-retimed-split/SCREEN-LOG.txt @@ -0,0 +1,36 @@ +windows 5598 +forward 0 systems 0 saved 0 sec 0.0 +forward 5000 systems 0 saved 0 sec 0.54 +forward 10000 systems 0 saved 0 sec 1.17 +forward 15000 systems 0 saved 0 sec 1.71 +forward 20000 systems 0 saved 0 sec 2.02 +forward 25000 systems 0 saved 0 sec 2.18 +forward 30000 systems 264 saved 7 sec 2.45 +forward 35000 systems 1368 saved 186 sec 4.86 +forward 40000 systems 2458 saved 337 sec 6.12 +forward 45000 systems 2848 saved 441 sec 6.8 +forward 50000 systems 2848 saved 441 sec 7.57 +forward 55000 systems 2848 saved 441 sec 7.97 +forward 60000 systems 2848 saved 441 sec 8.34 +forward 65000 systems 2848 saved 441 sec 9.15 +forward 70000 systems 2848 saved 441 sec 9.73 +prefix done 2848 saved 441 sec 9.788739919662476 +reverse 70000 pairs 0 hits 0 sec 9.8 +reverse 65000 pairs 0 hits 0 sec 9.86 +reverse 60000 pairs 0 hits 0 sec 10.04 +reverse 55000 pairs 0 hits 0 sec 10.27 +reverse 50000 pairs 0 hits 0 sec 10.66 +reverse 45000 pairs 0 hits 0 sec 11.53 +reverse 40000 pairs 0 hits 0 sec 12.04 +reverse 35000 pairs 158 hits 3 sec 13.15 +reverse 30000 pairs 164 hits 3 sec 23.86 +reverse 25000 pairs 164 hits 3 sec 25.41 +reverse 20000 pairs 164 hits 3 sec 26.65 +reverse 15000 pairs 164 hits 3 sec 27.49 +reverse 10000 pairs 164 hits 3 sec 28.01 +reverse 5000 pairs 164 hits 3 sec 28.16 +reverse 0 pairs 164 hits 3 sec 28.2 +paired 164 hits 3 seconds 28.204413890838623 +{'frame': 745, 'pivot': 533, 'cut': 37420, 'ranks': [3, 5], 'gain': 0.004078089746290203, 'paths': [{'role': 533, 'lo': 37411, 'hi': 39699, 'frame': 745, 'old': 3, 'new': 747, 'moves': [38792], 'old_paid': [6], 'new_paid': [3, 3], 'cost': 0.015026654526360872, 'private': False}]} +{'frame': 745, 'pivot': 1251, 'cut': 37420, 'ranks': [3, 5], 'gain': 0.004078089746290203, 'paths': [{'role': 1251, 'lo': 37412, 'hi': 38563, 'frame': 745, 'old': 3, 'new': 747, 'moves': [37412], 'old_paid': [6], 'new_paid': [3, 3], 'cost': 0.015026654526360872, 'private': False}]} +{'frame': 745, 'pivot': 1251, 'cut': 37419, 'ranks': [3, 5], 'gain': 0.004078089746290203, 'paths': [{'role': 1251, 'lo': 37412, 'hi': 38563, 'frame': 745, 'old': 3, 'new': 747, 'moves': [37412], 'old_paid': [6], 'new_paid': [3, 3], 'cost': 0.015026654526360872, 'private': False}]} diff --git a/research/p104-rank8-retimed-split/SOURCES.json b/research/p104-rank8-retimed-split/SOURCES.json new file mode 100644 index 0000000000..68fe2b9c1b --- /dev/null +++ b/research/p104-rank8-retimed-split/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "f16923d466a6aba912299882e0545564d2ba7bb2", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + } + ] +} diff --git a/research/p104-rank8-retimed-split/TASK.json b/research/p104-rank8-retimed-split/TASK.json new file mode 100644 index 0000000000..f3e4c1c5d4 --- /dev/null +++ b/research/p104-rank8-retimed-split/TASK.json @@ -0,0 +1,150 @@ +{ + "task_id": "p104-side-correction", + "scope_status": "changed", + "scope_change_reason": "Explicit donor continuation after #7105. Move from whole-boundary (3,127) to rank-eight group (3,245), pricing one relocated rank-six MOVE and all fourteen basis ADDs.", + "base_commit": "f16923d466a6aba912299882e0545564d2ba7bb2", + "priority_revision": 8, + "concrete_question": "Does one contact-free retiming in helper boundary group (3,245) on exact #7105 admit a fully paid independent split beating kappa .00363216151?", + "domain": "Exact #7105 word; existing nested charts; contact-free one-role paid retiming; rank-eight boundary group (3,245). Final witness retimes role533 and splits pivot1468 with integer basis changes.", + "success": "Changed complete profile, exact arbitrary-input and chart replay, complete caller/pricing/ordinary bill and all outer inequalities.", + "stop": "Reject if complete paid retiming costs consume split credit or ordinary budget fails.", + "predecessors": [ + "Ali Romman #5599 helper split and dyadic basis methods", + "Jerry Chen / CubeJerry #6805/#6916 paid retiming", + "DreamingOfClouds #6931 word and caller", + "retained source lineage in #6931 NOTICE", + "DreamingOfClouds #6936/#6937; CubeJerry #7000/#7001; ToikY #7003/#7004", + "dillona with OpenAI Codex #7105 causal paid retiming and split; public head92b09a2" + ], + "evidence_status": "Two complete author/source-aware CPython3.14.7 runs passed, including frozen-receipt comparison. Registered Python3.12 unavailable locally. No human/kernel acceptance.", + "overlap": "2026-11-10 14:06/14:07 UTC: 407 open and 6175 closed PR bodies; 7014 Discussion records and 10178 current tracked local notes. Source #7105 query has no matches; not proof of novelty.", + "ai_assistance": "Substantial OpenAI Codex assistance; no subagents.", + "predecessor_head": "92b09a2bd2a8f6f2e0fb502068c1259350c2a8c8", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19520521", + "schema_version": 1, + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "actual_scope": "Does one contact-free retiming in helper boundary group (3,245) on exact #7105 admit a fully paid independent split beating kappa .00363216151?", + "bottleneck_link": "Improve the full eighteen-LOCAL paid-minus-target moment by exposing one independent direction, with the same caller/provider contracts and no new scalar alphabet.", + "stop_rule": "One exact source-bound higher complete claim; no additional construction round after this result without refresh and expansion checkpoint.", + "evidence": "WITNESS.json, WORD.json.gz, RESULT.json and verify.py; exact predecessor source closure in inputs/pr7105.tar.", + "author": "Prepared for dillona with substantial OpenAI Codex assistance", + "outcome": "completed", + "open_questions": [ + { + "question": "Can the other two rank-eight nominations compose with this split?", + "why_it_matters": "Their boundary vectors overlap the same helper subspace, so three screen hits do not establish three independent gains.", + "first_step": "Recompute exact prefix/suffix capacity on the emitted successor, then fully price any joint basis changes.", + "blocked_by": "Joint independence and the changed cut geometry have not been established." + }, + { + "question": "Can this exact source be admitted under the retained five-assumption framework with a complete tariff/provider bridge?", + "why_it_matters": "Finite exact replay and source-unit caps do not instantiate the whole physical supplier application.", + "first_step": "Use the current #7000 admission review, its repaired BIT ambient cap134, and this word to produce an occurrence/interface map and upper-cost conversion.", + "blocked_by": "Complete caller/provider, storage, tariff and outer-threshold application remains open; source-specific review is required." + } + ], + "checkpoints": [ + { + "base": "f16923d466a6aba912299882e0545564d2ba7bb2", + "priority_revision": 8, + "decision": "Continue exact #7105 input with unchanged selected #6030 and priorities; read new #7000 admission review." + }, + { + "base": "f16923d466a6aba912299882e0545564d2ba7bb2", + "priority_revision": 8, + "decision": "Pre-submission fetch unchanged; latest #7106 is a scoped caller-query bound, no stronger kappa." + } + ] +} diff --git a/research/p104-rank8-retimed-split/VALIDATION.md b/research/p104-rank8-retimed-split/VALIDATION.md new file mode 100644 index 0000000000..e5ff0ef768 --- /dev/null +++ b/research/p104-rank8-retimed-split/VALIDATION.md @@ -0,0 +1,17 @@ +# Validation and limits + +Scientific source: public #7105 head `92b09a2bd2a8f6f2e0fb502068c1259350c2a8c8`. Canonical main was refreshed at entry and submission to `f16923d466a6aba912299882e0545564d2ba7bb2`; priorities revision 8 and selected #6030 were unchanged. The new #7000 admission review was read and its obligations retained. + +Two complete direct runs passed on macOS arm64, CPython 3.14.7. The first emitted a new receipt; the final run compared every result field against frozen `RESULT.json`: + +``` +python3 -I -B research/p104-rank8-retimed-split/verify.py +``` + +Final stdout is in `REPLAY.txt`, with its SHA256 and environment in `ENVIRONMENT.json`. Coverage: authenticated source reconstruction, exact rational cut identities, complete all-input adjoint and independent forward integer-grid endpoint replay, formal caller, full invoices and ordinary costs, two rational root enclosures, compiler/strictification/input lift and 54+4 outer gates, source precision engines and BIT artifact binding, five exact chart pairs including every Gaussian column and absolute phase, construction/grid/old-invoice rejection controls, relaxed native check and full width-512 physical replay at prime 1000000009, seed 11. + +All 24 archived #7105 members were separately compared against their Git blob IDs at the declared public source head. The metadata/provenance check passed. Explicit `-O` execution rejects before scientific work because pinned engines use assertions. + +The local interpreter has no Python 3.12. `VERIFY.json` registers the complete command for that environment; a local 3.12 run is not claimed. No Lean, Docker, whole selected multiplier or historical-suite sweep was run. Finite physical replay and exact scalar identities are different evidence. Source-engine reuse does not constitute independent human or proof-kernel review. + +All inherited framework assumptions and source-specific provider/caller/tariff application obligations remain. In particular, the passing source-unit cap is not a machine-step upper conversion. The #7000 BIT ambient-134 supplement was read, not rerun or discharged by the frozen BIT binding check. diff --git a/research/p104-rank8-retimed-split/VERIFY.json b/research/p104-rank8-retimed-split/VERIFY.json new file mode 100644 index 0000000000..f1330ca857 --- /dev/null +++ b/research/p104-rank8-retimed-split/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Regenerate exact predecessor and successor; rational prefix/suffix and forward/adjoint all-input checks, every new Gaussian column/phase, complete invoice and ordinary bill, two rational price engines, precision source engines, BIT binding, compiler and 54+4 outer gates, full width-512 physical replay and mutation controls. Source engines reject optimized mode explicitly." + } + ] +} diff --git a/research/p104-rank8-retimed-split/WITNESS.json b/research/p104-rank8-retimed-split/WITNESS.json new file mode 100644 index 0000000000..a586c69110 --- /dev/null +++ b/research/p104-rank8-retimed-split/WITNESS.json @@ -0,0 +1,48 @@ +{ + "frame": 745, + "pivot": 1468, + "cut": 37420, + "ranks": [ + 3, + 5 + ], + "paths": [ + { + "role": 533, + "lo": 37411, + "hi": 39699, + "frame": 745, + "old": 3, + "new": 747, + "moves": [ + 38792 + ], + "old_paid": [ + 6 + ], + "new_paid": [ + 3, + 3 + ], + "private": false + } + ], + "a": { + "533": "1", + "1454": "-2" + }, + "b": { + "533": "1", + "1468": "1", + "843": "-1" + }, + "c": { + "533": "1", + "1251": "4", + "1468": "1", + "1454": "-2" + }, + "d": { + "1468": "1" + } +} diff --git a/research/p104-rank8-retimed-split/WORD.json.gz b/research/p104-rank8-retimed-split/WORD.json.gz new file mode 100644 index 0000000000..2440b1072e Binary files /dev/null and b/research/p104-rank8-retimed-split/WORD.json.gz differ diff --git a/research/p104-rank8-retimed-split/construct.py b/research/p104-rank8-retimed-split/construct.py new file mode 100644 index 0000000000..1d816292f3 --- /dev/null +++ b/research/p104-rank8-retimed-split/construct.py @@ -0,0 +1,36 @@ +"""Retiming within one contact-free interval, then a checked helper split. +OpenAI Codex for dillona; Ali Romman and CubeJerry's split method. Apache-2.0. +""" +from copy import deepcopy +from fractions import Fraction as Q +from split import split +from support import L + +def prepare(word, hit): + paths=hit['paths']; L.need(len(paths)==1,'Exactly one paid retiming') + p=paths[0];r=p['role'];a,b,f=p['old'],p['new'],hit['frame'];cut=hit['cut'] + L.need(p['frame']==f and p['lo']<=cut<=p['hi'],'Cut in declared interval') + actual=[i for i in range(p['lo'],p['hi']) if word['program'][i][1]==r] + L.need(actual==p['moves'],'Every role event in interval is a relocated MOVE') + L.need(all(not(e[0]in('ADD','COPY')and e[2]==r)for e in word['program'][p['lo']:p['hi']]),'No intervening source read') + path=[word['program'][i]for i in actual] + L.need(path and all(e[0]=='MOVE' and e[1]==r and e[4]==p['private']for e in path),'Only MOVE events') + L.need(path[0][2]==a and path[-1][3]==b and all(x[3]==y[2]for x,y in zip(path,path[1:])),'Complete path') + spaces=[L.span(x)for x in word['frames']] + L.need(spaces[a]<=spaces[f]<=spaces[b] or spaces[b]<=spaces[f]<=spaces[a],'Nested intermediate frame') + remove=set(actual);program=[];split_cut=None + for i in range(len(word['program'])+1): + if i==cut: + if a!=f:program.append(['MOVE',r,a,f,p['private']]) + split_cut=len(program)-1 + if f!=b:program.append(['MOVE',r,f,b,p['private']]) + if i=maxgain-1e-12:continue + h=dict(role=r,lo=lo+1,hi=hi,frame=f,old=a,new=b,moves=mi,old_paid=paid,new_paid=[d1,d2],cost=cost,private=r>=n) + idx=len(windows);windows.append(h);starts[lo+1].append(idx);ends[hi+1].append(idx) +print('windows',len(windows),flush=True) +rows=[{r:Q(1)}if r=gain-1e-12 or len(used)!=1:continue + if not dyadic_program(basis(c,d,p,U)+basis(a,b,p,f)):continue + key=(f,p,tuple(sorted(c.items())),tuple(sorted(d.items())),tuple(sorted(a.items())),tuple(sorted(b.items()))) + if key in seen:continue + seen.add(key);hits.append(dict(frame=f,pivot=p,cut=cut,ranks=[dims[f]-dims[U],dims[V]-dims[f]],gain=gain-cost,paths=[windows[idx]for idx in used],a=a,b=b,c=c,d=d)) + if cut: + e=w['program'][cut-1];op,r=e[:2] + if op in('INIT','CLEAR'):cols[r]={} + elif op=='SCALE':cols[r]={k:v*Q(e[2])for k,v in cols[r].items()} + elif op in('ADD','COPY'): + add(cols[e[2]],cols[r],Q(e[3])) + if op=='COPY':cols[r]={} + if cut%5000==0:print('reverse',cut,'pairs',pairs,'hits',len(hits),'sec',round(time.time()-start,2),flush=True) +hits.sort(key=lambda h:-h['gain']) +(Path(sys.argv[2])).write_text(json.dumps(encode(hits),indent=2)+'\n') +print('paired',pairs,'hits',len(hits),'seconds',time.time()-start,flush=True) +for h in hits[:10]:print({k:v for k,v in encode(h).items()if k not in('a','b','c','d')},flush=True) diff --git a/research/p104-rank8-retimed-split/inputs/pr7105.tar b/research/p104-rank8-retimed-split/inputs/pr7105.tar new file mode 100644 index 0000000000..7be8d64f96 Binary files /dev/null and b/research/p104-rank8-retimed-split/inputs/pr7105.tar differ diff --git a/research/p104-rank8-retimed-split/source.py b/research/p104-rank8-retimed-split/source.py new file mode 100644 index 0000000000..e53273eb27 --- /dev/null +++ b/research/p104-rank8-retimed-split/source.py @@ -0,0 +1,53 @@ +"""Authenticated read-only extraction and rebuilding of the exact #7105 input.""" +from contextlib import contextmanager +from hashlib import sha256,sha1 +from pathlib import Path +import importlib.util,json,sys,tarfile,tempfile +HERE=Path(__file__).resolve().parent + +def need(ok, why): + if not ok:raise ValueError(why) + +def read(p): + import gzip + raw=Path(p).read_bytes() + return json.loads(gzip.decompress(raw)if raw[:2]==b'\x1f\x8b'else raw) + +def load(name,path): + spec=importlib.util.spec_from_file_location(name,path);m=importlib.util.module_from_spec(spec);sys.modules[name]=m;spec.loader.exec_module(m);return m + +def canonical(x):return json.dumps(x,sort_keys=True,separators=(',',':')).encode() + +@contextmanager +def sources(): + pins=read(HERE/'INPUTS.json');archive=HERE/'inputs/pr7105.tar' + need(sha256(archive.read_bytes()).hexdigest()==pins['archive_sha256'],'Immutable source archive SHA256') + with tempfile.TemporaryDirectory(prefix='kappa7105-')as tmp: + root=Path(tmp).resolve();expected={x['path']:x for x in pins['files']};seen=set() + with tarfile.open(archive)as tar: + for member in tar: + if member.isdir():continue + need(member.isfile()and member.name in expected and member.name not in seen,'Unique listed regular source member') + path=root/member.name;need(path.resolve().is_relative_to(root),'Safe source member') + raw=tar.extractfile(member).read();pin=expected[member.name] + need(len(raw)==pin['size'] and sha256(raw).hexdigest()==pin['sha256'] and sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest()==pin['git_blob'],'Exact per-file Git blob and SHA256') + path.parent.mkdir(parents=True,exist_ok=True);path.write_bytes(raw);seen.add(member.name) + need(seen==set(expected),'Complete source closure') + previous=root/'research/p104-causal-retimed-step' + old_path=list(sys.path);sys.path.insert(0,str(previous)) + try: + source_engine=load('pr7105_source',previous/'source.py') + constructor=load('pr7105_constructor',previous/'construct.py') + with source_engine.sources() as (base,ancestor): + word=constructor.construct(ancestor,read(previous/'WITNESS.json')) + need(canonical(word)==canonical(read(previous/'WORD.json.gz')),'Entire regenerated #7105 source word') + need(sha256(canonical(word)).hexdigest()==pins['source_canonical_sha256'],'Exact regenerated #7105 canonical SHA256') + yield base,word,previous + finally:sys.path[:]=old_path + +if __name__=='__main__': + import argparse,gzip + parser=argparse.ArgumentParser();parser.add_argument('--output',type=Path,required=True);args=parser.parse_args() + with sources()as(base,word,previous): + raw=canonical(word) + with args.output.open('xb')as out:out.write(gzip.compress(raw,mtime=0)if args.output.suffix=='.gz'else raw+b'\n') diff --git a/research/p104-rank8-retimed-split/split.py b/research/p104-rank8-retimed-split/split.py new file mode 100644 index 0000000000..3260b2a0a3 --- /dev/null +++ b/research/p104-rank8-retimed-split/split.py @@ -0,0 +1,145 @@ +"""Split independent helper jobs with three scalar basis changes. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +Adapted for arbitrary counted owned-field inventory by @CubeJerry with OpenAI assistance. +Successor: OpenAI Codex for dillona excludes both hosted main planes from helper groups. +The source word and caller retain the credits in README.md. +""" +from copy import deepcopy +from fractions import Fraction as Q +from support import L + + +def inverse(program): + return [[e[0], *e[1:-2], + str(1/Q(e[-2]) if e[0] == 'SCALE' else -Q(e[-2])), e[-1]] + for e in reversed(program)] + + +def basis(a, b, pivot, frame): + """Return B with row pivot equal to a and B b equal to e_pivot.""" + L.need(sum(v*b.get(k, 0) for k, v in a.items()) == 1, 'Unit basis pairing') + roles = sorted(set(a) | set(b) | {pivot}) + values, program = dict(b), [] + + def emit(event): + program.append(event) + r, q = event[1], Q(event[-2]) + if event[0] == 'SCALE': + values[r] = values.get(r, 0)*q + else: + values[r] = values.get(r, 0)+q*values.get(event[2], 0) + + j = pivot if b.get(pivot) else next(r for r in roles if b.get(r)) + if j != pivot: + for event in [['ADD', pivot, j, '1', frame], + ['ADD', j, pivot, '-1', frame], + ['ADD', pivot, j, '1', frame], + ['SCALE', j, '-1', frame]]: + emit(event) + if values[pivot] != 1: + emit(['SCALE', pivot, str(1/values[pivot]), frame]) + for r in roles: + if r != pivot and values.get(r): + emit(['ADD', r, pivot, str(-values[r]), frame]) + L.need(all(values.get(r, 0) == int(r == pivot) for r in roles), 'Basis column') + inverse_rows = {r: {r: Q(1)} for r in roles} + for e in inverse(program): + if e[0] == 'SCALE': + inverse_rows[e[1]] = {k: Q(e[-2])*v for k, v in inverse_rows[e[1]].items()} + else: + L.add(inverse_rows[e[1]], inverse_rows[e[2]], Q(e[-2])) + row = {} + for r, q in a.items(): + L.add(row, inverse_rows[r], q) + L.need(row[pivot] == 1, 'Basis row coefficient') + for r in roles: + if r != pivot and row.get(r): + program.append(['ADD', pivot, r, str(row[r]), frame]) + return program + + +def check_cut(word, h): + """Check the whole prefix row and suffix column over the rationals.""" + n, cut, f, p = word['public'], h['cut_after'], h['frame'], h['pivot'] + a, b, c, d = ({int(k): Q(v) for k, v in h[s].items()} for s in ('a', 'b', 'c', 'd')) + main = set(word['live']) | {r+112 for r in word['live']} | set(word['hosted']['X2']) | set(word['hosted']['Y2']) + L.need(p < n and p not in main, 'A helper supplies the retained output role') + u, v = word['initial'][p], word['final'][p] + group = {r for r in range(n) if r not in main and + (word['initial'][r], word['final'][r]) == (u, v)} + L.need(set(c) | set(d) <= group, 'Both boundary vectors use one helper group') + L.need(L.span(word['frames'][u]) < L.span(word['frames'][f]) < L.span(word['frames'][v]), + 'Two strictly productive nested targets') + L.need(h['ranks'] == [len(word['frames'][f])-len(word['frames'][u]), + len(word['frames'][v])-len(word['frames'][f])], 'Declared split ranks') + rows = [{r: Q(1)} if r < n else {} for r in range(n+word['owned_fields'])] + current = word['initial']+[None]*word['owned_fields'] + for e in word['program'][:cut+1]: + op, r = e[:2] + if op == 'MOVE': + current[r] = e[3] + elif op in ('INIT', 'CLEAR'): + rows[r] = {} + current[r] = e[2] if op == 'INIT' else None + elif op == 'SCALE': + rows[r] = {k: Q(e[-2])*x for k, x in rows[r].items()} + elif op == 'COPY': + rows[r] = {k: Q(e[-2])*x for k, x in rows[e[2]].items()} + else: + L.add(rows[r], rows[e[2]], Q(e[-2])) + L.need(all(current[r] == f for r in set(a) | set(b) | {p}), 'One intermediate chart') + total = {} + for r, q in a.items(): + L.add(total, rows[r], q) + L.need(total == c, 'Exact prefix functional; no other input') + column = [b.get(r, Q(0)) for r in range(n+word['owned_fields'])] + for e in word['program'][cut+1:]: + op, r = e[:2] + if op in ('INIT', 'CLEAR'): + column[r] = Q(0) + elif op == 'SCALE': + column[r] *= Q(e[-2]) + elif op == 'COPY': + column[r] = Q(e[-2])*column[e[2]] + elif op == 'ADD': + column[r] += Q(e[-2])*column[e[2]] + L.need(column == [d.get(r, Q(0)) for r in range(n+word['owned_fields'])], 'Exact suffix direction; no other output') + L.need(sum(x*b.get(r, 0) for r, x in a.items()) == + sum(x*d.get(r, 0) for r, x in c.items()) == 1, 'Both independent pairings') + return a, b, c, d + + +def split(word, h): + a, b, c, d = check_cut(word, h) + n, p, f, cut = word['public'], h['pivot'], h['frame'], h['cut_after'] + u, v = word['initial'][p], word['final'][p] + + def shift_owned(event): + e = event.copy() + e[1] += int(e[1] >= n) + if e[0] in ('ADD', 'COPY'): + e[2] += int(e[2] >= n) + return e + + def use_successor(event): + e = event.copy() + if e[1] == p: + e[1] = n + if e[0] in ('ADD', 'COPY') and e[2] == p: + e[2] = n + return e + + boundary, middle = basis(c, d, p, u), basis(a, b, p, f) + out = deepcopy(word) + out['public'] = n+1 + out['initial'].append(f) + out['final'].append(v) + out['final'][p] = f + out['program'] = inverse(boundary) + out['program'] += [shift_owned(e) for e in word['program'][:cut+1]] + out['program'] += [shift_owned(e) for e in middle] + out['program'] += [use_successor(shift_owned(e)) for e in inverse(middle)] + out['program'] += [use_successor(shift_owned(e)) for e in word['program'][cut+1:]] + out['program'] += [use_successor([*e[:-1], v]) for e in boundary] + return out diff --git a/research/p104-rank8-retimed-split/support.py b/research/p104-rank8-retimed-split/support.py new file mode 100644 index 0000000000..192cd38d27 --- /dev/null +++ b/research/p104-rank8-retimed-split/support.py @@ -0,0 +1,18 @@ +"""Small exact sparse operations, retained from Ali Romman/CubeJerry. Apache-2.0.""" +class L: + @staticmethod + def need(ok, why): + if not ok: raise ValueError(why) + @staticmethod + def add(dst, src, q): + for k,v in tuple(src.items()): + value=dst.get(k,0)+q*v + if value: dst[k]=value + else: dst.pop(k,None) + @staticmethod + def span(basis): + out={0} + for v in basis: + L.need(type(v) is int and 0