diff --git a/.github/workflows/e8-seven-stage-coupled-retiming.yml b/.github/workflows/e8-seven-stage-coupled-retiming.yml new file mode 100644 index 0000000000..811b1caf72 --- /dev/null +++ b/.github/workflows/e8-seven-stage-coupled-retiming.yml @@ -0,0 +1,36 @@ +name: Verify seven-stage E8 coupled retiming +on: + pull_request: + paths: + - 'research/e8-seven-stage-coupled-retiming/**' + - '.github/workflows/e8-seven-stage-coupled-retiming.yml' + push: + paths: + - 'research/e8-seven-stage-coupled-retiming/**' + - '.github/workflows/e8-seven-stage-coupled-retiming.yml' + workflow_dispatch: +permissions: + contents: read +jobs: + verify: + runs-on: ubuntu-latest + strategy: + fail-fast: false + matrix: + python: ['3.11', '3.14'] + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 + with: + python-version: ${{ matrix.python }} + - name: Install verifier dependencies + run: | + sudo apt-get update + sudo apt-get install -y g++ libboost-dev + python -m pip install -r research/e8-seven-stage-coupled-retiming/requirements.txt + - name: Replay source and new certificate + run: python -B research/e8-seven-stage-coupled-retiming/verify.py "$RUNNER_TEMP/e8-composed" + - name: Confirm source tree unchanged + run: git diff --exit-code diff --git a/certificates/joint-dual-kappa.json b/certificates/joint-dual-kappa.json index b7f7b89bc2..1f35b89221 100644 --- a/certificates/joint-dual-kappa.json +++ b/certificates/joint-dual-kappa.json @@ -842,7 +842,7 @@ "scripts/experiments/pin_joint_dual_sources.py": "4d31cc0e38b7902709ca5f8f714cba109760d2592346dd7f8dc0b900a2d9fe00", "scripts/experiments/verify_joint_dual.py": "7a31bba1e9c0ded32ae285df2ca9bc91ef20c330f6789fdba361876f3c7a1985" }, - "source_manifest_sha256": "4f3c15b82a2d97335d4fe95fb8bcb96bd2a921087da289d9da16c68213a17f17", + "source_manifest_sha256": "698fe862a620e5b80b85fbc6034c9456fa0fa9aea638dbbbcb3f9edd24c0415e", "sources": [ { "files": { diff --git a/certificates/joint-dual-validation.json b/certificates/joint-dual-validation.json index 194861d3c3..61a8d41622 100644 --- a/certificates/joint-dual-validation.json +++ b/certificates/joint-dual-validation.json @@ -226,7 +226,7 @@ } }, "bit_saving": "2382370177/50000000000000", - "certificate_sha256": "9801147b1502cf1e43d5fa39aa37f5291f03b48c30c4dd4f272e0877894a1c24", + "certificate_sha256": "6f684fa7f747073a132e8d0b5652cf12a8afa389f2a16ff6ade8e080d786dd22", "kappa": "4764513337/100000000000000", "margins": 7, "producer_words_regenerated_and_matched": true, diff --git a/research/e8-seven-stage-coupled-retiming/EXPECTED.json b/research/e8-seven-stage-coupled-retiming/EXPECTED.json new file mode 100644 index 0000000000..76fb5e9d6c --- /dev/null +++ b/research/e8-seven-stage-coupled-retiming/EXPECTED.json @@ -0,0 +1,110 @@ +{ + "baseline": { + "K": 3, + "stages": 7, + "idle_blocks_per_role_pair": [ + 27, + 7, + 14, + 7, + 20, + 27, + 1, + 7, + 6 + ], + "h": 8, + "T": 7, + "maxchild": 27, + "bit_moment_interval": [ + "26959946667150639756721257363109509664221746641166408767853702235917/26959946667150639794667015087019630673637144422540572481103610249216", + "26959946667150639756721257363109509664221746641166408767853702235919/26959946667150639794667015087019630673637144422540572481103610249216" + ], + "normalized_histogram": { + "1": 103404, + "2": 46158, + "3": 21952, + "4": 20482, + "5": 15092, + "6": 1778, + "8": 882, + "27": 3360, + "7": 5040, + "14": 1680, + "20": 1680 + }, + "W": 11095, + "m": 56, + "bit_coarse": "968197503705007/1000000000000000000", + "complex_coarse": "119394377245827/125000000000000000", + "binding": "complex", + "kappa": "95424356568133/100000000000000000", + "kappa_float": 0.00095424356568133 + }, + "candidate": { + "K": 3, + "stages": 7, + "idle_blocks_per_role_pair": [ + 27, + 7, + 14, + 7, + 20, + 27, + 1, + 7, + 6 + ], + "h": 8, + "T": 7, + "maxchild": 27, + "bit_moment_interval": [ + "26959946667150639756721257363109509664221746641166408767853702235917/26959946667150639794667015087019630673637144422540572481103610249216", + "26959946667150639756721257363109509664221746641166408767853702235919/26959946667150639794667015087019630673637144422540572481103610249216" + ], + "normalized_histogram": { + "1": 103404, + "2": 46158, + "3": 21952, + "4": 20482, + "5": 15092, + "6": 1778, + "8": 882, + "27": 3360, + "7": 5040, + "14": 1680, + "20": 1680 + }, + "W": 11095, + "m": 56, + "bit_coarse": "968197503705007/1000000000000000000", + "complex_coarse": "955306874505079/1000000000000000000", + "binding": "complex", + "kappa": "954395132518163/1000000000000000000", + "kappa_float": 0.000954395132518163 + }, + "complex_ledger": { + "histogram": { + "1": 14651, + "2": 4186, + "3": 3654, + "4": 987, + "5": 1463, + "6": 2585, + "7": 301, + "8": 648, + "9": 56, + "16": 240, + "22": 240, + "32": 240, + "38": 240 + }, + "calls": 29491, + "rank_mass": 94473, + "max_child": 38, + "deficit": 216, + "copy_calls": 56, + "centres": 8, + "idle_calls": 1680 + } +} diff --git a/research/e8-seven-stage-coupled-retiming/LICENSE b/research/e8-seven-stage-coupled-retiming/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/e8-seven-stage-coupled-retiming/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/e8-seven-stage-coupled-retiming/MANIFEST.json b/research/e8-seven-stage-coupled-retiming/MANIFEST.json new file mode 100644 index 0000000000..4822a32930 --- /dev/null +++ b/research/e8-seven-stage-coupled-retiming/MANIFEST.json @@ -0,0 +1,186 @@ +{ + "EXPECTED.json": "b0f32ed1e464e3e2adbb766f8c5d4e08743c8b18ef1634f285d8fb322ca0832a", + "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "NOTICE.md": "2c611d6494ef3156d8c5b56e13d5ae4713681ec3fc37619d911eecbdf2d7366e", + "README.md": "8331df59babecfcd44671d9e27a886744ae0d058e8a401d4072eab00ccf107b1", + "SOURCES.json": "6bfa222a5e75e8ab9929f7dd873e3725d079850a7f1de4266ca7a6fdc335ae9d", + "candidate-pins-b3.json": "02ec9d069f166d57ef0c82c6bbab3dc7a30eb287779e508fdce1a82d4886b80e", + "requirements.txt": "12ce61badd5c50c101d6d759e1de6bc494be3f906df49a63b6db20d7e54a7348", + "source365/NOTICE.md": "d90e498b08ebc83951ae44f5b3c507eac314ee03e7cab53df675e7a86da9046b", + "source365/PROOF.md": "f21c7a5f54ae39763765c833f8f4c916340f3417b508c267153a0fe52358c0c9", + "source365/README.md": "1d014a1835d3e50e0c8e10d4e1c18afe7e91837707e184440d0ca893ea50c165", + "source365/data/original.json.gz": "4b92f00fc7454b9b15e6d71a3b05062792eacca0a0ca4efee46f87827d57c8aa", + "source365/data/retimed.json.gz": "31467ace2b1667630b72e488e688911a0404b4755d0d2c87560b111ed4c07998", + "source365/reconstruct.py": "5a3d1e4cc45dde080a999f4a94040eba2d52c01877ffe70ae121109fbf9853e5", + "source365/retime.py": "0b4cddf5c9c0cb738b0e023d1108c65daf465843397428fef57f99c5bc7c1683", + "source365/scalar_map_comparison.py": "4ee8a3c9074d2e599e124882e182e0fc8397d9ef420f99508b7a7b0f0f9066e9", + "source365/sources.json": "016a1eb4edd569c2b13fdde9c39f7144f30c659eb3f947fae97c795a8905bbc5", + "source365/verification.json": "97874902c6548cf6fd04ead2345a7e40ad960407771515af40f202a9eac637b6", + "source365/verify.py": "2230294a81b980a4bee415e387e0371def5cda1e4651146dd1f98c4ad7911a6e", + "source375/LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "source375/MANIFEST.sha256": "51e760e691524dfe010bf84cda7f3cfcbf5f6a9383ef42dc4b99e81f2bbb5b53", + "source375/NOTICE-PR352.md": "967e6d7e76e216e4898cf543c75b527e8d397ec1ddba3800cb20701f24c89524", + "source375/NOTICE.md": "949fafcf2c993d0a719ee24adacabbf2d578bd657f234b38ba0464cd0d9dd759", + "source375/README.md": "378ab6a356cdc604204f9caf6c262fe7d29258db317435e6c65f0b2d0d59178e", + "source375/SOURCE-pr363.json": "8d44d9d894c70ef195d44468f6093e797f8757a969bda93b508f65bf334e6ade", + "source375/SOURCE-pr370.json": "ba19bc388a7da6f91a7eb85ed4ee98f309eda557d1206fc3b55c3fa070ca23b5", + "source375/SOURCE-pr373.json": "20e7c346d38cabed0555586fc99f96d497ae80d9e7b26286e84eed33a56db6e1", + "source375/code/bit/checkers/certify_bit_g.py": "c9a31508126f34e7ac95d802c39e8919a872cd705314de5bf3538de1636ce8ce", + "source375/code/bit/checkers/certify_bit_k.py": "97b07eb2e2664522f672fb520d188520a3a2967ecefd6700667994614d478e0c", + "source375/code/bit/checkers/columns_h.cpp": "d1297f9052be4f2496e1ff2a77e4db2c0cdbd7d460d489b4c03e50bf317238ce", + "source375/code/bit/checkers/columns_k.cpp": "1c344d18fcd494eeca93e259f10cafae7705780e6592f6dcb35b34752dab9bc2", + "source375/code/bit/checkers/cost.py": "d55d2b865d1c3d35e343e1a38c592b9172ed8e2596d1107e34d92e2a80c7d03f", + "source375/code/bit/checkers/exactnd_h.py": "28a0d8ee29ac75b8a789705454987f07d618f135ed1f1bd45b97f18bcc4163e3", + "source375/code/bit/checkers/finite_g.py": "a591d8caa9ab50a4c7ec6934c71c93fc18fd14680180b43071e8d9d704f7ac9a", + "source375/code/bit/checkers/finite_k.py": "f93207e50f1e07237d8c29ecef6b7be89f7c35e3f0c0f2449da8f7c66f6442e1", + "source375/code/bit/checkers/geometry_g.py": "b9fa3cd05f36f5fcebfdebfb4a86fb90e92ed3c1d9157c52918ee8c5b563b54f", + "source375/code/bit/checkers/geometry_k.py": "0609920cffe790e927a4106bb82e63b3f8078c647ac9156fe0d22624634e759f", + "source375/code/bit/checkers/gram_frames.py": "223a5a07731fc315a90a3e48177796babc155c1d9985c7ae5017eff6af2a0608", + "source375/code/bit/checkers/json.hpp": "aaf127c04cb31c406e5b04a63f1ae89369fccde6d8fa7cdda1ed4f32dfc5de63", + "source375/code/bit/checkers/legality_h.cpp": "6c1ef2b24e57781d6951c172a1024fc4300e6fd392c9d6672079a7806ab663b3", + "source375/code/bit/checkers/tile_g.py": "8140eec180e42202f2c6a9f11f5c92885e60861c38a7611dd805c524e3438138", + "source375/code/bit/checkers/tile_k.py": "64255088821f601ede2c3006f08cb97c39a4fa10dbbeb93a8a71fcfa0e1d8d77", + "source375/code/bit/export_records.py": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "source375/code/bit/independent/centres_sat.py": "f69379968367544807db2f0cf14359977e56299383b3edcc4469ddea7c7ecb40", + "source375/code/bit/independent/checkword.py": "11bf9620ca9db16d52d9fe806b814fc9ec9a89c4d7645354d1861d96f6e805ad", + "source375/code/bit/independent/mutate.py": "0ff65aace5da4b57d96235bf830f8f11969322e75134d498aeb70e9753ec6b0d", + "source375/code/bit/mutate_records.py": "b0e75d6550412a7be4017695e6b237392b611bb852ad8ff309d6682c9f166a4e", + "source375/code/bit/producer/compile.py": "60fea6a9d6617a3f87376d3fda040642e9cb70e7c179015e03ede8d289f30357", + "source375/code/bit/producer/compile2.py": "0e23d4282ceb75768e82631da016aaff9818aec53c7d75a6b2a28ee1b1160dc3", + "source375/code/bit/producer/e8lib.py": "4f8a6843e83bc4f7055d7337f33dbe12ce499051f46bee1b81bbf6b34c652574", + "source375/code/bit/producer/frames.py": "ba71f77dd3e3c1c54f361c066cebe9faadbc78db46376046e7af625bf1de8c24", + "source375/code/bit/producer/fullword.py": "0daf87599e9e48646b985ad87351c56c1b73cfc99cdf9eca081483846ddbfa90", + "source375/code/bit/producer/ham1.py": "359040fb432fd392472af6b8f5dca0234dd6c2be744a791df27ba62bc5da5175", + "source375/code/bit/producer/ham2.py": "fdf0af785ce697bd7f80b4e75f7163735f3b599d9dc42f652f0ffdbdf18ea8bf", + "source375/code/bit/producer/params-r865.json": "1256c54debe0a551da8e24896ab73ef0bd4a5233ff8e6fedf21a9e6301d6e6f3", + "source375/code/bit/producer/price.py": "46c858e60ba0a117bf8227b864abf55e85ebee2d56a0dce64472b706499ac405", + "source375/code/bit/producer/search2.py": "4999c5d6bac9757e4236c45435201631eae21f644dc9543d8c0b6e3cc8360daf", + "source375/code/bit/receipts_e8.py": "935ea65d9c6739e868ccf1aa439bd3c246657dfc887e4a0222a8f0901a5b41a5", + "source375/code/bit/receipts_k.py": "67f714e10a846e9cc62996342f825cd715055031e0b12591abdafd225717e195", + "source375/code/bit/regression/certify_bit.py": "fc03e8f7bf73d7d70346b87c835d44508b0581c9ff9aec708fbbd4f0121e0394", + "source375/code/bit/regression/columns_h_pr346.cpp": "26f5c9be3a7f545d50be458e3d17403921b5542a7dcd2986c848664a774977a8", + "source375/code/bit/regression/cost.py": "d55d2b865d1c3d35e343e1a38c592b9172ed8e2596d1107e34d92e2a80c7d03f", + "source375/code/bit/regression/json.hpp": "aaf127c04cb31c406e5b04a63f1ae89369fccde6d8fa7cdda1ed4f32dfc5de63", + "source375/code/bit/regression/legality_h_pr346.cpp": "5661d0b91e07d95736bde4c1824f27bebaecce0a84e38403f5391ebc51a52056", + "source375/code/bit/regression/prime_new.py": "7bd5cb48537621f1217d174274d42483da4e2d02feec238643c798c36b30366a", + "source375/code/bit/regression/prime_witnesses.py": "98cd03bc9582e7bd0ab194c191ea8eea940539e510051443ab9fd3e572a364ab", + "source375/code/bit/regression/stage_cohort.py": "6c288f6f234b528c1a7c0a4adfb724e91e0fe6b18c8dffad96af3f973de1829a", + "source375/code/bit/regression/tile_check.py": "38c3f78daac118395565a65fa3543b1c349638ff2519ce7fda0dad2d788e90ae", + "source375/code/certify_b3.py": "616bf82b56077c9e575791a70715047a5e01932649c3feb3e4c8ec56b39c9fab", + "source375/code/complex/code/bridged.py": "5fe7174cd3a6580a74e4c1bf8fa7b426e8673f1c285603bf3076d4e758d70731", + "source375/code/complex/code/complex_basis.py": "52d68781eaf6d9decf02446a532a7336fcf15924a9f6781ba0833d038decb9f8", + "source375/code/complex/code/complex_gx.py": "ccc924537db0c0d55f0c1934e79b8cf4d85b4fb336473d7b42d69e12557aa9f2", + "source375/code/complex/code/complex_labels.py": "e000ee131389fec427388b85f632879cbaaf10e5e5d979a47d6307d64ce58982", + "source375/code/complex/code/complex_scalars.py": "c617b0fd2e18adcff15f6bf6cb3d54cc31f8432993be048b3442a5729eeff410", + "source375/code/complex/code/complex_splice.py": "dfb4c9108bfea4a09f3e38f12b9dbe6164abab1a4fef8442ca593e2110d38ef4", + "source375/code/complex/code/p10pins.py": "93b78a2e038b23264d04836928c78b6ebf33b87ff3dcc0e43ba0f1748fadd143", + "source375/code/complex/code/scatter.py": "dfd1afbbb3ff86f54db6a0313916403ec8ee6f939caa62f3edcc9d7a151bff95", + "source375/code/complex/inputs/complex/LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "source375/code/complex/inputs/complex/NOTICE": "9419dd03a2f52cf8bdfc4d18216ce29f263ab583b27f01ced8e420985bcb7c81", + "source375/code/complex/inputs/complex/retained/FINITE_BRIDGE.txt": "66d8f4ea8752abd89952d6674a636575a0db16e18b1c16e293f48f64242f0c46", + "source375/code/complex/inputs/complex/retained/compact-control-layout.tex": "2bc28e50f3eb092195294cafa81213e520f6d42e7935e9905ad8a6199e2a7c87", + "source375/code/complex/inputs/complex/retained/compact-control-movement.tex": "b963c3d2f4e1b7059aa289bb4b4ac89b688920bcf42f5b20d7698cdef0132cc6", + "source375/code/complex/inputs/complex/retained/copied-centers-assembly.tex": "00117892971ae766188ace0af03030c44164fda105e42b70d84f52c3339a7dcb", + "source375/code/complex/inputs/complex/retained/copied-centers-lemma.tex": "d0ce6d3d504996aadb098227885224e48df46101daec8893523a0a8b7364d8fe", + "source375/code/complex/inputs/complex/retained/endpoint-gauge-complex.tex": "dfee33b0281e5551bb6927f757ff0240abade60ae1800f715afd88853ae0191e", + "source375/code/complex/inputs/complex/retained/general-clifford-frames.tex": "c9bb9655b594583c6b4bab8cb485233f1d1e588f83858cf1e4c3530cee8fed54", + "source375/code/complex/inputs/complex/retained/stopped-product-complex.tex": "4738089103a4b263b3b0ef458f5ef35519c696f1ea871ae79e508d3720f5870a", + "source375/code/complex/inputs/complex/source-pins.json": "0d76527bf9c259b9532466a7b056ad6ff118867a96e044ff8e1a24aca12e1dbb", + "source375/code/complex/inputs/complex/sources/Work__Bridge__Cert.lean": "5c24746a6330907b9b37d6064095035a58575d64ce793d6d7c9881121fdc3980", + "source375/code/complex/inputs/complex/sources/Work__Bridge__Net.lean": "cf7d7d330b1bffe2e66712c873e647b13dc32db1ccfc0e0f4cd62ee6caf584f0", + "source375/code/complex/inputs/complex/sources/Work__Carrier__Live.lean": "6d0649eb62589e66057f044e1e2103fc42f3f57a1498f82a26565bd8eb4026d0", + "source375/code/complex/inputs/complex/sources/Work__Carrier__Phases.lean": "71dc3dda23dfe510d5d53cbada3a6c540cd1dc2825503fda618a5bd6cfc3e812", + "source375/code/complex/inputs/complex/sources/Work__Fourier__Main.lean": "2e8e88efd4dcbdf0b1a6e39ce7eea8c5fd5ffee2faf360a8c0c9cba84c0e4ef3", + "source375/code/complex/inputs/complex/sources/Work__GCert__Chain__Geom.lean": "c302f5834287421f11f3b0da7112fcde876cbc702896f2af4145b2d72ee393a2", + "source375/code/complex/inputs/complex/sources/Work__GCert__Chain__InvThm.lean": "ade7e7873da75ca63a4b5ce2f562dde9c12bfbb69d87d7ae831039ff790e5adb", + "source375/code/complex/inputs/complex/sources/Work__GCert__Chain__NetCert.lean": "22ae34809466b4ac2a2c5cdde526f51ff246f5189f7c142b38aa4c0dcffb04a4", + "source375/code/complex/inputs/complex/sources/Work__GCert__Chain__NetDef.lean": "6e17a68b1e988969f6eb77000028f7ed877e687b8ad3976ec1707fcfe1d2f520", + "source375/code/complex/inputs/complex/sources/Work__GCert__Chain__NetStage.lean": "c122bc01392a6fdcc0bee918fed81804d3c9b1d3e071016dab65a4ed804ef0b6", + "source375/code/complex/inputs/complex/sources/Work__GCert__Chain__Phased.lean": "0de429c80231334f1ce92575c1e8ac382ca2d5e7d956767b547639a8941d9a8c", + "source375/code/complex/inputs/complex/sources/Work__GCert__Chain__WinB.lean": "c33ec3fce09c0971c32ddcbb86d9383ffbe4c6d05cf36f20460005e6547bb845", + "source375/code/complex/inputs/complex/sources/Work__GCert__Data__B2Gp193Main.lean": "cb61f304da51f1dd0a2ec25bca4b63eb095eeb2863289e1e2bdee7c82beff48b", + "source375/code/complex/inputs/complex/sources/Work__GCert__Data__Glue.lean": "d5314f2b93a7f0e1c949fb502331825bfc6d9d8762d35f865443e7c95b6c7ef7", + "source375/code/complex/inputs/complex/sources/Work__GCert__Data__InstB2Gp193.lean": "9587ddb9961f44938032b609307ab91c0b0e757e3991f1ad95480dd50fd4f72b", + "source375/code/complex/inputs/complex/sources/Work__GCert__Data__P193Cert.lean": "d92ee6889be4753fc99f467bd84039743325123a1165128378b9c906a04f2703", + "source375/code/complex/inputs/complex/sources/Work__GCert__Data__P193Price.lean": "0299bcd0fe255960eec682eef0f045f7e5cb1e4711af2aab4393526eae2caea3", + "source375/code/complex/inputs/complex/sources/Work__GCert__Data__P193ScalOK.lean": "479434815822e98f015e335361089c3788d00dc3dd39c2944f75410aa0c158fe", + "source375/code/complex/inputs/complex/sources/Work__GCert__Data__RateB2Gp193x.lean": "6b40cac1481c931d47b1a092e382d04716ede0e785c492a2f2983e886a257c3f", + "source375/code/complex/inputs/complex/sources/Work__GCert__Data__Raw.lean": "aba94a004c94dcae7cf3047c88a6da9561555f4ebe8ab92e299e6ce09ee7aa66", + "source375/code/complex/inputs/complex/sources/Work__GCert__Data__SolutionB2Gp193x.lean": "45c768c9d71a7cc18bd6db74cb036db880d89580ca60557bb4a492280296b169", + "source375/code/complex/inputs/complex/sources/Work__GFrame__Engine__Adapt.lean": "feec0a3828867968a5c7c2c30b86ed70449abc3c660a60ada67203a75bae2ef7", + "source375/code/complex/inputs/complex/sources/Work__GFrame__Engine__Letters.lean": "34906dbf5ae16b5174db00b4881a5cc1d2e583b8c8806db6523a5e2f86565f09", + "source375/code/complex/inputs/complex/sources/Work__GFrame__Engine__Level.lean": "80fb3daa9a45de0ed6da570eb4476b9104734be65d0116f58bcfcbcd67f771d0", + "source375/code/complex/inputs/complex/sources/tools__gx__ORIGIN.md": "6ba897a9495ddadcf8558b93133fdfaf66fc35ce7fa2c53e2d5667335c315e0b", + "source375/code/complex/inputs/complex/sources/tools__gx__gx.py": "6f3dc8bb639933227a8dae181ec4a542e85c7276be9c9e330f49518e7b630b95", + "source375/code/complex/inputs/complex/sources/tools__gx__gxbind.py": "9c9dcfac47f0535bf3aa8ebf7c662cdef0ebda50a9f0a9282b8f3cf34809f835", + "source375/code/complex/inputs/complex/sources/tools__gx__gxconv.py": "dab7fec9f44c2d368ed334055d7126e202017feb46e41a8d86e2d998720f67c2", + "source375/code/complex/inputs/complex/sources/tools__gx__gxcore.py": "eb972c06fe8c322db2d9a8d9a7d05596e8f40c4ca8e5f42eb6df3c7361b5d517", + "source375/code/complex/inputs/e8/LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "source375/code/complex/inputs/e8/NOTICE": "557c9ad4660eebd14a00583736c4d12d2c45f3fc9bc148845f9f3efec72c9434", + "source375/code/complex/inputs/e8/Work/GCert/Data/B2Ge8.lean": "842b217147cf84e8042d6ef1c33104d5444b6587b594664bc9eb89b237ab4ad0", + "source375/code/complex/inputs/e8/Work/GCert/Data/B2Ge8Main.lean": "987103107d5586c096016f0a702d0de35b74398dbb50ac66f5886a43a5ca0d05", + "source375/code/complex/inputs/e8/Work/GCert/Data/ChallengeB2Ge8x.lean": "a59db9d54b83adc73391916f7c1ef5e381ff073027781c26cb350f43b79839e3", + "source375/code/complex/inputs/e8/Work/GCert/Data/E8Cert.lean": "13a243c7d7be31ae429d19b5ecd5d428d60c41b7cca8a330f0c4179b110ba7ea", + "source375/code/complex/inputs/e8/Work/GCert/Data/E8Price.lean": "cd250dd72406dde37765c501f666ceeedcc18f831070b26369bcb154c1f99a8e", + "source375/code/complex/inputs/e8/Work/GCert/Data/E8ScalOK.lean": "6bd5e68effe8913a3f73e25ea59142cd9928ddf81e94250a6ea28aa7317388b3", + "source375/code/complex/inputs/e8/Work/GCert/Data/Gen/E8/S0.lean": "36de82f6969c23082876a4d6848428623d1c65d2df3fc917f23ecba003189dd2", + "source375/code/complex/inputs/e8/Work/GCert/Data/Gen/E8.lean": "5c7fb23df2c10b690f638a19bf066905b5b620b8a2ad0ffde76cc9348d8aa2b4", + "source375/code/complex/inputs/e8/Work/GCert/Data/Gen/E8End.lean": "6ea83365afe01664b2132a630511b4de65f938dc328744ce7f77a01fad97f32d", + "source375/code/complex/inputs/e8/Work/GCert/Data/Gen/E8Hist.lean": "cce81699abe1f85a870dcf64edd395d2cf5a586da7700af565b557093095ab51", + "source375/code/complex/inputs/e8/Work/GCert/Data/Gen/E8Par.lean": "a343219b419f30f8ac4dd3a0a98bf53550c5fec6b2cbd245320a95977c319016", + "source375/code/complex/inputs/e8/Work/GCert/Data/Gen/E8Scal0.lean": "78036e5443775ade5bde46a77ba3e0433fe22160da11b5b6c96c7f1075ecfbbd", + "source375/code/complex/inputs/e8/Work/GCert/Data/Gen/E8Seg0.lean": "f6b248dc4c3b2c94db95989b6bd5ad3c3f0d7ece3a511e5b69069550b821b138", + "source375/code/complex/inputs/e8/Work/GCert/Data/Gen/E8Seg1.lean": "79d16ccceb61391446ea97f77fddadafa9150e9dea97919e775f6c78daa71839", + "source375/code/complex/inputs/e8/Work/GCert/Data/Gen/E8SegF.lean": "924340aebc6f68b5a6526311ce33341af0a0a5a8375416762f08c1914ec08abe", + "source375/code/complex/inputs/e8/Work/GCert/Data/Gen/E8Tab0.lean": "650600b631a21221956f9abbab9abebcc9cca628512d3e9a017e2373e2649b17", + "source375/code/complex/inputs/e8/Work/GCert/Data/Gen/E8Tab1.lean": "60036fa4deeb19d39fc0dddf31359d2b6d2407ff66070f145b111bff16190eb0", + "source375/code/complex/inputs/e8/Work/GCert/Data/Gen/E8Tab2.lean": "c8a248da3eb770ba55ef267d118b29d49983311087ef789398d555e2c44b3a41", + "source375/code/complex/inputs/e8/Work/GCert/Data/Gen/E8Tab3.lean": "41975d430ec0095ad465a36d4903e90c01bc891d3abe5e2c372ef786c029a7ed", + "source375/code/complex/inputs/e8/Work/GCert/Data/Gen/E8YChk.lean": "a290360c175544cb85edffe1b92fcf7d447cba09128e19de8dc87e0a1ff0c524", + "source375/code/complex/inputs/e8/Work/GCert/Data/InstB2Ge8.lean": "c1fee298187ea19b5d70fcfccef7d4fd4161be70c0adda19a89ca9933a759954", + "source375/code/complex/inputs/e8/Work/GCert/Data/RateB2Ge8.lean": "7b6e59724c0f140e714afba237d5a1a91b22da70abc096ce274690140b39a3a6", + "source375/code/complex/inputs/e8/Work/GCert/Data/RateB2Ge8x.lean": "7c56d865ed6bfcb6919dabc1a6e53f8744ff4824a2f78335787485f3090970d1", + "source375/code/complex/inputs/e8/Work/GCert/Data/SolutionB2Ge8x.lean": "dd52f1fe0a372480edaf5e6c64903d6257c410e43d406f8acb6bf8f60a1ee28f", + "source375/code/complex/inputs/e8/comparator/B2Ge8x.json": "ddad06c37f9268986f3ec8ce43da5230ee2bd887da2480328413a0dc58f2a926", + "source375/code/complex/inputs/e8/tools/certificate/gcert1-e8-r783.json.gz": "4b92f00fc7454b9b15e6d71a3b05062792eacca0a0ca4efee46f87827d57c8aa", + "source375/code/complex/inputs/e8/tools/e8/replay.py": "be41ee310f28121c3e424cc8637d8fa02ef7c47fc8945e9bbd3856138fd800d6", + "source375/code/complex/inputs/e8/tools/gen/foldgen.py": "a0f16e2c9e078ffbfb2174281ee93a48c18593aefb880318fc105ec85a205932", + "source375/code/complex/inputs/e8/tools/gen/foldlib.py": "7a3c38a698c129e13a767da75926a1305eb0c031b908450afc6feb185505c59a", + "source375/code/complex/inputs/e8/tools/gen/gen_rates.py": "ef8c869e4cf8da33a4c10b96f7f6faafd46e15d66766238070a60315aa169994", + "source375/code/complex/inputs/e8/tools/gen/gen_sharp.py": "1b5eb3730cb16cf516e760879951fdfb9b065efc55f78c29a5c6404fcca57a78", + "source375/code/complex/inputs/e8/tools/gen/templates/ChallengeB2L16x.lean.txt": "0488b7a2442c795414f103df912d1e6cc66d37b5be270940ea9564b7f2b666be", + "source375/code/complex/inputs/e8/tools/gen/templates/SolutionB2L16x.lean.txt": "d414a890dfe126916374c1afc804b90e5081b7760f894b9ccdcf23d83a12f9ee", + "source375/code/complex/inputs/e8/tools/gx/gsmirror.py": "0e22bbe5924284e2fb916337ccefc8e41f6e54469749986ad15b3b81cfaec534", + "source375/code/complex/inputs/e8/tools/gx/gxbind.py": "9c9dcfac47f0535bf3aa8ebf7c662cdef0ebda50a9f0a9282b8f3cf34809f835", + "source375/code/complex/inputs/e8/tools/gx/gxcore.py": "eb972c06fe8c322db2d9a8d9a7d05596e8f40c4ca8e5f42eb6df3c7361b5d517", + "source375/code/complex/inputs/e8/tools/gx/gxgen.py": "ce9151054370c2210ed08f54c249a19dcb6946d182cdf934dee1a3781b53040f", + "source375/code/complex/inputs/e8/tools/gx/gxpaths.py": "f00802d48ef3fedb00278f0b1c7bde074cc49dd30f202d7f32a9d2aebb3be443", + "source375/code/complex/inputs/e8/tools/gx/gxrate.py": "514a5719f970fe36b1273cf59df0396db0e042dd7864c2eea53ab2a2fd1e2ad6", + "source375/code/complex/inputs/e8/tools/gx/gxunit.py": "3cc09a9c1a2db681c0f2016bc821af5b674d34834dbd6f195b9d482ce7c0ff58", + "source375/code/complex/inputs/e8/tools/gx/regen_check.py": "b6172d58749c0b3b9138570c74827bcb23bf5db4ff9643740768cd7782ac4ca6", + "source375/code/complex/inputs/e8/tools/gx/regen_check_e8.py": "ad8fe9811c6ea0d89c795caef48686cfca600f5d540ebfd5d1251d6777cec7cf", + "source375/code/complex/pins-e8-b3.json": "9e2d5b8e1f5f5d1c3113ed563ace88a3e5a605e1f053af350f1cec4d4791a4c4", + "source375/code/complex/pins-e8-b3h.json": "bffda4be2ef3ba7a1072029779cfa448e3d19a986eae444c7970b87f48b294c6", + "source375/code/complex/pins-e8.json": "bf66f785878f636616ceab193e5a222143945ea06fc2f13dfb99b204ebba82ff", + "source375/code/complex/portable_complex.py": "a28cfd37ce5da0e97e03f225629f17f31e0278142b3757345ed47d7a66560cbf", + "source375/code/pricing/base_two_moment.py": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098", + "source375/code/pricing/moment.py": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482", + "source375/code/pricing/outer.py": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c", + "source375/code/pricing/prime_witnesses.py": "98cd03bc9582e7bd0ab194c191ea8eea940539e510051443ab9fd3e572a364ab", + "source375/code/provenance.py": "e509d08cd82d078df86f491f83a312516cae26c5528ad073b924c73f53b34edd", + "source375/data/bit/RECORD-SHA256SUMS": "cfc30216f441a1c44a533f2f26954f90e454136af8842c497de4e2da9bd32d8d", + "source375/data/bit/bitE8-r865.json.gz": "1fb726ea3818fe0837cceb0dd22a71a0814f064e5e781628104610d6468e0e55", + "source375/data/regression-p10/BASE-RECORDS.bin.gz": "caabc13126e8f87d08f7697f51512cb3431ff52861f4190149251d8e19224430", + "source375/data/regression-p10/BASE-frames.json.gz": "35070b83d12ebc60003ed344315328713134a43bdb04217c2c5cbc39e101391f", + "source375/data/regression-p10/BASE-states.json.gz": "1e37ae5001447dd78a8287d8aa23d73a1d5862c4017f44db49af327f58d7cf22", + "source375/data/regression-p10/receipts-loans/banks.json.gz": "0bd464f873b0f59622026793affb308bf087833de6f3197202adc7a36d9d0782", + "source375/data/regression-p10/receipts-loans/finite.json.gz": "82b21b4e6bb4b20e0ecbca44f59941362f57a26a019f179e19b5b7b86262a116", + "source375/data/regression-p10/receipts-loans/global_result.json.gz": "7dccea4b8c4a81597779dc0944297d5f60efd9e2e5b19469417712e2192c6cca", + "source375/data/regression-p10/receipts-loans/math.json.gz": "c4074b86171c5bde8fbbff6df0022a116f17e11f0d2116ae3dfe75c8b2a18c64", + "source375/data/regression-p10/receipts-loans/raw.json.gz": "505c13c667230e946e708d7c9086de34d1c5e259a557f6685765054001e29981", + "source375/data/regression-p10/receipts-loans/scalar.json.gz": "e7bb691b741227ce389ff6341fa0548ff8f638cc492a06be40fcd829fac0bed9", + "source375/requirements.txt": "1939ad706e192fb3781e8a0018880b1c6291ded07d40edc4048ab1a0e48f71ee", + "source375/verify.sh": "f00ebcfa36f95e45b79b636c826cc8a390a3e4b724b24644231014c8d74a5663", + "support/bits/stdc++.h": "51908262576163a64815def96ff39b62aef3d52daaad9c561505c4293ff88e18", + "verify.py": "619ad7823f4becf0be93fd1885861069179d67e8ba8fcf87f541cf13f3ac32f7" +} diff --git a/research/e8-seven-stage-coupled-retiming/NOTICE.md b/research/e8-seven-stage-coupled-retiming/NOTICE.md new file mode 100644 index 0000000000..e9d4201826 --- /dev/null +++ b/research/e8-seven-stage-coupled-retiming/NOTICE.md @@ -0,0 +1,14 @@ +# Attribution and provenance + +New composition and orchestration: Rohan, with substantial OpenAI Codex assistance. Apache-2.0. + +All `source375/` files are unchanged from CrocSwap/integer-mult-bounds PR375 at +`79874623cf86d92325c26ccafc31413d12e9d248`, package `research/e8-seven-stage-halving-two`. +All `source365/` files are unchanged from PR365 at +`a22270515e9c6102dda3b22e75ca2c62e82812ff`, package `research/e8-coupled-retiming`. +Their original licenses, notices, source pins and proof-scope limitations remain included. +The macOS standard-header compatibility file is from PR364 at the commit and path recorded in SOURCES.json. + +Principal upstream authors: Jacob Sussman (E8 complex circuit and proof framework), Dylan Crow / utcorvusvolat-dotcom (E8 bit word, with Anthropic Claude assistance), DaysSky (seven-stage extension, composition and degree-two guard, with Anthropic Claude assistance), Ali Romman / aliromman (coupled complex retiming, with OpenAI Codex assistance), and the exact-pricing/assembly authors credited in source375/NOTICE.md and NOTICE-PR352.md. + +This package neither claims authorship of those results nor claims that their inherited assumptions have been discharged. Original Lean-data regeneration is a baseline check only; the retimed circuit has not been compiled in Lean here. diff --git a/research/e8-seven-stage-coupled-retiming/README.md b/research/e8-seven-stage-coupled-retiming/README.md new file mode 100644 index 0000000000..d81d60384a --- /dev/null +++ b/research/e8-seven-stage-coupled-retiming/README.md @@ -0,0 +1,60 @@ +# Seven-stage E8 with the coupled complex retiming + +Combining PR365's four coupled frame changes with PR375's seven-stage construction raises the conditional integer-multiplication saving to + +**κ = 954395132518163 / 1000000000000000000 = 0.000954395132518163.** + +This is approximately **0.01588% above PR375** at commit `79874623cf86d92325c26ccafc31413d12e9d248`. The bit word, its seven-stage layout, replica count, banks, and finite bill are unchanged. The improvement comes from applying PR365's already checked complex circuit to the seven-stage complex supplier. This package claims that composition, not a new E8 word or new retiming discovery. + +| Quantity | PR375 baseline | Composition | +|---|---:|---:| +| Complex coarse saving b, denominator 10^18 | 955155017966616 | 955306874505079 | +| Bit coarse saving c, denominator 10^18 | 968197503705007 | unchanged | +| Final κ, denominator 10^18 | 954243565681330 | 954395132518163 | +| Complex recursive calls in seven stages | 29498 | 29491 | +| Complex rank mass | 94473 | unchanged | +| Complex width / live normalization | 63 / 1503 | unchanged | +| Complex deficit / maximum child | 216 / 38 | unchanged | +| Complex scalar primitive steps, forward / backward | 68158 / 72856 | unchanged | + +The complex side still binds. As in PR375, the complex idle climbs remain unsplit, with maximum child 38 at width 63. The guard charges halving degree two: `63^2 > 2*38^2`, physical row coefficient `2*1903 + 9909 + 252 = 13967 < 20161`, and completed-child induction gap `49*B`. These quantities are unchanged by the retiming. The exact difference in κ is `151566836833 / 1000000000000000000`. + +## Replay + +Requires Python 3.11 or later, NumPy, SymPy, mpmath, a C++17 compiler, Boost headers, Bash, and `sha256sum`: + +```sh +python -m pip install -r research/e8-seven-stage-coupled-retiming/requirements.txt +python -B research/e8-seven-stage-coupled-retiming/verify.py /path/to/fresh/output +``` + +The output must be outside the package and not already exist. On macOS with Homebrew Boost, add `--boost-include /opt/homebrew/include`. Temporary files stay beneath the supplied output. Allow several minutes and at least 200 MB of available output space. + +The verifier first runs the entire pinned PR375 replay, including its producer reconstruction, native all-column checks, negative controls, geometry, banks, finite bills, five-stage regressions and original complex supplier. It then runs PR365's reconstruction and complete rational scalar-map comparison, binds its source certificate to PR375's original certificate, and checks the retimed circuit through PR375's complex B3 label, scalar, splice and precision checkers with frozen new pins. Neither vendor tree is edited. + +Both exact rational moment engines prove the new complex saving and reject the adjacent 10^-18 grid point. The unchanged bit certificate is repriced with that supplier; all 47 strict outer constraints hold and the next κ grid point is rejected. The resulting finite bit bill must equal the baseline receipt. `RESULT.json` is written only after all checks pass. Expected results are comparison targets, not substitutes for replay. + +The full original Bash replay receives a small transport adapter for paths containing spaces and for the chosen Python interpreter. It retains every original scientific check. A standard-header compatibility file supports macOS Clang. `SOURCES.json` pins both source PRs and that header; `MANIFEST.json` binds every shipped file. All source notices remain in the vendor trees. + +## Why the cost decreases + +PR365 independently checks the one-invocation histogram delta + +``` +rank: 1 2 3 4 5 6 +count: +2 -6 +4 +1 -6 +4 +``` + +It is a positive weighted sum of second differences of `x^p`, with weights `(1,4,1,2,4)` and `0^p=0`. For `0
=2.0,<3
+sympy==1.14.0
+mpmath==1.3.0
diff --git a/research/e8-seven-stage-coupled-retiming/source365/NOTICE.md b/research/e8-seven-stage-coupled-retiming/source365/NOTICE.md
new file mode 100644
index 0000000000..8bbad70301
--- /dev/null
+++ b/research/e8-seven-stage-coupled-retiming/source365/NOTICE.md
@@ -0,0 +1,78 @@
+# Attribution and scope of new work
+
+Jacob Sussman supplied the E8 label family, circuit, scatter, frame scheduler,
+checkers, price routines, and general proof framework in
+`jacobalansussman/wht-power-saving-lean`, commit
+`9c94857bbaee886f8649edee0bc2d3c738f9555e`.
+
+`data/original.json.gz` is an unchanged copy from that commit. The new
+certificate derives from that file. This package uses the repository's
+[Apache-2.0 license](../../LICENSE). The source notices that apply to the
+retained certificate are copied below.
+
+DaysSky's CrocSwap PR352 supplies the connection to the complex branch and the
+exact coarse-moment convention used here. Its commit
+`04b4c3c478b5bd8797d2663d89d8db4dfd0ad9f2`, source paths, and hashes are
+recorded in `sources.json`. Prior frame-retiming contributions
+include CrocSwap PR328 and PR350. No claim of priority for the general method is
+made.
+
+The new work consists of four explicit frame changes, a deterministic
+generator, independent scalar and frame checks, exact rational cost bounds,
+and the short cost proof. OpenAI Codex and its research agents supplied
+substantial assistance. New contributions are
+offered under the repository's Apache-2.0 license.
+
+Attribution does not imply review or endorsement by the credited authors.
+
+## Upstream notice excerpts
+
+The following text is copied from the copyright header and sections 4 and 8
+of the [upstream NOTICE](https://github.com/jacobalansussman/wht-power-saving-lean/blob/9c94857bbaee886f8649edee0bc2d3c738f9555e/NOTICE).
+References within these excerpts refer to that source repository.
+
+```text
+Walsh-Hadamard power saving (wht-power-saving-lean)
+Copyright 2026 Jacob Sussman
+
+Repository: https://github.com/jacobalansussman/wht-power-saving-lean
+
+4. How the new files were made.
+ Jacob Sussman made the new files on 2026-10-08, 2026-10-09 and 2026-10-10
+ by directing a team of AI agents (Claude). The agents wrote the new Lean
+ files, the certificate data and the generator scripts. They made the
+ rebuild scripts under tools/rebuild/, in part by adapting programs of
+ CrocSwap/integer-mult-bounds (section 6): ten of the thirteen on
+ 2026-10-09, tidied for this repository on 2026-10-10, and three on
+ 2026-10-10. On 2026-10-10 they also wrote the search programs under
+ tools/e8/ and found with them the certificate of the fourth result
+ (section 8). See README.md, section 4.
+
+8. The certificate of the fourth result and the search programs.
+ tools/certificate/gcert1-e8-r783.json.gz, the Lean data modules
+ generated from it (Work/GCert/Data/Gen/E8*.lean, Work/GCert/Data/Gen/E8/
+ and the modules of Work/GCert/Data/ with E8 or B2Ge8 in their names) and
+ the Python programs under tools/e8/ were made by the agents for this
+ repository on 2026-10-10 (section 4). The circuit in that certificate
+ is not the circuit of section 6, and no data file of
+ CrocSwap/integer-mult-bounds was loaded to make it. It uses three
+ devices that were published by others in pull requests to that
+ repository:
+ - the in-place pair, a + b and a - b formed on the two arrays that held
+ a and b: icekylinx (#184), carried in #191 and #193 (ikeboy);
+ - the re-use of a finished helper with a compensating read: jamesyc
+ (#124) and eumemic (#143);
+ - the late pairing rule, the choice of which finished helper a new
+ value takes: Chafik Boukhalfa (the account chafreaky), #200 and #233,
+ and pull request #2 of this repository. The search programs apply the
+ idea with a greedy rule of their own; his program, his pairs and his
+ certificate were not used.
+ No program of that repository is included in tools/e8/, imported or
+ run by it. The programs of tools/e8/ have not been compared statement
+ by statement with the programs of that repository, as those of
+ tools/rebuild/ were (section 6). The integer programme of
+ tools/e8/ is solved with the open-source solver HiGHS, called through
+ SciPy (scipy.optimize.milp), with NumPy; none of the three is included
+ here. The credits, with links, are in README.md ("Whose ideas the new
+ unit uses") and in RELATED-WORK.md, section 8.
+```
diff --git a/research/e8-seven-stage-coupled-retiming/source365/PROOF.md b/research/e8-seven-stage-coupled-retiming/source365/PROOF.md
new file mode 100644
index 0000000000..332d30c265
--- /dev/null
+++ b/research/e8-seven-stage-coupled-retiming/source365/PROOF.md
@@ -0,0 +1,170 @@
+# Four E8 frame changes
+
+All gate and register indices below are zero-based indices in the original
+certificate. Binary frames are given by integer bit masks. The new certificate
+has uncompressed SHA-256
+`3191011e0cb189665c8e0a9b97137dbed50241a0704c8be01c11b1b5a9518fc2`.
+
+## Circuit changes
+
+1. Remove `helper388 -= source64` and `helper771 += source64` from A65.
+ Insert those two additions just before A187, at frame 285 with basis
+ `[196,56]`. No gate A66 through A186 touches any of these three registers.
+ Source 64 has label 56.
+2. Remove `helper693 += source98` and `helper839 -= source98` from A100.
+ Insert those two additions just before A198, at frame 296 with basis
+ `[257,243,14]`. No gate A101 through A197 touches any of these three
+ registers. Source 98 has label 253, and `253 = 243 XOR 14`.
+3. In B193, B916, and B917, replace frame 599, with basis
+ `F=[276,148,84,51,15]`, by `G=[256,128,64,39,20,15]`.
+ These gates add helper807 to helper766, distribute plus or minus half of
+ helper807 to targets149 and155, and add helper766 to helper807.
+4. In B873 and B874, replace frame 585, with basis `[161,81,9,5,3]`,
+ by `[305,161,81,9,5,3]`. The first gate adds half of helper550 to target198
+ and subtracts half of helper550 from target202. The second gate adds
+ helper521 to helper550.
+
+The first two changes move additions only across gates that touch disjoint
+registers. Such scalar operations commute, for all initial register values.
+Neither change crosses the scatter. The last two changes keep all scalar
+operations and their order. Thus the complete scalar operator and the retained
+totals at scatter stay the same. The verifier also compares the complete
+1023-by-1023 rational scalar matrices.
+
+All paths remain nested. The verifier checks actual binary subspace inclusion,
+not only dimensions. For the third change, `G=F+span(256)` has dimension six.
+The identities
+
+```
+276 = 256 XOR 20
+148 = 128 XOR 20
+84 = 64 XOR 20
+51 = 39 XOR 20
+```
+
+show that F is contained in G. The preceding helper frames are contained in F.
+The next helper frames are
+
+```
+helper766: [256,128,64,37,20,13,2]
+helper807: [256,128,64,38,20,14,1]
+```
+
+They contain G because `39=37 XOR 2=38 XOR 1` and
+`15=13 XOR 2=14 XOR 1`. The final target frames also contain G:
+
+```
+target149: [256,128,64,32,18,8,6,1]
+target155: [256,128,64,34,16,10,4,1]
+```
+
+For target149, use `39=32 XOR 6 XOR 1`, `20=18 XOR 6`, and
+`15=8 XOR 6 XOR 1`. For target155, use `39=34 XOR 4 XOR 1`,
+`20=16 XOR 4`, and `15=10 XOR 4 XOR 1`.
+
+For the fourth change, let `F=span(161,81,9,5,3)` and
+`G=F+span(305)`. These frames have dimensions five and six. All preceding
+frames are contained in F. The next frame of helper521 is
+`span(257,145,81,48,9,5,3)`. The next frame of helper550 and both targets is
+`span(304,160,80,8,4,2,1)`. Both contain F. They contain the added vector
+because `305=257 XOR 48=304 XOR 1`. Thus both contain G, and the paths
+remain nested.
+
+## Child ranks
+
+Each climb contributes a child whose rank is the increase in frame dimension.
+The four changes affect disjoint sets of registers. Thus their histogram
+differences add.
+
+| Change | Register | Old child ranks | New child ranks |
+| --- | --- | --- | --- |
+| 1 | source64 | 5,3 | 1,4,3 |
+| 1 | helper388 | 1,1,2,2,3 | 2,2,2,3 |
+| 1 | helper771 | 1,1,1,3,1,2 | 2,1,3,1,2 |
+| 2 | source98 | 5,3 | 2,3,3 |
+| 2 | helper693 | 1,2,1,5 | 3,1,5 |
+| 2 | helper839 | 1,2,1,2,1,1,1 | 3,1,2,1,1,1 |
+| 3 | helper766 and helper807, each | 3,2,2,1,1 | 3,3,1,1,1 |
+| 3 | target149 and target155, each | 5,3 | 6,2 |
+| 4 | target198 and target202, each | 5,2,1 | 6,1,1 |
+| 4 | helper521 | 2,1,2,2,1,1 | 2,1,2,1,1,1,1 |
+| 4 | helper550 | 2,1,2,2,2 | 2,1,3,1,2 |
+
+The combined invocation histogram difference is
+
+```
+rank: 1 2 3 4 5 6
+change: +2 -6 +4 +1 -6 +4
+```
+
+Its rank mass is zero and its child count is minus one. Copy cost remains 72.
+The five-stage histogram is five times the invocation histogram, plus 240
+children at each rank 4, 8, 16, and 20. Therefore its rank mass remains 56,715,
+with dimension m=45, stock W=1263, and deficit mW-56715=120.
+
+## Strict cost inequality
+
+Let a be a saving, with 0 1
+M_candidate(876412559609473 / 10^18) < 1
+M_candidate(876412559609474 / 10^18) > 1.
+```
+
+The logarithm uses the atanh series with a positive geometric tail bound.
+Arguments are reduced to [1,2]. The exponential uses a Taylor polynomial of degree 20 with
+a geometric tail bound. All arithmetic in these enclosures is rational.
+Decimals in the saved result are only displays of the proved margins.
+
+## Limits
+
+This proves the finite circuit and recursive-cost improvement under the
+stated convention. The general frame-transfer and recursion theorems remain
+dependencies. A complete scalar identity is not a proof of the tape compiler
+or the integer-multiplication assembly. No global optimum or larger final
+integer-multiplication saving is claimed.
+
+The local verifier checks the finite rational circuit, its frame paths, and
+the stated moment. It does not run the upstream checkers or their Lean
+representation checks for separate positive and negative parts and digit
+limits. The disjoint operations in the first two changes commute in those
+representations as well: each moved addition crosses only operations on other
+registers. The last two changes leave the scalar operations in place. This
+preserves the scalar computation from the pinned baseline; it does not replace
+a build of new Lean data.
diff --git a/research/e8-seven-stage-coupled-retiming/source365/README.md b/research/e8-seven-stage-coupled-retiming/source365/README.md
new file mode 100644
index 0000000000..50593e7050
--- /dev/null
+++ b/research/e8-seven-stage-coupled-retiming/source365/README.md
@@ -0,0 +1,80 @@
+# E8 complex cost from four coupled frame changes
+
+This package changes Jacob Sussman's E8 circuit at commit
+`9c94857bbaee886f8649edee0bc2d3c738f9555e`. It gives a smaller recursive moment with
+the same 783 helpers, copy cost 72, rank mass 56,715, and deficit 120.
+
+| Quantity | Original | Candidate |
+| --- | ---: | ---: |
+| Conditional complex saving under PR352's fallback convention | 876248285600677 / 10^18 | 876412559609473 / 10^18 |
+| Children in one invocation | 3974 | 3973 |
+| Children in five stages | 20830 | 20825 |
+| Scalar additions, including scatter | 3876 | 3876 |
+
+The conditional saving increases by about 0.01875%.
+
+Four phase-A additions move to two later frames. Two sets of phase-B gates use
+larger frames. The original frame table gains two entries. All scalar coefficients,
+retained totals, and scatter coefficients stay the same. The complete rational
+scalar operator also stays the same, including its dependence on every initial
+helper value.
+
+[PROOF.md](PROOF.md) gives the exact edits and a strict cost inequality for every
+saving between zero and one. It does not rely on the approximate moment root.
+
+## Reproduce
+
+From the repository root, run:
+
+```sh
+python3 -B research/e8-coupled-retiming/verify.py
+```
+
+The script uses Python and its standard library. It checks source hashes,
+rebuilds the candidate, checks every frame path, reconstructs the scalar source
+map and histogram, and compares all 1,046,529 entries of the complete scalar maps.
+A coefficient identity checks the
+strict-concavity proof for the full saving interval. Exact rational bounds prove both
+reported savings. In each case the next 10^-18 grid point fails. Four damaged
+inputs must fail for their stated reasons.
+
+To write the candidate to another file, run:
+
+```sh
+python3 -B research/e8-coupled-retiming/retime.py /tmp/e8-retimed.json.gz
+```
+
+The saved verification result is `verification.json`. Run the script to obtain
+a fresh result; the script does not use that saved result as an input.
+
+## Scope
+
+This is a finite complex-circuit improvement. It does not change the selected
+integer-multiplication result, the bit circuit, or its saving.
+
+The new certificate has not been compiled in Lean. The original certificate's
+Lean data and theorem do not certify this changed file. A formal extension must
+generate and compile new data. The general frame-transfer, helper cleanup,
+recursive construction, and multiplication assembly remain inherited
+dependencies. The complete scalar-map comparison does not prove those steps.
+The script does not run the upstream checkers or their Lean representation
+checks for separate positive and negative parts and digit limits.
+
+## Source and search
+
+The baseline is Sussman's `tools/certificate/gcert1-e8-r783.json.gz`. The exact
+commit and original-data hash are in `sources.json`. The E8 complex
+connection and fallback convention follow CrocSwap PR352 at
+`04b4c3c478b5bd8797d2663d89d8db4dfd0ad9f2`. The exact reference paths and
+hashes are recorded as mathematical provenance in `sources.json`; those files
+are not imported or run. Earlier retiming
+work includes Sussman's `tools/e8/sched.py` and CrocSwap PR328 and PR350.
+This package supplies a new E8 witness; it does not claim to invent retiming.
+
+The candidate came from bounded searches over pairs of moves and common
+intermediate frames. Frames came from existing stops and their joins or
+intersections. A later search moved two more complete gates to one common
+intermediate frame. These searches do not establish
+global optimality. The search is not needed to reproduce or verify the witness.
+
+See [NOTICE.md](NOTICE.md) for attribution and AI assistance.
diff --git a/research/e8-seven-stage-coupled-retiming/source365/data/original.json.gz b/research/e8-seven-stage-coupled-retiming/source365/data/original.json.gz
new file mode 100644
index 0000000000..0bd0bacf74
Binary files /dev/null and b/research/e8-seven-stage-coupled-retiming/source365/data/original.json.gz differ
diff --git a/research/e8-seven-stage-coupled-retiming/source365/data/retimed.json.gz b/research/e8-seven-stage-coupled-retiming/source365/data/retimed.json.gz
new file mode 100644
index 0000000000..efdb76ecf3
Binary files /dev/null and b/research/e8-seven-stage-coupled-retiming/source365/data/retimed.json.gz differ
diff --git a/research/e8-seven-stage-coupled-retiming/source365/reconstruct.py b/research/e8-seven-stage-coupled-retiming/source365/reconstruct.py
new file mode 100644
index 0000000000..9cefd8ec9d
--- /dev/null
+++ b/research/e8-seven-stage-coupled-retiming/source365/reconstruct.py
@@ -0,0 +1,226 @@
+"""Check the E8 scalar map, frame paths, and recursive cost from one certificate.
+
+This file uses only the Python standard library. It imports no supplier code.
+The checks do not prove the all-size tape compiler or the multiplication theorem.
+"""
+
+import argparse
+from collections import Counter
+from fractions import Fraction as Q
+from functools import lru_cache
+import gzip
+import hashlib
+import json
+from pathlib import Path
+
+
+def require(condition, message):
+ if not condition:
+ raise ValueError(message)
+
+
+def add(row, source, coefficient):
+ for key, value in source.items():
+ increment = coefficient * value
+ require(6 % increment.denominator == 0, "Scalar increment is not in sixths")
+ result = row.get(key, Q(0)) + increment
+ if result:
+ row[key] = result
+ else:
+ row.pop(key, None)
+
+
+def elements(basis):
+ result = {0}
+ for vector in basis:
+ require(vector not in result, "Dependent frame basis")
+ result |= {x ^ vector for x in result}
+ return frozenset(result)
+
+
+@lru_cache(None)
+def logarithm(ratio):
+ def small(value):
+ t = (value - 1) / (value + 1)
+ total = Q(0)
+ power = t
+ terms = 80
+ for j in range(terms):
+ total += 2 * power / (2 * j + 1)
+ power *= t * t
+ tail = 2 * power / ((2 * terms + 1) * (1 - t * t))
+ return total, total + tail
+
+ exponent = 0
+ while ratio >= 2:
+ ratio /= 2
+ exponent += 1
+ lo, hi = small(ratio)
+ a, b = small(Q(2))
+ return lo + exponent * a, hi + exponent * b
+
+
+def exponential(value):
+ require(0 <= value < 1, "Exponential bound requires an argument below one")
+ total = term = Q(1)
+ for j in range(1, 21):
+ term *= value / j
+ total += term
+ tail = term * value / 21 / (1 - value / 22)
+ return total, total + tail
+
+
+def moment(histogram, dimension, stock, saving, fallback=True):
+ lo = hi = Q(0)
+ terms = {rank: Q(count) for rank, count in histogram.items()}
+ if fallback:
+ terms[1] = terms.get(1, Q(0)) + Q(
+ 32 * dimension * dimension * sum(histogram.values()), 10**16
+ )
+ for rank, count in terms.items():
+ a, b = logarithm(Q(dimension, rank))
+ lower = exponential(saving * a)[0]
+ upper = exponential(saving * b)[1]
+ weight = count * rank / (dimension * stock)
+ lo += weight * lower
+ hi += weight * upper
+ return lo, hi
+
+
+def reconstruct(c):
+ require(c["format"] == "gcert/1", "Certificate format")
+ h, v, helpers = c["h"], c["v"], c["R"]
+ require((h, v) == (9, 120), "This audit is for the E8 label family")
+ require(not c["ext"], "Exterior gauges are outside this audit")
+ ports = c["ports"]
+ require(len(ports) == v and set(ports) == {p for p in range(512) if p.bit_count() in (3, 7)}, "E8 ports")
+ require(c["frames"][0] == [] and c["frames"][1] == [1 << i for i in range(h - 1, -1, -1)], "Frame endpoints")
+ for basis in c["frames"]:
+ require(all(0 < vector < 512 for vector in basis), "Frame outside ambient space")
+ pivots = [vector.bit_length() - 1 for vector in basis]
+ require(pivots == sorted(set(pivots), reverse=True) and all(
+ not (vector >> pivot & 1)
+ for i, vector in enumerate(basis) for j, pivot in enumerate(pivots) if i != j
+ ), "Noncanonical frame basis")
+ spaces = [elements(f) for f in c["frames"]]
+ dimensions = [len(f) for f in c["frames"]]
+ require(len(set(spaces)) == len(spaces), "Duplicate frame spaces")
+ require(all(all(0 <= x < 512 for x in s) for s in spaces), "Frame outside ambient space")
+ total = 2 * v + helpers
+ require(len(c["start"]) == len(c["final"]) == total, "Endpoint count")
+ require(all(0 <= frame < len(spaces) for frame in c["start"] + c["final"]), "Endpoint frame index")
+ current = list(c["start"])
+ rows = [{i: Q(1)} if i < v else {} for i in range(total)]
+ by_role = {kind: Counter() for kind in "xysc"}
+ allowed = {("x", "s"), ("s", "s"), ("s", "y"), ("x", "y"), ("x", "x")}
+
+ def kind(register):
+ return "x" if register < v else "y" if register < 2 * v else "s"
+
+ def climb(register, frame):
+ previous = current[register]
+ require(spaces[previous] <= spaces[frame], "A frame path is not nested")
+ if previous != frame:
+ by_role[kind(register)][dimensions[frame] - dimensions[previous]] += 1
+ current[register] = frame
+
+ for i, port in enumerate(ports):
+ require(spaces[current[i]] == {0, port}, "Source start")
+ require(spaces[c["final"][i]] == frozenset(range(512)), "Source final")
+ require(spaces[current[v + i]] == {0}, "Target start")
+ require(spaces[c["final"][v + i]] == {x for x in range(512) if (x & port).bit_count() % 2 == 0}, "Target final")
+ for i in range(2 * v, total):
+ require(spaces[current[i]] == {0} and len(spaces[c["final"][i]]) == 512, "Helper endpoints")
+
+ def run(gates, phase):
+ for gate in gates:
+ require(gate[0] in ("in", "out") and len(gate) == (5 if gate[0] == "out" else 4), "Unsupported gate")
+ tag, frame, pivot, terms = gate[:4]
+ require(0 <= frame < len(spaces), "Gate frame index")
+ spectators = gate[4] if tag == "out" else []
+ registers = [pivot] + [r for r, _, _ in terms] + spectators
+ require(len(set(registers)) == len(registers), "Aliased gate ports")
+ require(all(0 <= r < total for r in registers), "Register outside circuit")
+ require(phase == "B" or all(kind(r) != "y" for r in registers), "Early target operation")
+ for register in registers:
+ climb(register, frame)
+ for register, numerator, denominator in terms:
+ target, source = (pivot, register) if tag == "in" else (register, pivot)
+ require((kind(source), kind(target)) in allowed, "Unsupported scalar direction")
+ require(phase == "B" or (kind(source), kind(target)) in {("x", "s"), ("s", "s")}, "Unsupported phase-A scalar direction")
+ require(denominator > 0, "Coefficient denominator")
+ add(rows[target], rows[source], Q(numerator, denominator))
+
+ run(c["A"], "A")
+ retained = c["ret"]
+ require(sorted(k for k, _, _ in retained) == list(range(len(retained))), "Retained total indices")
+ totals = {}
+ for k, register, frame in retained:
+ require(2 * v <= register < total and current[register] == frame, "Retained total frame")
+ totals[k] = dict(rows[register])
+ by_role["c"][dimensions[frame]] += 1
+ require(all(spaces[current[v + i]] == {0} for i in range(v)), "Target moved before scatter")
+ require(len(c["scat"]["table"]) == v, "Scatter size")
+ for target, entries in enumerate(c["scat"]["table"]):
+ for k, numerator, denominator in entries:
+ require(k in totals and denominator > 0, "Scatter entry")
+ add(rows[v + target], totals[k], Q(numerator, denominator))
+ run(c["B"], "B")
+ require(all(rows[i] == {i: Q(1)} and rows[v + i] == {i: Q(1)} for i in range(v)), "Clean-source scalar identity")
+ for i, frame in enumerate(c["final"]):
+ climb(i, frame)
+ recorded = {kind: {int(r): n for r, n in hist.items()} for kind, hist in c["blocks"].items()}
+ require(by_role == recorded, "Recorded histogram differs from actual paths")
+ invocation = sum(by_role.values(), Counter())
+ copy_cost = sum(rank * count for rank, count in by_role["c"].items())
+ require(copy_cost == c["cst"], "Copy cost")
+ mass = sum(rank * count for rank, count in invocation.items())
+ require(mass == c["N"] == helpers * h + 2 * v * (h - 1) + copy_cost, "Telescoping rank identity")
+ histogram = Counter({rank: 5 * count for rank, count in invocation.items()})
+ for rank in (h - 1, 2 * h - 2, 2 * h + 2, 4):
+ histogram[rank] += 2 * v
+ dimension, stock = 5 * h, 4 * v + helpers
+ deficit = dimension * stock - sum(rank * count for rank, count in histogram.items())
+ require(deficit == 4 * v - 5 * copy_cost, "Five-stage deficit")
+ return {
+ "h": h, "v": v, "helpers": helpers, "frames": len(spaces),
+ "source_columns": v, "copy_cost": copy_cost,
+ "invocation_histogram": dict(sorted(invocation.items())), "invocation_mass": mass,
+ "m": dimension, "W": stock, "histogram": dict(sorted(histogram.items())),
+ "rank_mass": dimension * stock - deficit, "deficit": deficit,
+ "scope": "Exact scalar source columns and frame paths. The general dirty and frame transfer theorems remain dependencies. No tape compiler or Lean build is checked.",
+ }
+
+
+def main():
+ parser = argparse.ArgumentParser()
+ parser.add_argument("certificate", type=Path)
+ parser.add_argument("--saving", default="876248285600677/1000000000000000000")
+ parser.add_argument("--output", type=Path)
+ args = parser.parse_args()
+ blob = args.certificate.read_bytes()
+ raw = gzip.decompress(blob) if blob[:2] == b"\x1f\x8b" else blob
+ result = reconstruct(json.loads(raw))
+ result["source_sha256"] = hashlib.sha256(raw).hexdigest()
+ saving = Q(args.saving)
+ lower, upper = moment(result["histogram"], result["m"], result["W"], saving)
+ following = moment(result["histogram"], result["m"], result["W"], saving + Q(1, 10**18))
+ require(upper < 1, "Requested saving is not certified")
+ result["saving"] = str(saving)
+ scale = 2**256
+ lo = lower - 1
+ hi = upper - 1
+ enclosed = [Q(lo.numerator * scale // lo.denominator, scale),
+ Q(-((-hi.numerator * scale) // hi.denominator), scale)]
+ result["moment_minus_one"] = list(map(str, enclosed))
+ result["interval_method"] = "Exact rational log and exp bounds; outward rounding to 256 bits for the saved interval."
+ result["adjacent_grid_excluded"] = following[0] > 1
+ result["moment_gap_decimal"] = float(1 - upper)
+ text = json.dumps(result, indent=2) + "\n"
+ if args.output:
+ args.output.write_text(text)
+ print(json.dumps({k: result[k] for k in ("source_sha256", "helpers", "copy_cost", "invocation_mass", "rank_mass", "deficit", "saving", "moment_gap_decimal", "adjacent_grid_excluded")}, indent=2))
+
+
+if __name__ == "__main__":
+ main()
diff --git a/research/e8-seven-stage-coupled-retiming/source365/retime.py b/research/e8-seven-stage-coupled-retiming/source365/retime.py
new file mode 100644
index 0000000000..db25baf196
--- /dev/null
+++ b/research/e8-seven-stage-coupled-retiming/source365/retime.py
@@ -0,0 +1,102 @@
+"""Change E8 frame assignments and count the resulting blocks."""
+
+from collections import Counter
+from copy import deepcopy
+import gzip
+import hashlib
+import json
+from pathlib import Path
+import sys
+
+
+ROOT = Path(__file__).resolve().parent
+SOURCE_SHA256 = "3594f19c4d01cf11fb930c5c61baeed399620acbc5b94096b16bcacb23997dd3"
+# All positions refer to the original, zero-based phase-A gate list.
+MOVES = ((65, 187, 64, (388, 771), 285),
+ (100, 198, 98, (693, 839), 296))
+
+
+def registers(gate):
+ return {gate[2]} | {term[0] for term in gate[3]} | set(gate[4] if gate[0] == "out" else [])
+
+
+def build(source):
+ candidate = deepcopy(source)
+ additions = {}
+ for origin, destination, source_register, targets, frame in MOVES:
+ gate = candidate["A"][origin]
+ assert gate[0] == "out" and gate[2] == source_register and not gate[4]
+ selected = [term for term in gate[3] if term[0] in targets]
+ assert len(selected) == len(targets)
+ touched = {source_register, *targets}
+ # The moved additions commute with every gate they cross.
+ assert all(not (registers(g) & touched) for g in source["A"][origin + 1:destination])
+ assert source["A"][destination][1] == frame
+ gate[3] = [term for term in gate[3] if term[0] not in targets]
+ additions[destination] = ["out", frame, source_register, selected, []]
+ candidate["A"] = [g for i, gate in enumerate(candidate["A"])
+ for g in ([additions[i], gate] if i in additions else [gate])]
+ frame = len(candidate["frames"])
+ assert frame == 946
+ candidate["frames"].append([256, 128, 64, 39, 20, 15])
+ for index in (193, 916, 917):
+ assert candidate["B"][index][1] == 599
+ candidate["B"][index][1] = frame
+ frame = len(candidate["frames"])
+ assert frame == 947
+ assert candidate["frames"][585] == [161, 81, 9, 5, 3]
+ assert candidate["B"][873] == ["out", 585, 550, [[198, 1, 2], [202, -1, 2]], []]
+ assert candidate["B"][874] == ["in", 585, 550, [[521, 1, 1]]]
+ candidate["frames"].append([305, 161, 81, 9, 5, 3])
+ for index in (873, 874):
+ candidate["B"][index][1] = frame
+ candidate["derived_from"] = (
+ "Three frame changes from Sussman E8 at 9c94857b; see PROOF.md"
+ "; move B873 and B874 to one common rank-six frame"
+ )
+
+ current = list(candidate["start"])
+ blocks = {role: Counter() for role in "xysc"}
+ v = candidate["v"]
+
+ def climb(register, frame):
+ old = current[register]
+ if old != frame:
+ role = "x" if register < v else "y" if register < 2 * v else "s"
+ rank = len(candidate["frames"][frame]) - len(candidate["frames"][old])
+ assert rank > 0
+ blocks[role][rank] += 1
+ current[register] = frame
+
+ for phase in ("A", "B"):
+ if phase == "B":
+ for _, register, frame in candidate["ret"]:
+ assert current[register] == frame
+ blocks["c"][len(candidate["frames"][frame])] += 1
+ for gate in candidate[phase]:
+ for register in registers(gate):
+ climb(register, gate[1])
+ for register, frame in enumerate(candidate["final"]):
+ climb(register, frame)
+ candidate["blocks"] = {role: {str(r): count for r, count in sorted(hist.items())}
+ for role, hist in blocks.items()}
+ assert sum(r * n for hist in blocks.values() for r, n in hist.items()) == candidate["N"]
+ return candidate
+
+
+def main():
+ if sys.flags.optimize:
+ raise SystemExit("Assertions must remain enabled for generation")
+ raw = gzip.decompress((ROOT / "data/original.json.gz").read_bytes())
+ assert hashlib.sha256(raw).hexdigest() == SOURCE_SHA256
+ candidate = build(json.loads(raw))
+ output = Path(sys.argv[1]) if len(sys.argv) > 1 else ROOT / "data/retimed.json.gz"
+ raw = json.dumps(candidate, separators=(",", ":")).encode()
+ with output.open("wb") as stream:
+ with gzip.GzipFile(filename="", mode="wb", fileobj=stream, mtime=0) as zipped:
+ zipped.write(raw)
+ print(hashlib.sha256(raw).hexdigest())
+
+
+if __name__ == "__main__":
+ main()
diff --git a/research/e8-seven-stage-coupled-retiming/source365/scalar_map_comparison.py b/research/e8-seven-stage-coupled-retiming/source365/scalar_map_comparison.py
new file mode 100644
index 0000000000..f814448cf7
--- /dev/null
+++ b/research/e8-seven-stage-coupled-retiming/source365/scalar_map_comparison.py
@@ -0,0 +1,71 @@
+"""Compare every row of the complete rational scalar maps of two certificates."""
+
+from fractions import Fraction
+import gzip
+import hashlib
+import json
+from pathlib import Path
+import sys
+
+
+def word(certificate):
+ additions = []
+ for phase in ("A", "B"):
+ if phase == "B":
+ retained = {k: register for k, register, _ in certificate["ret"]}
+ for target, terms in enumerate(certificate["scat"]["table"]):
+ additions.extend((certificate["v"] + target, retained[k], Fraction(a, b)) for k, a, b in terms)
+ for gate in certificate[phase]:
+ tag, _, pivot, terms = gate[:4]
+ for register, a, b in terms:
+ target, source = (pivot, register) if tag == "in" else (register, pivot)
+ additions.append((target, source, Fraction(a, b)))
+ return additions
+
+
+def row(additions, output):
+ result = {output: Fraction(1)}
+ for target, source, coefficient in reversed(additions):
+ value = result.get(target, 0)
+ if value:
+ result[source] = result.get(source, 0) + coefficient * value
+ if not result[source]:
+ del result[source]
+ return result
+
+
+def compare(certificates):
+ """Compare the complete scalar maps, including all initial helper values."""
+ a, b = certificates
+ assert all(a[key] == b[key] for key in ("h", "v", "R", "ports", "scat"))
+ n = 2 * a["v"] + a["R"]
+ words = [word(certificate) for certificate in certificates]
+ assert len(words[0]) == len(words[1])
+ counts = []
+ for output in range(n):
+ original, candidate = (row(additions, output) for additions in words)
+ assert original == candidate, output
+ counts.append(len(original))
+ return {
+ "complete_scalar_maps_equal": True,
+ "rows": n,
+ "columns": n,
+ "nonzero_entries": sum(counts),
+ "elementary_additions": len(words[0]),
+ "scope": "Exact full rational scalar map, including arbitrary source, target, and helper initial values. Frame transforms and compiled cleanup are separate obligations."
+ }
+
+
+def main():
+ if sys.flags.optimize:
+ raise SystemExit("Assertions must remain enabled for verification")
+ assert len(sys.argv) == 3
+ raws = [gzip.decompress(Path(path).read_bytes()) for path in sys.argv[1:]]
+ result = compare([json.loads(raw) for raw in raws])
+ result["uncompressed_sha256"] = [hashlib.sha256(raw).hexdigest() for raw in raws]
+ result["source_files"] = sys.argv[1:]
+ print(json.dumps(result, indent=2))
+
+
+if __name__ == "__main__":
+ main()
diff --git a/research/e8-seven-stage-coupled-retiming/source365/sources.json b/research/e8-seven-stage-coupled-retiming/source365/sources.json
new file mode 100644
index 0000000000..68edc2307c
--- /dev/null
+++ b/research/e8-seven-stage-coupled-retiming/source365/sources.json
@@ -0,0 +1,26 @@
+{
+ "repository": "https://github.com/jacobalansussman/wht-power-saving-lean",
+ "commit": "9c94857bbaee886f8649edee0bc2d3c738f9555e",
+ "mathematical_provenance": {
+ "repository": "https://github.com/DaysSky/integer-mult-bounds",
+ "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/352",
+ "commit": "04b4c3c478b5bd8797d2663d89d8db4dfd0ad9f2",
+ "scope": "Reference for the moment convention only. These files are not imported or run.",
+ "files": {
+ "research/w3-p10b-e8-complex/code/pricing/moment.py": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482",
+ "research/w3-p10b-e8-complex/code/complex/certify_complex.py": "7e480b7761fa700944a7dca41ccbefd530203b5e9168b6b37fe879b7e6da57fa"
+ }
+ },
+ "files": {
+ "data/original.json.gz": "4b92f00fc7454b9b15e6d71a3b05062792eacca0a0ca4efee46f87827d57c8aa"
+ },
+ "upstream_notice": {
+ "path": "NOTICE",
+ "sha256": "557c9ad4660eebd14a00583736c4d12d2c45f3fc9bc148845f9f3efec72c9434",
+ "retained_sections": [
+ "copyright header",
+ "4. How the new files were made.",
+ "8. The certificate of the fourth result and the search programs."
+ ]
+ }
+}
diff --git a/research/e8-seven-stage-coupled-retiming/source365/verification.json b/research/e8-seven-stage-coupled-retiming/source365/verification.json
new file mode 100644
index 0000000000..76e59bff23
--- /dev/null
+++ b/research/e8-seven-stage-coupled-retiming/source365/verification.json
@@ -0,0 +1,67 @@
+{
+ "status": "PASS",
+ "source_commit": "9c94857bbaee886f8649edee0bc2d3c738f9555e",
+ "uncompressed_sha256": [
+ "3594f19c4d01cf11fb930c5c61baeed399620acbc5b94096b16bcacb23997dd3",
+ "3191011e0cb189665c8e0a9b97137dbed50241a0704c8be01c11b1b5a9518fc2"
+ ],
+ "histogram_delta": {
+ "1": 2,
+ "2": -6,
+ "3": 4,
+ "4": 1,
+ "5": -6,
+ "6": 4
+ },
+ "histogram": {
+ "1": 2093,
+ "2": 598,
+ "3": 522,
+ "4": 141,
+ "5": 209,
+ "6": 335,
+ "7": 43,
+ "8": 24,
+ "9": 8
+ },
+ "positive_second_difference_weights": [
+ 1,
+ 4,
+ 1,
+ 2,
+ 4
+ ],
+ "baseline": {
+ "saving": "876248285600677/1000000000000000000",
+ "strict_upper_below_one": true,
+ "next_grid_lower_above_one": true,
+ "upper_gap_decimal": 8.291462013379377e-19
+ },
+ "candidate": {
+ "saving": "876412559609473/1000000000000000000",
+ "strict_upper_below_one": true,
+ "next_grid_lower_above_one": true,
+ "upper_gap_decimal": 2.5095997917841125e-19
+ },
+ "m": 45,
+ "W": 1263,
+ "helpers": 783,
+ "copy_cost": 72,
+ "rank_mass": 56715,
+ "deficit": 120,
+ "scalar_map_rows_and_columns": 1023,
+ "checks": [
+ "frame_paths",
+ "clean_source_identity",
+ "complete_scalar_map",
+ "exact_moments",
+ "strict_concavity_identity"
+ ],
+ "rejected_controls": [
+ "scatter sign",
+ "same-rank wrong subspace",
+ "copy undercharge",
+ "forbidden phase-A cancellation"
+ ],
+ "scope": "Finite E8 circuit and exact recursive moment. No new Lean build or full multiplication theorem is claimed."
+}
diff --git a/research/e8-seven-stage-coupled-retiming/source365/verify.py b/research/e8-seven-stage-coupled-retiming/source365/verify.py
new file mode 100644
index 0000000000..10c56a738a
--- /dev/null
+++ b/research/e8-seven-stage-coupled-retiming/source365/verify.py
@@ -0,0 +1,110 @@
+"""Check the pinned E8 frame changes and their exact recursive cost."""
+
+from collections import Counter
+from copy import deepcopy
+from fractions import Fraction as Q
+import gzip
+import hashlib
+import json
+from pathlib import Path
+import sys
+
+sys.dont_write_bytecode = True
+from reconstruct import moment, reconstruct
+from retime import build
+from scalar_map_comparison import compare
+
+
+ROOT = Path(__file__).resolve().parent
+OLD = Q(876248285600677, 10**18)
+NEW = Q(876412559609473, 10**18)
+GRID = Q(1, 10**18)
+
+
+def digest(data):
+ return hashlib.sha256(data).hexdigest()
+
+
+def check_bound(result, saving):
+ args = result["histogram"], result["m"], result["W"]
+ low, high = moment(*args, saving)
+ next_low, _ = moment(*args, saving + GRID)
+ assert high < 1 < next_low
+ return {"saving": str(saving), "strict_upper_below_one": True,
+ "next_grid_lower_above_one": True, "upper_gap_decimal": float(1 - high)}
+
+
+def main():
+ if sys.flags.optimize:
+ raise SystemExit("Assertions must remain enabled for verification")
+ pins = json.loads((ROOT / "sources.json").read_text())
+ for path, expected in pins["files"].items():
+ assert digest((ROOT / path).read_bytes()) == expected, path
+ raw = [gzip.decompress((ROOT / "data" / name).read_bytes())
+ for name in ("original.json.gz", "retimed.json.gz")]
+ original, candidate = map(json.loads, raw)
+ assert digest(raw[0]) == "3594f19c4d01cf11fb930c5c61baeed399620acbc5b94096b16bcacb23997dd3"
+ assert digest(raw[1]) == "3191011e0cb189665c8e0a9b97137dbed50241a0704c8be01c11b1b5a9518fc2"
+ rebuilt = json.dumps(build(original), separators=(",", ":")).encode()
+ assert rebuilt == raw[1]
+ old, new = map(reconstruct, (original, candidate))
+ delta = {r: new["invocation_histogram"].get(r, 0) - old["invocation_histogram"].get(r, 0)
+ for r in range(1, 10)}
+ delta = {r: count for r, count in delta.items() if count}
+ assert delta == {1: 2, 2: -6, 3: 4, 4: 1, 5: -6, 6: 4}
+ # These positive weights prove the cost sign for every exponent in (0, 1).
+ weights = [1, 4, 1, 2, 4]
+ coefficients = Counter()
+ for rank, weight in enumerate(weights, 1):
+ assert weight > 0
+ coefficients[rank - 1] += weight
+ coefficients[rank] -= 2 * weight
+ coefficients[rank + 1] += weight
+ assert coefficients.pop(0) == 1
+ assert dict(coefficients) == delta
+ assert sum(delta.values()) == -1
+ for key in ("helpers", "copy_cost", "invocation_mass", "rank_mass", "deficit", "m", "W"):
+ assert old[key] == new[key], key
+
+ # These damaged inputs test separate proof obligations.
+ controls = []
+ bad = deepcopy(candidate)
+ bad["scat"]["table"][0][0][1] *= -1
+ controls.append(("scatter sign", bad, "Clean-source scalar identity"))
+ bad = deepcopy(candidate)
+ bad["A"][0][1] = candidate["start"][1]
+ controls.append(("same-rank wrong subspace", bad, "A frame path is not nested"))
+ bad = deepcopy(candidate)
+ bad["cst"] -= 1
+ controls.append(("copy undercharge", bad, "Copy cost"))
+ bad = deepcopy(candidate)
+ bad["A"] += [["out", 1, 0, [[1, 1, 1]], []], ["out", 1, 0, [[1, -1, 1]], []]]
+ controls.append(("forbidden phase-A cancellation", bad, "Unsupported phase-A scalar direction"))
+ rejected = []
+ for name, broken, expected in controls:
+ try:
+ reconstruct(broken)
+ except ValueError as error:
+ assert str(error) == expected, (name, str(error))
+ rejected.append(name)
+ else:
+ raise AssertionError("Damaged input accepted: " + name)
+
+ scalar = compare((original, candidate))
+ assert scalar["complete_scalar_maps_equal"] and scalar["rows"] == 1023
+ result = {"status": "PASS", "source_commit": pins["commit"],
+ "uncompressed_sha256": list(map(digest, raw)),
+ "histogram_delta": delta, "histogram": new["invocation_histogram"],
+ "positive_second_difference_weights": weights,
+ "baseline": check_bound(old, OLD), "candidate": check_bound(new, NEW),
+ "m": new["m"], "W": new["W"], "helpers": new["helpers"],
+ "copy_cost": new["copy_cost"], "rank_mass": new["rank_mass"], "deficit": new["deficit"],
+ "scalar_map_rows_and_columns": scalar["rows"],
+ "checks": ["frame_paths", "clean_source_identity", "complete_scalar_map", "exact_moments", "strict_concavity_identity"],
+ "rejected_controls": rejected,
+ "scope": "Finite E8 circuit and exact recursive moment. No new Lean build or full multiplication theorem is claimed."}
+ print(json.dumps(result, indent=2))
+
+
+if __name__ == "__main__":
+ main()
diff --git a/research/e8-seven-stage-coupled-retiming/source375/LICENSE b/research/e8-seven-stage-coupled-retiming/source375/LICENSE
new file mode 100644
index 0000000000..261eeb9e9f
--- /dev/null
+++ b/research/e8-seven-stage-coupled-retiming/source375/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/e8-seven-stage-coupled-retiming/source375/MANIFEST.sha256 b/research/e8-seven-stage-coupled-retiming/source375/MANIFEST.sha256
new file mode 100644
index 0000000000..f09444eaff
--- /dev/null
+++ b/research/e8-seven-stage-coupled-retiming/source375/MANIFEST.sha256
@@ -0,0 +1,163 @@
+c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4 ./LICENSE
+967e6d7e76e216e4898cf543c75b527e8d397ec1ddba3800cb20701f24c89524 ./NOTICE-PR352.md
+949fafcf2c993d0a719ee24adacabbf2d578bd657f234b38ba0464cd0d9dd759 ./NOTICE.md
+378ab6a356cdc604204f9caf6c262fe7d29258db317435e6c65f0b2d0d59178e ./README.md
+8d44d9d894c70ef195d44468f6093e797f8757a969bda93b508f65bf334e6ade ./SOURCE-pr363.json
+ba19bc388a7da6f91a7eb85ed4ee98f309eda557d1206fc3b55c3fa070ca23b5 ./SOURCE-pr370.json
+20e7c346d38cabed0555586fc99f96d497ae80d9e7b26286e84eed33a56db6e1 ./SOURCE-pr373.json
+c9a31508126f34e7ac95d802c39e8919a872cd705314de5bf3538de1636ce8ce ./code/bit/checkers/certify_bit_g.py
+97b07eb2e2664522f672fb520d188520a3a2967ecefd6700667994614d478e0c ./code/bit/checkers/certify_bit_k.py
+d1297f9052be4f2496e1ff2a77e4db2c0cdbd7d460d489b4c03e50bf317238ce ./code/bit/checkers/columns_h.cpp
+1c344d18fcd494eeca93e259f10cafae7705780e6592f6dcb35b34752dab9bc2 ./code/bit/checkers/columns_k.cpp
+d55d2b865d1c3d35e343e1a38c592b9172ed8e2596d1107e34d92e2a80c7d03f ./code/bit/checkers/cost.py
+28a0d8ee29ac75b8a789705454987f07d618f135ed1f1bd45b97f18bcc4163e3 ./code/bit/checkers/exactnd_h.py
+a591d8caa9ab50a4c7ec6934c71c93fc18fd14680180b43071e8d9d704f7ac9a ./code/bit/checkers/finite_g.py
+f93207e50f1e07237d8c29ecef6b7be89f7c35e3f0c0f2449da8f7c66f6442e1 ./code/bit/checkers/finite_k.py
+b9fa3cd05f36f5fcebfdebfb4a86fb90e92ed3c1d9157c52918ee8c5b563b54f ./code/bit/checkers/geometry_g.py
+0609920cffe790e927a4106bb82e63b3f8078c647ac9156fe0d22624634e759f ./code/bit/checkers/geometry_k.py
+223a5a07731fc315a90a3e48177796babc155c1d9985c7ae5017eff6af2a0608 ./code/bit/checkers/gram_frames.py
+aaf127c04cb31c406e5b04a63f1ae89369fccde6d8fa7cdda1ed4f32dfc5de63 ./code/bit/checkers/json.hpp
+6c1ef2b24e57781d6951c172a1024fc4300e6fd392c9d6672079a7806ab663b3 ./code/bit/checkers/legality_h.cpp
+8140eec180e42202f2c6a9f11f5c92885e60861c38a7611dd805c524e3438138 ./code/bit/checkers/tile_g.py
+64255088821f601ede2c3006f08cb97c39a4fa10dbbeb93a8a71fcfa0e1d8d77 ./code/bit/checkers/tile_k.py
+8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3 ./code/bit/export_records.py
+f69379968367544807db2f0cf14359977e56299383b3edcc4469ddea7c7ecb40 ./code/bit/independent/centres_sat.py
+11bf9620ca9db16d52d9fe806b814fc9ec9a89c4d7645354d1861d96f6e805ad ./code/bit/independent/checkword.py
+0ff65aace5da4b57d96235bf830f8f11969322e75134d498aeb70e9753ec6b0d ./code/bit/independent/mutate.py
+b0e75d6550412a7be4017695e6b237392b611bb852ad8ff309d6682c9f166a4e ./code/bit/mutate_records.py
+60fea6a9d6617a3f87376d3fda040642e9cb70e7c179015e03ede8d289f30357 ./code/bit/producer/compile.py
+0e23d4282ceb75768e82631da016aaff9818aec53c7d75a6b2a28ee1b1160dc3 ./code/bit/producer/compile2.py
+4f8a6843e83bc4f7055d7337f33dbe12ce499051f46bee1b81bbf6b34c652574 ./code/bit/producer/e8lib.py
+ba71f77dd3e3c1c54f361c066cebe9faadbc78db46376046e7af625bf1de8c24 ./code/bit/producer/frames.py
+0daf87599e9e48646b985ad87351c56c1b73cfc99cdf9eca081483846ddbfa90 ./code/bit/producer/fullword.py
+359040fb432fd392472af6b8f5dca0234dd6c2be744a791df27ba62bc5da5175 ./code/bit/producer/ham1.py
+fdf0af785ce697bd7f80b4e75f7163735f3b599d9dc42f652f0ffdbdf18ea8bf ./code/bit/producer/ham2.py
+1256c54debe0a551da8e24896ab73ef0bd4a5233ff8e6fedf21a9e6301d6e6f3 ./code/bit/producer/params-r865.json
+46c858e60ba0a117bf8227b864abf55e85ebee2d56a0dce64472b706499ac405 ./code/bit/producer/price.py
+4999c5d6bac9757e4236c45435201631eae21f644dc9543d8c0b6e3cc8360daf ./code/bit/producer/search2.py
+935ea65d9c6739e868ccf1aa439bd3c246657dfc887e4a0222a8f0901a5b41a5 ./code/bit/receipts_e8.py
+67f714e10a846e9cc62996342f825cd715055031e0b12591abdafd225717e195 ./code/bit/receipts_k.py
+fc03e8f7bf73d7d70346b87c835d44508b0581c9ff9aec708fbbd4f0121e0394 ./code/bit/regression/certify_bit.py
+26f5c9be3a7f545d50be458e3d17403921b5542a7dcd2986c848664a774977a8 ./code/bit/regression/columns_h_pr346.cpp
+d55d2b865d1c3d35e343e1a38c592b9172ed8e2596d1107e34d92e2a80c7d03f ./code/bit/regression/cost.py
+aaf127c04cb31c406e5b04a63f1ae89369fccde6d8fa7cdda1ed4f32dfc5de63 ./code/bit/regression/json.hpp
+5661d0b91e07d95736bde4c1824f27bebaecce0a84e38403f5391ebc51a52056 ./code/bit/regression/legality_h_pr346.cpp
+7bd5cb48537621f1217d174274d42483da4e2d02feec238643c798c36b30366a ./code/bit/regression/prime_new.py
+98cd03bc9582e7bd0ab194c191ea8eea940539e510051443ab9fd3e572a364ab ./code/bit/regression/prime_witnesses.py
+6c288f6f234b528c1a7c0a4adfb724e91e0fe6b18c8dffad96af3f973de1829a ./code/bit/regression/stage_cohort.py
+38c3f78daac118395565a65fa3543b1c349638ff2519ce7fda0dad2d788e90ae ./code/bit/regression/tile_check.py
+616bf82b56077c9e575791a70715047a5e01932649c3feb3e4c8ec56b39c9fab ./code/certify_b3.py
+5fe7174cd3a6580a74e4c1bf8fa7b426e8673f1c285603bf3076d4e758d70731 ./code/complex/code/bridged.py
+52d68781eaf6d9decf02446a532a7336fcf15924a9f6781ba0833d038decb9f8 ./code/complex/code/complex_basis.py
+ccc924537db0c0d55f0c1934e79b8cf4d85b4fb336473d7b42d69e12557aa9f2 ./code/complex/code/complex_gx.py
+e000ee131389fec427388b85f632879cbaaf10e5e5d979a47d6307d64ce58982 ./code/complex/code/complex_labels.py
+c617b0fd2e18adcff15f6bf6cb3d54cc31f8432993be048b3442a5729eeff410 ./code/complex/code/complex_scalars.py
+dfb4c9108bfea4a09f3e38f12b9dbe6164abab1a4fef8442ca593e2110d38ef4 ./code/complex/code/complex_splice.py
+93b78a2e038b23264d04836928c78b6ebf33b87ff3dcc0e43ba0f1748fadd143 ./code/complex/code/p10pins.py
+dfd1afbbb3ff86f54db6a0313916403ec8ee6f939caa62f3edcc9d7a151bff95 ./code/complex/code/scatter.py
+c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4 ./code/complex/inputs/complex/LICENSE
+9419dd03a2f52cf8bdfc4d18216ce29f263ab583b27f01ced8e420985bcb7c81 ./code/complex/inputs/complex/NOTICE
+66d8f4ea8752abd89952d6674a636575a0db16e18b1c16e293f48f64242f0c46 ./code/complex/inputs/complex/retained/FINITE_BRIDGE.txt
+2bc28e50f3eb092195294cafa81213e520f6d42e7935e9905ad8a6199e2a7c87 ./code/complex/inputs/complex/retained/compact-control-layout.tex
+b963c3d2f4e1b7059aa289bb4b4ac89b688920bcf42f5b20d7698cdef0132cc6 ./code/complex/inputs/complex/retained/compact-control-movement.tex
+00117892971ae766188ace0af03030c44164fda105e42b70d84f52c3339a7dcb ./code/complex/inputs/complex/retained/copied-centers-assembly.tex
+d0ce6d3d504996aadb098227885224e48df46101daec8893523a0a8b7364d8fe ./code/complex/inputs/complex/retained/copied-centers-lemma.tex
+dfee33b0281e5551bb6927f757ff0240abade60ae1800f715afd88853ae0191e ./code/complex/inputs/complex/retained/endpoint-gauge-complex.tex
+c9bb9655b594583c6b4bab8cb485233f1d1e588f83858cf1e4c3530cee8fed54 ./code/complex/inputs/complex/retained/general-clifford-frames.tex
+4738089103a4b263b3b0ef458f5ef35519c696f1ea871ae79e508d3720f5870a ./code/complex/inputs/complex/retained/stopped-product-complex.tex
+0d76527bf9c259b9532466a7b056ad6ff118867a96e044ff8e1a24aca12e1dbb ./code/complex/inputs/complex/source-pins.json
+5c24746a6330907b9b37d6064095035a58575d64ce793d6d7c9881121fdc3980 ./code/complex/inputs/complex/sources/Work__Bridge__Cert.lean
+cf7d7d330b1bffe2e66712c873e647b13dc32db1ccfc0e0f4cd62ee6caf584f0 ./code/complex/inputs/complex/sources/Work__Bridge__Net.lean
+6d0649eb62589e66057f044e1e2103fc42f3f57a1498f82a26565bd8eb4026d0 ./code/complex/inputs/complex/sources/Work__Carrier__Live.lean
+71dc3dda23dfe510d5d53cbada3a6c540cd1dc2825503fda618a5bd6cfc3e812 ./code/complex/inputs/complex/sources/Work__Carrier__Phases.lean
+2e8e88efd4dcbdf0b1a6e39ce7eea8c5fd5ffee2faf360a8c0c9cba84c0e4ef3 ./code/complex/inputs/complex/sources/Work__Fourier__Main.lean
+c302f5834287421f11f3b0da7112fcde876cbc702896f2af4145b2d72ee393a2 ./code/complex/inputs/complex/sources/Work__GCert__Chain__Geom.lean
+ade7e7873da75ca63a4b5ce2f562dde9c12bfbb69d87d7ae831039ff790e5adb ./code/complex/inputs/complex/sources/Work__GCert__Chain__InvThm.lean
+22ae34809466b4ac2a2c5cdde526f51ff246f5189f7c142b38aa4c0dcffb04a4 ./code/complex/inputs/complex/sources/Work__GCert__Chain__NetCert.lean
+6e17a68b1e988969f6eb77000028f7ed877e687b8ad3976ec1707fcfe1d2f520 ./code/complex/inputs/complex/sources/Work__GCert__Chain__NetDef.lean
+c122bc01392a6fdcc0bee918fed81804d3c9b1d3e071016dab65a4ed804ef0b6 ./code/complex/inputs/complex/sources/Work__GCert__Chain__NetStage.lean
+0de429c80231334f1ce92575c1e8ac382ca2d5e7d956767b547639a8941d9a8c ./code/complex/inputs/complex/sources/Work__GCert__Chain__Phased.lean
+c33ec3fce09c0971c32ddcbb86d9383ffbe4c6d05cf36f20460005e6547bb845 ./code/complex/inputs/complex/sources/Work__GCert__Chain__WinB.lean
+cb61f304da51f1dd0a2ec25bca4b63eb095eeb2863289e1e2bdee7c82beff48b ./code/complex/inputs/complex/sources/Work__GCert__Data__B2Gp193Main.lean
+d5314f2b93a7f0e1c949fb502331825bfc6d9d8762d35f865443e7c95b6c7ef7 ./code/complex/inputs/complex/sources/Work__GCert__Data__Glue.lean
+9587ddb9961f44938032b609307ab91c0b0e757e3991f1ad95480dd50fd4f72b ./code/complex/inputs/complex/sources/Work__GCert__Data__InstB2Gp193.lean
+d92ee6889be4753fc99f467bd84039743325123a1165128378b9c906a04f2703 ./code/complex/inputs/complex/sources/Work__GCert__Data__P193Cert.lean
+0299bcd0fe255960eec682eef0f045f7e5cb1e4711af2aab4393526eae2caea3 ./code/complex/inputs/complex/sources/Work__GCert__Data__P193Price.lean
+479434815822e98f015e335361089c3788d00dc3dd39c2944f75410aa0c158fe ./code/complex/inputs/complex/sources/Work__GCert__Data__P193ScalOK.lean
+6b40cac1481c931d47b1a092e382d04716ede0e785c492a2f2983e886a257c3f ./code/complex/inputs/complex/sources/Work__GCert__Data__RateB2Gp193x.lean
+aba94a004c94dcae7cf3047c88a6da9561555f4ebe8ab92e299e6ce09ee7aa66 ./code/complex/inputs/complex/sources/Work__GCert__Data__Raw.lean
+45c768c9d71a7cc18bd6db74cb036db880d89580ca60557bb4a492280296b169 ./code/complex/inputs/complex/sources/Work__GCert__Data__SolutionB2Gp193x.lean
+feec0a3828867968a5c7c2c30b86ed70449abc3c660a60ada67203a75bae2ef7 ./code/complex/inputs/complex/sources/Work__GFrame__Engine__Adapt.lean
+34906dbf5ae16b5174db00b4881a5cc1d2e583b8c8806db6523a5e2f86565f09 ./code/complex/inputs/complex/sources/Work__GFrame__Engine__Letters.lean
+80fb3daa9a45de0ed6da570eb4476b9104734be65d0116f58bcfcbcd67f771d0 ./code/complex/inputs/complex/sources/Work__GFrame__Engine__Level.lean
+6ba897a9495ddadcf8558b93133fdfaf66fc35ce7fa2c53e2d5667335c315e0b ./code/complex/inputs/complex/sources/tools__gx__ORIGIN.md
+6f3dc8bb639933227a8dae181ec4a542e85c7276be9c9e330f49518e7b630b95 ./code/complex/inputs/complex/sources/tools__gx__gx.py
+9c9dcfac47f0535bf3aa8ebf7c662cdef0ebda50a9f0a9282b8f3cf34809f835 ./code/complex/inputs/complex/sources/tools__gx__gxbind.py
+dab7fec9f44c2d368ed334055d7126e202017feb46e41a8d86e2d998720f67c2 ./code/complex/inputs/complex/sources/tools__gx__gxconv.py
+eb972c06fe8c322db2d9a8d9a7d05596e8f40c4ca8e5f42eb6df3c7361b5d517 ./code/complex/inputs/complex/sources/tools__gx__gxcore.py
+c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4 ./code/complex/inputs/e8/LICENSE
+557c9ad4660eebd14a00583736c4d12d2c45f3fc9bc148845f9f3efec72c9434 ./code/complex/inputs/e8/NOTICE
+842b217147cf84e8042d6ef1c33104d5444b6587b594664bc9eb89b237ab4ad0 ./code/complex/inputs/e8/Work/GCert/Data/B2Ge8.lean
+987103107d5586c096016f0a702d0de35b74398dbb50ac66f5886a43a5ca0d05 ./code/complex/inputs/e8/Work/GCert/Data/B2Ge8Main.lean
+a59db9d54b83adc73391916f7c1ef5e381ff073027781c26cb350f43b79839e3 ./code/complex/inputs/e8/Work/GCert/Data/ChallengeB2Ge8x.lean
+13a243c7d7be31ae429d19b5ecd5d428d60c41b7cca8a330f0c4179b110ba7ea ./code/complex/inputs/e8/Work/GCert/Data/E8Cert.lean
+cd250dd72406dde37765c501f666ceeedcc18f831070b26369bcb154c1f99a8e ./code/complex/inputs/e8/Work/GCert/Data/E8Price.lean
+6bd5e68effe8913a3f73e25ea59142cd9928ddf81e94250a6ea28aa7317388b3 ./code/complex/inputs/e8/Work/GCert/Data/E8ScalOK.lean
+5c7fb23df2c10b690f638a19bf066905b5b620b8a2ad0ffde76cc9348d8aa2b4 ./code/complex/inputs/e8/Work/GCert/Data/Gen/E8.lean
+36de82f6969c23082876a4d6848428623d1c65d2df3fc917f23ecba003189dd2 ./code/complex/inputs/e8/Work/GCert/Data/Gen/E8/S0.lean
+6ea83365afe01664b2132a630511b4de65f938dc328744ce7f77a01fad97f32d ./code/complex/inputs/e8/Work/GCert/Data/Gen/E8End.lean
+cce81699abe1f85a870dcf64edd395d2cf5a586da7700af565b557093095ab51 ./code/complex/inputs/e8/Work/GCert/Data/Gen/E8Hist.lean
+a343219b419f30f8ac4dd3a0a98bf53550c5fec6b2cbd245320a95977c319016 ./code/complex/inputs/e8/Work/GCert/Data/Gen/E8Par.lean
+78036e5443775ade5bde46a77ba3e0433fe22160da11b5b6c96c7f1075ecfbbd ./code/complex/inputs/e8/Work/GCert/Data/Gen/E8Scal0.lean
+f6b248dc4c3b2c94db95989b6bd5ad3c3f0d7ece3a511e5b69069550b821b138 ./code/complex/inputs/e8/Work/GCert/Data/Gen/E8Seg0.lean
+79d16ccceb61391446ea97f77fddadafa9150e9dea97919e775f6c78daa71839 ./code/complex/inputs/e8/Work/GCert/Data/Gen/E8Seg1.lean
+924340aebc6f68b5a6526311ce33341af0a0a5a8375416762f08c1914ec08abe ./code/complex/inputs/e8/Work/GCert/Data/Gen/E8SegF.lean
+650600b631a21221956f9abbab9abebcc9cca628512d3e9a017e2373e2649b17 ./code/complex/inputs/e8/Work/GCert/Data/Gen/E8Tab0.lean
+60036fa4deeb19d39fc0dddf31359d2b6d2407ff66070f145b111bff16190eb0 ./code/complex/inputs/e8/Work/GCert/Data/Gen/E8Tab1.lean
+c8a248da3eb770ba55ef267d118b29d49983311087ef789398d555e2c44b3a41 ./code/complex/inputs/e8/Work/GCert/Data/Gen/E8Tab2.lean
+41975d430ec0095ad465a36d4903e90c01bc891d3abe5e2c372ef786c029a7ed ./code/complex/inputs/e8/Work/GCert/Data/Gen/E8Tab3.lean
+a290360c175544cb85edffe1b92fcf7d447cba09128e19de8dc87e0a1ff0c524 ./code/complex/inputs/e8/Work/GCert/Data/Gen/E8YChk.lean
+c1fee298187ea19b5d70fcfccef7d4fd4161be70c0adda19a89ca9933a759954 ./code/complex/inputs/e8/Work/GCert/Data/InstB2Ge8.lean
+7b6e59724c0f140e714afba237d5a1a91b22da70abc096ce274690140b39a3a6 ./code/complex/inputs/e8/Work/GCert/Data/RateB2Ge8.lean
+7c56d865ed6bfcb6919dabc1a6e53f8744ff4824a2f78335787485f3090970d1 ./code/complex/inputs/e8/Work/GCert/Data/RateB2Ge8x.lean
+dd52f1fe0a372480edaf5e6c64903d6257c410e43d406f8acb6bf8f60a1ee28f ./code/complex/inputs/e8/Work/GCert/Data/SolutionB2Ge8x.lean
+ddad06c37f9268986f3ec8ce43da5230ee2bd887da2480328413a0dc58f2a926 ./code/complex/inputs/e8/comparator/B2Ge8x.json
+4b92f00fc7454b9b15e6d71a3b05062792eacca0a0ca4efee46f87827d57c8aa ./code/complex/inputs/e8/tools/certificate/gcert1-e8-r783.json.gz
+be41ee310f28121c3e424cc8637d8fa02ef7c47fc8945e9bbd3856138fd800d6 ./code/complex/inputs/e8/tools/e8/replay.py
+a0f16e2c9e078ffbfb2174281ee93a48c18593aefb880318fc105ec85a205932 ./code/complex/inputs/e8/tools/gen/foldgen.py
+7a3c38a698c129e13a767da75926a1305eb0c031b908450afc6feb185505c59a ./code/complex/inputs/e8/tools/gen/foldlib.py
+ef8c869e4cf8da33a4c10b96f7f6faafd46e15d66766238070a60315aa169994 ./code/complex/inputs/e8/tools/gen/gen_rates.py
+1b5eb3730cb16cf516e760879951fdfb9b065efc55f78c29a5c6404fcca57a78 ./code/complex/inputs/e8/tools/gen/gen_sharp.py
+0488b7a2442c795414f103df912d1e6cc66d37b5be270940ea9564b7f2b666be ./code/complex/inputs/e8/tools/gen/templates/ChallengeB2L16x.lean.txt
+d414a890dfe126916374c1afc804b90e5081b7760f894b9ccdcf23d83a12f9ee ./code/complex/inputs/e8/tools/gen/templates/SolutionB2L16x.lean.txt
+0e22bbe5924284e2fb916337ccefc8e41f6e54469749986ad15b3b81cfaec534 ./code/complex/inputs/e8/tools/gx/gsmirror.py
+9c9dcfac47f0535bf3aa8ebf7c662cdef0ebda50a9f0a9282b8f3cf34809f835 ./code/complex/inputs/e8/tools/gx/gxbind.py
+eb972c06fe8c322db2d9a8d9a7d05596e8f40c4ca8e5f42eb6df3c7361b5d517 ./code/complex/inputs/e8/tools/gx/gxcore.py
+ce9151054370c2210ed08f54c249a19dcb6946d182cdf934dee1a3781b53040f ./code/complex/inputs/e8/tools/gx/gxgen.py
+f00802d48ef3fedb00278f0b1c7bde074cc49dd30f202d7f32a9d2aebb3be443 ./code/complex/inputs/e8/tools/gx/gxpaths.py
+514a5719f970fe36b1273cf59df0396db0e042dd7864c2eea53ab2a2fd1e2ad6 ./code/complex/inputs/e8/tools/gx/gxrate.py
+3cc09a9c1a2db681c0f2016bc821af5b674d34834dbd6f195b9d482ce7c0ff58 ./code/complex/inputs/e8/tools/gx/gxunit.py
+b6172d58749c0b3b9138570c74827bcb23bf5db4ff9643740768cd7782ac4ca6 ./code/complex/inputs/e8/tools/gx/regen_check.py
+ad8fe9811c6ea0d89c795caef48686cfca600f5d540ebfd5d1251d6777cec7cf ./code/complex/inputs/e8/tools/gx/regen_check_e8.py
+9e2d5b8e1f5f5d1c3113ed563ace88a3e5a605e1f053af350f1cec4d4791a4c4 ./code/complex/pins-e8-b3.json
+bffda4be2ef3ba7a1072029779cfa448e3d19a986eae444c7970b87f48b294c6 ./code/complex/pins-e8-b3h.json
+bf66f785878f636616ceab193e5a222143945ea06fc2f13dfb99b204ebba82ff ./code/complex/pins-e8.json
+a28cfd37ce5da0e97e03f225629f17f31e0278142b3757345ed47d7a66560cbf ./code/complex/portable_complex.py
+aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098 ./code/pricing/base_two_moment.py
+81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482 ./code/pricing/moment.py
+c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c ./code/pricing/outer.py
+98cd03bc9582e7bd0ab194c191ea8eea940539e510051443ab9fd3e572a364ab ./code/pricing/prime_witnesses.py
+e509d08cd82d078df86f491f83a312516cae26c5528ad073b924c73f53b34edd ./code/provenance.py
+cfc30216f441a1c44a533f2f26954f90e454136af8842c497de4e2da9bd32d8d ./data/bit/RECORD-SHA256SUMS
+1fb726ea3818fe0837cceb0dd22a71a0814f064e5e781628104610d6468e0e55 ./data/bit/bitE8-r865.json.gz
+caabc13126e8f87d08f7697f51512cb3431ff52861f4190149251d8e19224430 ./data/regression-p10/BASE-RECORDS.bin.gz
+35070b83d12ebc60003ed344315328713134a43bdb04217c2c5cbc39e101391f ./data/regression-p10/BASE-frames.json.gz
+1e37ae5001447dd78a8287d8aa23d73a1d5862c4017f44db49af327f58d7cf22 ./data/regression-p10/BASE-states.json.gz
+0bd464f873b0f59622026793affb308bf087833de6f3197202adc7a36d9d0782 ./data/regression-p10/receipts-loans/banks.json.gz
+82b21b4e6bb4b20e0ecbca44f59941362f57a26a019f179e19b5b7b86262a116 ./data/regression-p10/receipts-loans/finite.json.gz
+7dccea4b8c4a81597779dc0944297d5f60efd9e2e5b19469417712e2192c6cca ./data/regression-p10/receipts-loans/global_result.json.gz
+c4074b86171c5bde8fbbff6df0022a116f17e11f0d2116ae3dfe75c8b2a18c64 ./data/regression-p10/receipts-loans/math.json.gz
+505c13c667230e946e708d7c9086de34d1c5e259a557f6685765054001e29981 ./data/regression-p10/receipts-loans/raw.json.gz
+e7bb691b741227ce389ff6341fa0548ff8f638cc492a06be40fcd829fac0bed9 ./data/regression-p10/receipts-loans/scalar.json.gz
+1939ad706e192fb3781e8a0018880b1c6291ded07d40edc4048ab1a0e48f71ee ./requirements.txt
+f00ebcfa36f95e45b79b636c826cc8a390a3e4b724b24644231014c8d74a5663 ./verify.sh
diff --git a/research/e8-seven-stage-coupled-retiming/source375/NOTICE-PR352.md b/research/e8-seven-stage-coupled-retiming/source375/NOTICE-PR352.md
new file mode 100644
index 0000000000..4f9a0194a3
--- /dev/null
+++ b/research/e8-seven-stage-coupled-retiming/source375/NOTICE-PR352.md
@@ -0,0 +1,33 @@
+# Attribution and provenance
+
+Prepared by DaysSky, assisted with Claude. Apache-2.0 (see `LICENSE`) applies to the new code and to the inherited Apache-2.0
+code below; third-party notices are preserved where files are vendored.
+
+- **Complex supplier: the E8 unit** (`code/complex/inputs/e8/`): Jacob Sussman, jacobalansussman/wht-power-saving-lean
+ at `9c94857bbaee886f8649edee0bc2d3c738f9555e` (Apache-2.0, Copyright 2026 Jacob Sussman; his `LICENSE` and `NOTICE`
+ are vendored beside the files). The certificate `tools/certificate/gcert1-e8-r783.json.gz`, the 24 Lean modules and
+ the comparator configuration of his kernel-checked theorem `wht_main_block_B2Ge8x`, his Lean-data generators
+ (`tools/gx/{gxgen,gxrate,gxbind,gxunit,gxcore,gsmirror,gxpaths,regen_check,regen_check_e8}.py`,
+ `tools/gen/{foldlib,foldgen,gen_rates,gen_sharp}.py` and templates) and his stand-alone `tools/e8/replay.py` are
+ vendored byte-identical and sha-pinned in `code/complex/inputs/complex/source-pins.json`. His README credits
+ devices from this repository in the unit: slot reuse with a compensating read (jamesyc #124, eumemic #143), late
+ pairing (Chafik Boukhalfa #200/#233), the in-place pair (icekylinx #184, carried in ikeboy's #191/#193).
+- **Bit word, Design T, twin condensation, checkers and engines** (`data/bit/`, `code/builders/`, `code/checkers/`,
+ `code/pricing/`, `code/export_p10.py`, `code/stage_cohort.py`): unchanged from LJH-217's PR #346 at
+ `11b4de5ff8ed5fccf55d4af1043358d257308e8e`, which builds on DreamingOfClouds' PR #325 p10b word and PR #315 engines
+ (#285/#276 gen5/gen4 lineage on eumemic's PR168 generator and source527 package, PR #200's physical rules, hcg890
+ and Jacob Sussman's five-stage architecture, Evan McKinney's completed banks), utcorvusvolat-dotcom's w3 Design T,
+ twin condensation and verifier (PR #310) and PR #266's official checkers. See PR #346's notice for detail.
+ `json.hpp`: Niels Lohmann, MIT license in its header.
+- **Complex checks** (`code/complex/portable_complex.py`, `code/complex/code/`, `code/complex/inputs/complex/`):
+ PR #315's portable complex checks as ported to p = 10 in PR #346 (#256/#233/#202/#200/#194/#184 lineage:
+ icekylinx, Chafik Boukhalfa, Avi Eisenberg, eumemic and others). Jacob Sussman's `gx.check1`, `gxcore` and pinned
+ Lean chain sources under `code/complex/inputs/complex/sources` are unchanged from PR #346 (byte-identical at
+ `9c94857` except his `ORIGIN.md`, kept at `f010392`).
+- **New here**: `code/complex/code/scatter.py` and the generalization of the label, scalar, splice and guard checks
+ from the paired-cube star scatter with h centres of rank h − 2 to any gx scatter (table or star) with any number
+ of retained totals of any rank (regression: on PR #346's p = 10 program the generalized checks give byte-identical
+ scalar schedules, splice programs, primitive expansions, ledger and precision guard); the generalized final-climb
+ partition; the E8 pins; the Lean-binding and replay steps of `certify_complex.py`; `verify.sh` changes.
+
+Credits do not imply endorsement or review by the credited authors.
diff --git a/research/e8-seven-stage-coupled-retiming/source375/NOTICE.md b/research/e8-seven-stage-coupled-retiming/source375/NOTICE.md
new file mode 100644
index 0000000000..235facfadc
--- /dev/null
+++ b/research/e8-seven-stage-coupled-retiming/source375/NOTICE.md
@@ -0,0 +1,57 @@
+# Attribution and provenance
+
+Prepared by DaysSky, assisted with Claude. Apache-2.0 (see `LICENSE`) applies to the new code and to the inherited
+Apache-2.0 code; third-party notices are preserved where files are vendored. `SOURCE-pr370.json`, `SOURCE-pr363.json`
+and `SOURCE-pr373.json` record, by git blob id, every file taken unchanged from those three pull requests.
+
+## Vendored
+
+- **The E8 bit word and its bit-side checks** (`data/`, `code/bit/` except the files listed as new below,
+ `code/pricing/`, `NOTICE-PR352.md`, `LICENSE`): unchanged from PR #370 (Dylan Crow, utcorvusvolat-dotcom) at
+ `b7fe9cdf2da009c947ff6b334c562bc190b30373`:
+ - the word `bitE8-r865`, its producer, the record exporter, the independent checker and its controls, the centre-count
+ CP-SAT proof;
+ - the generalized checkers `legality_h.cpp`, `columns_h.cpp`, `gram_frames.py`, `geometry_g.py`, `tile_g.py`,
+ `certify_bit_g.py`, `finite_g.py` and the receipt assembler `receipts_e8.py`;
+ - the unmodified PR #346/#352 sources in `code/bit/regression/` and the regression data in `data/regression-p10/`.
+
+ PR #370's notice gives the lineage of these checkers: PR #266's official cohort checkers as generalized by LJH-217's
+ PR #346; the source527/p10 packages' `finite_check.py`, `geometry527.py` and `global_lowering.py` (eumemic's source527
+ package; PR #200, Chafik Boukhalfa; PR234, hcg890 / Henry Grant, on Jacob Sussman's five-stage architecture; Evan
+ McKinney's completed banks; the p = 10 ports by DreamingOfClouds and Chafik Boukhalfa); PR #315's engines
+ (`moment.py`, `base_two_moment.py`, `outer.py`, `prime_witnesses.py`). `json.hpp`: Niels Lohmann, MIT license in its
+ header.
+- **The complex supplier** (`code/complex/`, `code/certify_b3.py`): unchanged from PR #363 (DaysSky) at
+ `9df55dad6ddd05c3458793dfd82d1c2fe0ddbbb4`: Jacob Sussman's E8 unit, Lean data, generators and replay
+ (jacobalansussman/wht-power-saving-lean at `9c94857`, Apache-2.0, Copyright 2026 Jacob Sussman; his `LICENSE` and
+ `NOTICE` are beside the files), PR #352's portable complex checks with the layout as a parameter, and `bridged.py`,
+ which generalizes Sussman's bridged five-stage word to B_K. See `NOTICE-PR352.md` for the complex-check lineage.
+
+## From PR #373
+
+Everything above was vendored by PR #373 (DaysSky) at `3ff87b5dc0b22a57958547ee347d5da25b7f9401`. That PR also added the
+K-parameterized bit-side checkers `columns_k.cpp`, `geometry_k.py`, `tile_k.py`, `certify_bit_k.py`, `finite_k.py`
+and `receipts_k.py` (`SOURCE-pr373.json`).
+
+## New in this package (halving degree two)
+
+- `code/complex/portable_complex.py`: the finite guard computes the least halving degree and charges it in the
+ external row coefficient (t = 1 is the original). It keeps m <= 72, and the idle-climb split is read from the pins.
+- `code/complex/pins-e8-b3h.json` (unsplit B_3) and the third guard run and exact b in `code/certify_b3.py`.
+- `verify.sh`, `code/provenance.py`, `README.md`, this notice, `MANIFEST.sha256`, the provenance files, the workflow.
+
+## New in PR #373 (kept)
+
+- `code/bit/checkers/columns_k.cpp`: `columns_h.cpp` with the bank schedule, twin bridges and terminal exchange
+ generated for B_K (`-DKPAIRS`, default 2 = the five-stage tables).
+- `code/bit/checkers/geometry_k.py`: `geometry_g.py`'s routes, chained stage boundaries, idle pairs and entrance
+ completion on 2K + 1 blocks, with the idle chronology of `bridged.py` and explicit dyadic intermediate frames for
+ the half-shrink splits.
+- `code/bit/checkers/tile_k.py`, `certify_bit_k.py`, `finite_k.py` and `code/bit/receipts_k.py`: the bank width, the
+ one-level histogram, the stage counts of the finite bill and the receipt assembly for B_K.
+- `verify.sh`, `code/provenance.py`, `README.md`, this notice, `MANIFEST.sha256`, the two provenance files, the
+ workflow.
+
+Each new checker reproduces the PR #370 checker it generalizes at K = 2; `verify.sh` compares the receipts.
+
+Credits do not imply endorsement or review by the credited authors.
diff --git a/research/e8-seven-stage-coupled-retiming/source375/README.md b/research/e8-seven-stage-coupled-retiming/source375/README.md
new file mode 100644
index 0000000000..bafeeaab56
--- /dev/null
+++ b/research/e8-seven-stage-coupled-retiming/source375/README.md
@@ -0,0 +1,168 @@
+κ = 9.5424356568133e-4
+
+# Seven-stage E8 bit and complex suppliers, with the complex idle climbs at halving degree two
+
+This package gives a conditional finite construction with **κ = 95424356568133/10¹⁷ ≈ 9.5424356568133·10⁻⁴**:
+
+- +2.40 % over PR #373 (9.3191395651209e-4), which it extends;
+- +9.00 % over PR #370 (8.75481145306751e-4).
+
+Everything is PR #373's, with one change on the complex side. PR #363 split the complex supplier's two longest idle
+climbs below m/2, 38 → 31 + 7 and 32 → 31 + 1, to meet the half-shrink guard of the inherited finite bridge
+(2 · max child < m). Here they are **left whole**. The largest complex child is then 38 of m = 63, so one recursion level
+no longer halves the size, but two do: 63² = 3969 > 2 · 38² = 2888, which is **halving degree two**.
+
+| side | supplier | layout | coarse saving |
+| --- | --- | --- | ---: |
+| bit | PR #370's E8 bit word `bitE8-r865`, unchanged (PR #373) | B₃, split (max child 27 of 56, degree 1) | c = 968197503705007/10¹⁸ ≈ 9.68197503705007·10⁻⁴ |
+| complex | Sussman's E8 unit `gcert1-e8-r783`, unchanged | B₃, **unsplit** (max child 38 of 63, degree 2) | b = 119394377245827/(125·10¹⁵) ≈ **9.55155017966616·10⁻⁴** |
+
+The bit side is 1.4 % above the complex side, so **the complex side binds**. κ is the complex-bound assembly of PR
+#315's `outer.assembly`: all 47 constraints hold, the complex leaf cap itself is rejected, and the adjacent 10⁻¹⁸ grid
+point is rejected. The bit word, its seven-stage checks and the circuit of the complex unit are unchanged from PR #373.
+That includes the Lean binding of Sussman's `wht_main_block_B2Ge8x`.
+
+## Halving degree two
+
+The half-shrink guard is used once in the inherited complex finite bridge
+(`code/complex/inputs/complex/retained/FINITE_BRIDGE.txt`, section 4): "The complex child maximum below m/2 gives
+halving degree 1, while log2 W < 5208 < 10000". The external row coefficient is then bounded by
+A = 10000 + 9909 + 252 = 20161. With halving degree t the recursion depth is t·⌈log₂ n⌉, and the row term becomes
+t·log₂ W. The guard (`code/complex/portable_complex.py`) now:
+
+- computes the least t with mᵗ > 2·(max child)ᵗ;
+- charges t times the actual physical stock logarithm, 2 · 1903 + 9909 + 252 = 13,967 < 20,161, so A and the outer
+ assembly are unchanged;
+- keeps the cover bound m ≤ 72 and the completed-child induction gap, now 49·B > 0.
+
+At t = 1 it is the original guard. The B₂ run (PR #352's pins) and the split B₃ run (PR #363's pins) are
+regressions in `verify.sh`.
+
+This is the generalization the repository already uses elsewhere:
+
+- **PR #144's integration review** (`research/pr-review-20261009/check_paired_cube_arithmetic.py`): a complex child of
+ 60 at m = 72, halving degree 4, and the row coefficient 4·2571 + 9909 + 252.
+- **The copied-centers assembly** (`copied-centers-assembly.tex`, with `research/copied-fixed-reversed/balanced_assembly.py`):
+ halving degrees 9 and 20, a row reserve D_j(e) = t_j⌈log₂ e⌉, and coefficient Σ t_j·w_j.
+- **PR234 on the bit side** (`research/five-stage-source527-banks/UPSTREAM-PR234-PROOF.md`): "The proper child ratio 5/6
+ requires halving degree four. The one-level weighted recurrence is retained; its histogram is not multiplied by four."
+
+The moment equation is the one-level histogram either way. Only the finite row constant depends on t.
+
+**Why not further.** Unsplit complex B₄ prices at 9.5673·10⁻⁴, but m = 81 exceeds the cover bound m ≤ 72. Unsplit B₅
+needs halving degree three and prices lower (9.3708·10⁻⁴). The bit side keeps PR #373's split layout because it does
+not bind. Unsplit, at halving degree two, it would give 9.9123·10⁻⁴.
+
+## The layout
+
+PR #370's bit word uses the five-stage bridged word: two bank pairs per class, five invocations, three layers of twin
+bridges, then the terminal exchange. In B_K (PR #363, `code/complex/code/bridged.py`) pair p borrows its first forward
+invocation from pair p − 1 in the same way:
+
+ stage 0, 1, 2 pair 1: forward, backward, forward
+ stage 2p-1, 2p pair p: backward, forward (p = 2..K)
+ after stage 2p-3 X(p-1) += Xp, Yp -= Y(p-1)
+ after stage 2p-2 Yp += Y(p-1), X(p-1) -= Xp
+ at the end Y(p-1) -= Yp, Xp += X(p-1) (p = K..2)
+
+So K pairs are exchanged by 2K + 1 invocations on H ⊕ 2K·H, with m = (2K+1)h, W = 2Kv + R and D = 2Kv − (2K+1)·L for copy
+loss L per invocation. With L = 72, both E8 units have D = 120 in five stages and D = 216 in seven. One invocation of
+the bit word is unchanged. Only the word around it changes:
+
+- **Idle climbs of the bit word in B₃** (h = 8): pair 1 [34], pair 2 [14, 7, 20], pair 3 [28, 7, 6]. The two climbs
+ above m/2 are split at explicit intermediate frames, 34 → 27 + 7 and 28 → 27 + 1. The largest paid child is then
+ 27, and 2 · 27 < 56 satisfies the half-shrink guard.
+- **Banks.** Every helper starts at frame 0, so all 865 residuals have width 8. Width-56 banks hold 7 of them, and 7 ∤ 865,
+ so the bank tiling uses **T = 7 literal replicas**: 865 exact width-56 banks. The moment arithmetic is invariant
+ under this normalization.
+
+## What is checked (`bash research/e8-seven-stage-halving-two/verify.sh