diff --git a/research/crosscall-kernel-demotion/LICENSE b/research/crosscall-kernel-demotion/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/crosscall-kernel-demotion/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/crosscall-kernel-demotion/MANIFEST.json b/research/crosscall-kernel-demotion/MANIFEST.json new file mode 100644 index 0000000000..5f9d80419c --- /dev/null +++ b/research/crosscall-kernel-demotion/MANIFEST.json @@ -0,0 +1,71 @@ +{ + "audit_candidate.py": "a86441df1e354f611a56484cc54267fb985f842c8785e8bc5b0bb33252db046f", + "audit_owner_table.py": "f63f27331a7c815b25cccfc6a72f62a54dd0520d746643adaff2edd5a1d7a27f", + "data/CONSTRUCTION.json": "d73dbd0015117af6a1f0d239e71e0e6fee75fcccb5edd26558201a03eb9bc304", + "data/DISPATCH.json": "f81aad6195eacf186edacf0ca4adcd7dfe9765cc205949b691968c28b50f5942", + "data/EDITS-FROM-PR1148.json": "e79e5ece31655be723dc64b309ab751e665a7346a3ff45b7a91a1c715678646f", + "data/OWNERS.json.gz": "eb53009d2a21d1ee3fb80453075bd38f35622b16222a8a33a5ec723eb1625df0", + "data/PLAN.json": "5dd01b82011de226d2aa21ba44bab893fb555d5e378c8f7e91d5b17e61f3d243", + "expected/CONSERVATIVE-PRICE.json": "41c872a091b16870f97ea7171790c2afaf4207836a15dbc4cc0f46936567e3cf", + "expected/EXACT-PRICE.json": "da8b3e90fbd8e127aecda32cf634c7a8596ffc8e687d85fe9b5c02e1e4e63822", + "expected/OWNER-AUDIT.json": "c6d20b018e2a3dd6a986de906788652beb5954a277f11f45152ec421e66dfb53", + "finite_invoice.py": "2d1a8a66481483ffd91537faf0a96c4fc734e1ff2e940796f2f998276cb73718", + "inputs/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "inputs/PR589-EXPECTED.json": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4", + "inputs/PRIOR-ALLOWANCE.json": "ce1bfa49be88ae67a404f606a11db2232b7e1f2610d4418058e39749d86d8478", + "inputs/ROUND20-PARENT-TEMPLATE.json.gz": "025448abdf2012d327e50a009084e1501690d05e650300d2982836aa0350ae00", + "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "local/check_changed_phases.py": "92061d2e7392f4afe2d13bc336faf1a0c42325e4f63f09ebd092ce0d3597d65e", + "local/check_local.py": "2e771bc2ddd1561c9e5d3647a4b409b35d9712cb7a2cfa63b03f05882ce8c243", + "local/data/EXPECTED-1-CANONICAL-WORD.json.gz": "b41c78942ea3174dbfab28e6dade6545e2c7f755a14de2e81be63761843b2bc2", + "local/data/EXPECTED-1-CHANGED-PHASES.json": "0091bbff98fca45e54397fca69fda6b935a5ef85a7254c498013e6522e20db76", + "local/data/EXPECTED-1-LOCAL-REPLAY.json": "ff5947ade6e5f4c2d1b91679997dd11f70868b72806d1fe190bf56b10f70f75a", + "local/data/EXPECTED-2-CANONICAL-WORD.json.gz": "14c3a1997625a24c60e7de0222ae6953b7bfdad184dc0596f430200f2d37b47e", + "local/data/EXPECTED-2-CHANGED-PHASES.json": "6fd1fc288e2534607140def2ae9376e56bb6edd08caef0da4f1f382745fbe3b3", + "local/data/EXPECTED-2-LOCAL-REPLAY.json": "5482fe7635fbda7af6fb6dc312ea55f1c56ee37cfdecde9bae00591217d28228", + "local/data/EXPECTED-3-CANONICAL-WORD.json.gz": "fa2a382574c758e28ddac24ebef628dbac26d31905b49059e58ed1baeeb68d1a", + "local/data/EXPECTED-3-CHANGED-PHASES.json": "e4c6e9b050aafbdcb3816f04d0dddcaaaf73390918689d44413fa7bff501de28", + "local/data/EXPECTED-3-LOCAL-REPLAY.json": "32443956851b3515ba10999c435614aa061ff1c1ebd21ef9a8bdc49ada25a838", + "local/data/OLD-CANONICAL-WORD.json.gz": "023d65ac313372f489d90d8d53a5ca867c9016c154b158860590290042cd1297", + "local/data/PARENT-ROUTING.json.gz": "66d3c3c70983224650643a0a05a21ac6c6959f84d0f4528650601016f5a76844", + "local/data/PATCHES.json": "bc8d71681ec1658e812f6be648e672034813dd38fe5bcef7a7d2c22ab65e2278", + "local/data/PR1148-WORD.json.gz": "a8a1362e1cf3bb4d5a43e077bbc842d140eb8a4420c16673757c486ca001f1a8", + "local/data/PROVIDERS.json": "f77bc9af0d6700c34580e6d140225f9eab82842fbb8bf94c0a851a66adf4a356", + "local/LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "local/README.md": "36399dbc4e13ffadb90c97d5d0076a5bff18c3faae8a4dbca14fa64b905c226b", + "local/SOURCE-PINS.json": "48d14e9b0d0832488779dd314d390e31813353a8df1a56e00451c302fdc21db1", + "local/UPSTREAM-NOTICE.md": "a0fe85fb2207f0e6831a96deaeefb65afa379c1377a29f0b586f1db4bb4b2137", + "local/vendor/audit_local.py": "03afcfc9da428b3f6edac81c1fee7f277ab81b64998efae78380b63498dec6cd", + "local/vendor/clifford/clifford_exact.py": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "local/vendor/hpe_audit_and_transport.py": "c9a05ff291016b870b4fc925b317abd9c3a604c73ffc8920dfdbbeb475e20aa3", + "local/vendor/hpe_audit_local.py": "6bd9a1e279c9c9e4f3767d9f82e537b559292906feb2ddab02f380fb6523a810", + "local/vendor/hpe_emit_local.py": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805", + "notes/cells/HYPERPLANE-CLASS-CHECK.json": "cf68267429634dab4ee0946d465d93cef82514a5cbf838fdb3c49d4cfc03468b", + "notes/cells/HYPERPLANE-PROOF.md": "4b0e29b45a54c7d888e2b9e9d8f1359aa0e5c0614f62ada7011353d6446c1cf9", + "notes/cells/HYPERPLANE-SCREEN.json": "0dda1a83ff4f3520b524d59405f996bb70a61b58f2bfd5f62de820f042b1039a", + "notes/cells/OPENAI-MECHANISMS.md": "3e77e69cab40698e7a87201a26b1a859b532a74dc056de50ea7e0c6ef62fc5f2", + "notes/cells/OPENAI-SOURCE-LEDGER.json": "529f4732ce1fd34e63eef27b47245b8ffabbb441867ba92dd9de52087bb46730", + "notes/cells/PR-SYNOPSIS.md": "5c4bb2d91ef8e17cd8db05420b8c4f2a642202b19564a204404a17699131dc22", + "notes/lead/OPENAI-MECHANISMS.md": "c98b4f960459b7016ce5e92c824da3cbf33ee5ad53de3b7618d39317ed8e80f9", + "notes/lead/OPENAI-SOURCES.json": "cf6ca10b5a5cd255c9ccb0514fb563054d4d2471076fec3dcbbf84956282d056", + "notes/owners/LAST-GROUP-SEARCH.json": "d1ba4e0330bf2ec5a03ccc1f31acf87ed9a23d7a070525554b03944dfdb0e921", + "notes/owners/OPENAI-SOURCE-LEDGER.json": "c432b5ee2e3ac9a51ebfdc2f11d22a53e1d1321a4625a1716345ad75e1c0aaea", + "notes/owners/OWNERS-PROOF.md": "8a8e702b46c4f554f52d8eeb15b66d16b37321ed8962433553b9e17492ba1cc2", + "notes/recurrence/OPENAI-SOURCES.json": "ab4cf18ef7981742bbfe0d2f71e9b69b73067702f94381a56c8e10a262c2522d", + "notes/recurrence/RESULTS.md": "188f5f13532cc2fb0c97f3ddfbda212c8ec7c2058d3a29679b7c32bea0a37aed", + "notes/recurrence/SUFFICIENT-TRANSPORT.md": "dbbd6f1fcd4fb0e03fa704c60cc42458aac469f96cc6e543470d70f6bcb6dd54", + "NOTICE.md": "a449bf1d4b1aa4a7469409d7acb96a6d1c0c8e8e93060cdd730778289a0d1d60", + "pricing.py": "f70822befde7c5bb94b6ee11cb4ecc57bc4d15f6abac9f9bc2fab8e4d0846aa3", + "README.md": "afdb5aba76867a2718c53dd4409f9330f604ef482768668bf502f6b4d3fc028f", + "UPSTREAM-NOTICE.md": "a75967ebc34e3bf2ff2c25c08e6c7f1a61b0c0d171cfd1b62196ae2caaf2c610", + "vendor/engines/base_two_moment.py": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098", + "vendor/engines/moment.py": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482", + "vendor/engines/outer.py": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c", + "vendor/pr1148/CLAIM.json": "5d2d7f3a0c57373942d588303f9736db01d4dc69fc8b35b6e2945b10627905db", + "vendor/pr1148/NOTICE.md": "a0fe85fb2207f0e6831a96deaeefb65afa379c1377a29f0b586f1db4bb4b2137", + "vendor/pr1148/OWNERS.json.gz": "93cb570c9496725ed5204d9f890ddf337ed8c3fb1a1b980de3e905f65e71b2dd", + "vendor/pr1148/PLAN.json.gz": "c56ac6b25f119107c8470e01582a8be3d78421553b684c113582c6078f998e36", + "vendor/pr1148/SOURCE-PINS.json": "d23f4c3e6c68a1090b2d9fb92fbbc075a2c125b60fcae1fba7091c1778d893c0", + "vendor/pr1148/SPEC.json": "448141cbeeb6747f742360b72b5561c3c398decf0a308a559f4c0acd93db800c", + "verify.py": "4aeed60ca226c6531ffdbd7d315a3cc792ad64c364a3b45a27b709423831785d" +} diff --git a/research/crosscall-kernel-demotion/NOTICE.md b/research/crosscall-kernel-demotion/NOTICE.md new file mode 100644 index 0000000000..be18de44a3 --- /dev/null +++ b/research/crosscall-kernel-demotion/NOTICE.md @@ -0,0 +1,21 @@ +Cross-call kernel demotion, 2026-10-13. New work is Apache-2.0. + +This package was prepared with substantial OpenAI Codex assistance and adds no +submitting-user name or email. It is a finite conditional construction. + +Direct input: PR1148 at 98235a9cf4ce355ec5cf3fac2eca7b3b98a20838, +CrocSwap/integer-mult-bounds, research/k8-three-demotions. Its original notice +is retained in vendor/pr1148/NOTICE.md. The entrance-demotion lead is credited +there to PR1111; the earlier adaptive-prefix and local frame work from our +previous package is reused with its original upstream source notices. + +PR1129/1131/1152 supplied the T37 comparison and motivated the early screen; +their gains and owner maps are not composed into this final T16 certificate. +Original local, controller, Clifford and exact arithmetic ancestry is recorded +in UPSTREAM-NOTICE.md and local/UPSTREAM-NOTICE.md. Those attributions are +preserved rather than replaced by a claim of independent invention. + +Eight mathematical source adaptations from OpenAI's math collection are +documented in notes/ with exact source hashes and declaration statements. +No new Lean kernel certification, unconditional multiplication result, +public submission, accepted upstream result or external review is claimed. diff --git a/research/crosscall-kernel-demotion/README.md b/research/crosscall-kernel-demotion/README.md new file mode 100644 index 0000000000..f6803eeb50 --- /dev/null +++ b/research/crosscall-kernel-demotion/README.md @@ -0,0 +1,137 @@ +# Cross-call kernel demotion + +**Conditional kappa = 0.001675224519162937.** Conservative endpoint: +**0.001675224516317980**. Frozen comparison is +[PR1148](https://github.com/CrocSwap/integer-mult-bounds/pull/1148) at +`98235a9cf4ce355ec5cf3fac2eca7b3b98a20838`, kappa 0.001675121647789207. +The absolute improvement is 0.000000102871373730, about 0.006141 percent. +The latest public PR bodies were reviewed through PR1153; no later-frontier or +unconditional multiplication claim is made. + +From the repository root, with Python 3.10+ and a new output directory: + +```sh +python -I -B research/crosscall-kernel-demotion/verify.py --out ../crosscall-result +``` + +The replay is self-contained and standard-library-only. Three newly reconstructed +providers run sequentially with bounded native Python children, at BelowNormal +priority on Windows. No C++, GPU, WSL, network, optimizer, Lean build or persistent +service is used. Allow approximately a minute for the full replay on a typical +desktop. Programs, charts, receipts and logs are written outside the source tree. + +## Two coupled mechanisms + +PR1148 supplies the three-demotion, eight-rank-seven-end local word and its actual +T16 table. We add three disjoint demotion islands at groups **627, 635, 651**. +Searching every codimension-one subspace of each five-dimensional start frame +finds legal directions that a last-vector-only rule misses: group 651 works while +retaining the required vector 30. Each concrete joint prefix is recounted and +independently checked; a local algebraic fit alone is not a scalar certificate. + +The selected four-helper subframes are: + +```text +627: [68,34,24,1] 635: [170,102,30,1] 651: [139,96,25,7] +``` + +The extra helper indices are `(403,405,406,407)`, `(411,413,414,415)` and +`(427,429,430,431)`. Prefix k widens exactly 4k helpers from four to five and +changes its complete local paid profile by +`k * (-8H1 + 8H2 + 4H3 - 4H4)`. + +A same-call allocation hosts 42 extra groups. Cross-call width-four donor +exchanges raise this to **89 groups across 52 calls**. A donor can execute at a +different call only when both literal inactivity windows, active-family +exclusions and per-call uniqueness checks allow the exchange. Swapping the +width-four roles preserves every occurrence and every old family load; widening +the selected target then consumes one actual unit of slack. All subsequent +offsets are rebuilt chronologically. The final map consumes **356 of 360 unit +axes**; no fractional or shared helper is introduced. + +Prefixes zero through three occur **92, 30, 7, 15 times**. The complete profile is: + +```text +{1:340860, 2:71848, 3:59684, 4:18364, 5:11808, + 8:1152, 24:1, 48:4918} +``` + +The complete difference is 89 copies of `-12H1+8H2+4H3-4H4`, including the paid +remainders. Rank mass stays 1,041,408, live stock 14,336 and deficit 5,120. There +are 69,120 literal helper roles, 144 complete calls, 1,409 changed owner records, +4,923 paid remainders and 10,271 actual 73-column chart types. The source-bound +literal edits reconstruct the final table from PR1148 exactly. + +## Fresh checks and charged work + +Each changed local prefix is checked on all 704 arbitrary input columns in both +orientations, including dirty helpers, complete monotone frame histories, +low-end cones, exact native emitted programs and 25 emitted corruption controls. +Every changed Clifford edge and endpoint wrapper is checked including global +phase: prefixes one/two/three have 9/18/27 changed edges, 1/2/3 changed wrappers, +and 10/20/30 phase controls. + +The independent owner audit reconstructs source events and inactivity windows, +checks all actual pending axes, literal per-call inventories, family identities, +disjoint chronological blocks, source/phase geometry and full orthogonal charts. +It recounts every paid residual and performs 13 role/geometry/dispatch controls. +The full profile is priced by two exact rational moment engines, with native and +conservative brackets and all 47 strict outer inequalities. The retained bit +profile's complete mass and exceptional-residue arithmetic are repriced; its full +circuit is not cold-replayed. + +The fresh invoice reads the actual changed programs. The local child count is +3,498, adapters 387,120, and local primitive bound 10,039,700,351,134. It adds the +entire fresh per-vertex bill **3,589,198,021,555,152** to the pinned prior allowance +**2,877,946,989,724,568**, giving **6,467,145,011,279,720**. All nine finite guards +and four invoice controls pass. Actual prefix 397 fits the charged 512-bit +reserve; physical row 16,469 fits the retained 20,161 limit. Chart cost is bounded +per occurrence; a lower distinct-chart count is not treated as free work. + +## Two distinct OpenAI proof structures for each worker + +Sources were inspected in the registered [OpenAI math](https://github.com/openai/math) +collection. These are sourced mathematical adaptations, not newly compiled Lean +imports, eight independent exponent gains, or priority claims for those sources. + +| Worker | Two structures used | Evidence | +|---|---|---| +| Local words | Split-flag coordinate projections; postselection transporter bijections | `notes/cells/OPENAI-MECHANISMS.md`, `OPENAI-SOURCE-LEDGER.json` | +| Owners | Matching augmentation that preserves covered roles; explicit disjoint physical pool templates | `notes/owners/OWNERS-PROOF.md`, `OPENAI-SOURCE-LEDGER.json` | +| Controller | Direct-sum tensor restriction; joint-signature histogram/orbit lifting | `notes/recurrence/SUFFICIENT-TRANSPORT.md`, `OPENAI-SOURCES.json` | +| Root | Exact positive capacity scans; semantics and additive cost under program relabelling/composition | `notes/lead/OPENAI-MECHANISMS.md`, `OPENAI-SOURCES.json` | + +The notes preserve the sufficient proofs, exact source hashes, checked scopes, +hyperplane census, same-call fallback and bounded final augmentation search. +The naive PR1148/T37 composition priced worse and was stopped before a large +replay. PR1129/1131/1152 inform that alternative; none of their gains is added. +Failure of a restricted last-four-gap search is not a global optimality theorem. + +## Conditional scope and provenance + +Fresh checks establish this changed finite construction. Unchanged PR1148 scalar +admission/phase edges, compiler/all-size interfaces, common-label and mutable +source realization, complete-call hosting, precision/tape and exact recovery, +analytic transfer and inherited bit H1-H5 remain explicit assumptions. This is +not an unconditional multiplication theorem, new Lean certificate, hosted CI +result, independent human review or global packing optimum. + +`MANIFEST.json` binds every other file by SHA-256 and exact file inventory before +replay. `vendor/pr1148/SOURCE-PINS.json` binds ancestor inputs. Preserve raw bytes +and disable automatic line-ending conversion when cloning; fresh gzip headers +may differ across Python versions, so generated byte bindings and mathematical +equality are checked together. + +The candidate `data/PLAN.json` contains only the geometry fields used and checked +by this verifier. The unchanged full upstream plan is retained separately in +`vendor/pr1148/PLAN.json.gz`. Actual per-call widths and profiles come exclusively +from `data/DISPATCH.json` and the freshly reconstructed native providers; old +registry metadata is not retagged as a certificate of the new mixed controller. + +Direct credits include PR1148, PR1111, PR1117 and our preceding adaptive-prefix +method; PR1018/987, PR1030, PR1005/1004, PR1022/858/870/1074, PR942, PR864, +PR635 and retained ancestry; PR589 supplies the unchanged bit contract. +PR1129/1131/1152 supplied the new T37 comparison. The Apache-2.0 license and +original source notices are preserved. See `NOTICE.md`, `UPSTREAM-NOTICE.md`, +`vendor/pr1148/NOTICE.md` and `local/UPSTREAM-NOTICE.md`. New work was prepared +with OpenAI Codex assistance; no submitting-user name or email is added. diff --git a/research/crosscall-kernel-demotion/UPSTREAM-NOTICE.md b/research/crosscall-kernel-demotion/UPSTREAM-NOTICE.md new file mode 100644 index 0000000000..ebc24a0168 --- /dev/null +++ b/research/crosscall-kernel-demotion/UPSTREAM-NOTICE.md @@ -0,0 +1,34 @@ +# Attribution and scope + +Four verified provider types are offered to every call: PR571's prefix word with twelve multi-cut cold kernels (PR568's unchanged constructor), the same word with forty width-five entrance promotions (PR569's unchanged frame constructor) before those kernels, PR575's plain joint-prefix provider, and PR568's eight-cold provider. A window MILP with an exact per-pattern model chooses the dispatch and a literal owner map. PR583's six source-bound kernel frame coalescences (its unchanged constructor and negative controls) are applied to every PR571-prefix provider word (ck and atm3), followed by two further coalescences that each first move one addition past two commuting additions (package code/build_gate_moves.py, extending PR583's constructor); a final hyperplane_end step (package code/build_hpe.py) then runs 46 single-gate cleanups h -= p right after part B at the dim-8 join U of their registers, so 46 width-8 entering helpers per call end at U with width 7; each such gate commutes with every earlier cleanup gate on its registers (for 8 of them the partner's one earlier gate x -= p only reads p), and the reordered program is replayed exactly. A window MILP (exact windows, RINS around an LP vertex) gives the dispatch ck 45 / atm3 21 / jp8 6 and the literal owner map. + +Pinned external sources (unchanged; `verify.py` checks their manifests and every file it uses): +- PR568 (`research/complex-multicold`, commit `71c99ac935a33bb7b59a1b4a7af8725a939b0b90`). +- PR571 (`research/structural-gain`, commit `b7bdc5a8de18fcf418cfb9c7d83a2b1097a5e4a3`). +- PR569 (`research/larger-gain`, commit `897213a855b7fb8a1b8b0e552a2f5c42e6c1b326`). +- PR575 (`research/complex-joint-prefix`, commit `eac6f7e378ab622dac50a2fd4b7ef6eab014de44`). +- PR583 (`research/kernel-frame-coalescing`, commit `89be768f0157f5a3d8e4db69cf1748768605eac9`). + +Provider construction is described as typed steps in `data/SPEC.json` (`build`); `verify.py` runs only allowlisted step types with their paired omission audits and checks every input and output content hash. `code/` holds the spec-driven global admission scripts adapted from PR571's `frontier-composition/global-code/` (OpenAI Codex assisted, Apache-2.0): every expected value is read from `data/SPEC.json` and compared only after independent recomputation. `code/generated_identity.py` and `code/generated_identity_controls.py`, and the decompressed-content artifact identities in the bind, audit, invoice, assembly and phase-timing scripts, are taken unchanged from PR586 by chafreaky (`research/promoted-kernel-coalescing`, commit `4846fee5b06af770e9b3a10c36200f673d656725`, OpenAI Codex assisted, Apache-2.0), including its proof-content and reference/metadata mutation controls; the normalization of descriptive width metadata after frame changes follows the same PR. + +In PR601, the owner map was nominated by a HiGHS window MILP (adapted from PR569's `global/nominate_width7.py`) with lazy cross-time Hall cuts; this package's re-solved map is described below. Neither is an admission dependency. + +DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. (The PR601 package this one starts from states: "Prepared by Claude Code (Anthropic) research agents.") Apache-2.0 applies; LICENSE is included. All notices, licenses, source pins and AI disclosures of the pinned sources and their ancestry are retained in those packages and are not replaced by this notice. All inherited conditional assumptions remain conditional. + +**This package (complex-571-cold14, DreamingOfClouds).** It starts from PR601 (jeremykothe2, `research/complex-571-hpem46`, commit `529ab7dcb59d5ea7a5798e9e06cf5b3aee8a1550`). Everything above is kept unchanged except the following: +- every provider chain (ck, atm3, jp8) gains the typed step `cold_end` (`code/build_cold_end.py`, `code/cold_end_controls.py`; recipes `data/recipes/*-cold_end.json.gz`); +- the generalised native chain and the global admission scripts accept cold helpers that end below FULL (with `0:U` wrappers), a refactored exact cleanup, and check the wrapper order; +- `data/PLAN.json` / `data/OWNERS.json.gz` (dispatch and literal owner map) come from a relocate/swap/ejection-chain/provider-flip annealing search started from PR601's map, refined by an exact pattern-restricted owner model (CP-SAT) with a literal edge-colouring expansion (not an admission dependency); +- `data/SPEC.json` holds the expected values, recorded by a discovery run and then checked by a strict run. + +The cold-end construction (a row-plus-column cone condition for low-frame ends, a rank-0 dirt-spread premix and multi-gate lower-frame cleanup) builds on PR591 / PR592 / PR593 / PR601 (jeremykothe2) and our PR599 (Lean: multi-gate and cold hyperplane-end tails). DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. Build on this at your own risk. + +**This package (complex-571-cold14-b3, jeremykothe2).** It is PR604's `complex-571-cold14` (DreamingOfClouds) with ColdBeyond's second cold end per block (two new `cold_end` A-gate primitives, `PROOF-NOTE.md`), ColdSupply's E1 entering pair and reviewed controls, a free dispatch (jp8 ×60, atm3 ×12) and a literal owner map from an exact per-time-Hall window MIP. All other construction, code, controls and proofs are PR604's and earlier contributors', unchanged. + +**This package (complex-571-cold14-k492).** It is complex-571-cold14-b3 with these changes: +- **K-triangle base words.** The leaver-read K-triangle skeleton atom and its read schedule (`data/TRI-SCHEDULE.json`) are by AtomScout, a Claude Code research agent. `code/construct_k_triangle.py` is PR531's `code/construct_504.py` (icekylinx, OpenAI Codex / GPT assisted, Apache-2.0; pinned source `direct_delivery`) extended with that atom. +- **Ported chains.** The PR604/B3 chains are ported stage by stage onto the K-triangle words by `code/build_port_stage.py` (Port480, a Claude Code research agent). `code/build_frame_regroup.py` extends PR583's `build_frames.py` (chafreaky). +- **Helper count R.** The generalisation of the global scripts to the provider helper count R is by GlobalR (a Claude Code research agent), with AtomReviewer's fixes (PROOF-NOTE-R.md). +- **Owner map.** The owner map, the cold_end recipes on the K-triangle words and the package assembly are by Stack492, Port480 and ColdBeyond (Claude Code research agents). + +Build on this at your own risk. diff --git a/research/crosscall-kernel-demotion/audit_candidate.py b/research/crosscall-kernel-demotion/audit_candidate.py new file mode 100644 index 0000000000..c878e9c8ed --- /dev/null +++ b/research/crosscall-kernel-demotion/audit_candidate.py @@ -0,0 +1,108 @@ +"""Fresh T-variable literal candidate owner/event/chart audit; no background work.""" +import argparse,collections,copy,gzip,hashlib,importlib.util,json,time +from pathlib import Path +s=importlib.util.spec_from_file_location('owners',Path(__file__).with_name('audit_owner_table.py'));O=importlib.util.module_from_spec(s);s.loader.exec_module(O) +def basis(vs): + d={} + for x in vs: + O.need(type(x) is int and 0<=x<512,'invalid local frame') + while x: + p=x.bit_length()-1 + if p in d:x^=d[p] + else:d[p]=x;break + return tuple(d[k] for k in sorted(d,reverse=True)) + +def local_contract(native,inherited=None): + w=O.read(native/'CANONICAL-WORD.json.gz') + if inherited is None: + r=O.read(native/'INDEPENDENT-LOCAL-REPLAY.json') + O.need(O.sha(native/'CANONICAL-WORD.json.gz')==r['canonical_word_sha256'],'local canonical binding') + O.need(O.sha(native/'LOCAL-PROGRAMS.json.gz')==r['local_programs_sha256'],'local program binding') + else: + r=dict(paid_profiles={o:inherited['paid_profile'] for o in ('forward','backward')},local={o:dict(prefix_bits_upper=inherited['local'][o]['prefix_bits']) for o in ('forward','backward')},scope='old scalar semantic admission inherited; frame profile and width freshly recounted') + F=[basis(x) for x in w['frames']];now=[F[i] for i in w['start']];paid=collections.Counter() + def climb(q,to): + O.need(len(basis(now[q]+to))==len(to),'local nonmonotone frame') + jump=len(to)-len(now[q]);O.need(jump>=0,'negative local jump') + if jump:paid[jump]+=1 + now[q]=to + O.need(not w['target_levels'],'zero target centre interface') + for sec in ('A','B','tail'): + if sec=='B': + O.need(all(not now[q] for q in range(w['v'],2*w['v'])),'target level interface') + for q,fi in zip(w['centers'],w['center_frames']):O.need(now[q]==F[fi],'centre frame');paid[len(F[fi])]+=1 + for gate in w[sec]: + O.need(gate[0] in ('add','scale'),'local scalar gate') + for q in (gate[1:3] if gate[0]=='add' else gate[1:2]):climb(q,F[gate[-1]]) + for q,fi in enumerate(w['final']):climb(q,F[fi]) + O.need(dict(paid)=={int(k):v for k,v in w['local_profile'].items()},'complete local profile recount') + for orientation in ('forward','backward'):O.need(dict(paid)=={int(k):v for k,v in r['paid_profiles'][orientation].items()},'native local profile binding') + widths=[len(F[w['final'][q]])-len(F[w['start'][q]]) for q in range(2*w['v'],len(w['start']))] + O.need(len(widths)==480 and all(0>j)&1);u=q^(1<>j)&1 else 0) for j in order]+[1<=0,'negative remainder') + if rem: + idle[rem]+=1;remainders.append({'owner_replica':o,'child':c,'port':p,'family':896*o+(2*P['pairs'][str(c)]+P['sides'][str(c)])*112+p,'pending_offset':used_,'rank':rem}) + paid=collections.Counter() + for call in order: + paid.update({int(k):v for k,v in profiles_by_call.get(call,S['providers']['gauge44']['expected_profile']).items()}) + paid.update(idle);mass=sum(k*v for k,v in paid.items());need(mass==S['expected']['rank_mass']==73*live-deficit,'rank mass');need(73*live-mass==deficit,'rank deficit') + return {'roles':len(rows),'calls':nc,'helper_per_call':480,'profile':dict(sorted(paid.items())),'idle_profile':dict(sorted(idle.items())),'idle_remainders':sum(idle.values()),'rank_mass':mass,'deficit':deficit,'cross_replica':cross,'actual_73column_sigmas':len(sigmas),'sigma_stream_sha256':stream.hexdigest(),'sigmas':sigmas,'remainders':remainders} + + +def rebuild_windows(parent,order,T,ph=None): + """Reconstruct last-touch to idle boundaries from literal original32-event source.""" + need(len(parent['calls'])==72,'original source call count') + source=parent.get('async_schedule',{}).get('source_schedule',parent['execution_schedule']);need(len(source)==32,'source event count') + blocks={};global_events=[];stage=None + for index,event in enumerate(source): + kind=event['kind'] + if kind in ('bank_padding_cover_sweep','translate_every_live_family'): + global_events.append(index);continue + if kind=='local_cover_sweep':stage=event['stage'];blocks[stage]=[] + need(stage is not None,'event before invocation');blocks[stage].append((index,event)) + need(global_events==[30,31],'source global tail') + events=[(idx,event,r,t) for t,(s,r) in enumerate(order) for idx,event in blocks[s]] + projections=collections.defaultdict(list) + for idx,event,r,t in events:projections[r].append(idx) + need(set(projections)==set(range(T)) and all(z==list(range(30)) for z in projections.values()),'per-replica event order') + ranks={c['child']:c['rank'] for c in parent['idle_children']} + if ph is not None: + ranks={j:z['rank'] for j,z in enumerate(ph['recipes'][0]['idle_children']) if z['rank']>0} + for recipe in ph['recipes']: + need({j:z['rank'] for j,z in enumerate(recipe['idle_children']) if z['rank']>0}==ranks,'phase rank geometry') + need(all(len(z['orthogonal_axes'])==z['rank'] for z in recipe['idle_children']),'actual phase axis rank') + stage_pair={x['stage']:x['pair'] for x in parent['recipe'] if x['kind']=='local'} + last={};bounds={};callpos={};pairs={};sides={} + for pos,(idx,event,r,t) in enumerate(events): + kind=event['kind'] + if kind=='local_cover_sweep':last[r,stage_pair[event['stage']]]=pos;callpos[t]=pos + elif kind=='bridge':last[r,event['src']]=last[r,event['dst']]=pos + elif kind=='idle_cover_sweep': + for side,child in enumerate(event['child_indices']): + if child in ranks: + bounds[r,child]=(last.get((r,event['pair']),-1),pos);pairs[str(child)]=event['pair'];sides[str(child)]=side + need(set(callpos)==set(range(9*T)),'complete source invocation positions') + windows={f'{r},{c}':[ranks[c],[t for t,p in sorted(callpos.items()) if lo2*maxchild**2) + return checks,dict(physical_stock_bits=stock.bit_length(),logical_bits=logical.bit_length(),router_bits=router.bit_length(),literal_bits=literal.bit_length(),total_mass_bits=total.bit_length(),precision_bits=(32*73*total*total).bit_length(),tape_bits=(2*total+18).bit_length(),physical_row_coefficient=row,global_prefix_bits=prefix) + +def calculate(spec,audit,dispatch,native,prior): + M,V,R=73,112,480;T=audit['calls']//9;nc=9*T;payload=512 if T<=16 else 1024;compiler=64*74**3;C=spec['providers']['gauge44']['complete_contract'] + # k0 scalar admission stays inherited. All changed providers are read from fresh native output. + providers={0:dict(children=sum(C['paid_profile'].values()),local=C['local'],wrappers=C['entering_helpers']+C['cold_hyperplane_ended_helpers'],profile={int(k):v for k,v in C['paid_profile'].items()})} + native_bindings={} + for k,d in native.items(): + w=read(d/'CANONICAL-WORD.json.gz');checks=read(d/'LOCAL-CHECKS.json');receipt=read(d/'INDEPENDENT-LOCAL-REPLAY.json');programs=read(d/'LOCAL-PROGRAMS.json.gz') + need(sha(d/'CANONICAL-WORD.json.gz')==receipt['canonical_word_sha256'] and sha(d/'LOCAL-PROGRAMS.json.gz')==receipt['local_programs_sha256'],'native source binding') + dims=[rank(x) for x in w['frames']];indices=range(224,704) + entering=sum(dims[w['start'][q]]>0 for q in indices);cold=sum(dims[w['start'][q]]==0 and dims[w['final'][q]]<9 for q in indices) + need(entering==receipt['entering_helpers']==192 and cold==receipt['cold_hyperplane_ended_helpers']==48,'actual wrapper-selected helper sets') + lp={int(r):n for r,n in w['local_profile'].items()};local={} + for o in ('forward','backward'): + z=checks[o];need(len(programs[o])==z['events'],'literal event count') + macros=sum(p[0]=='scalar' for p in programs[o]);need(macros==z['scalar_macros'],'literal macro count') + need(lp=={int(r):n for r,n in z['paid_profile'].items()}=={int(r):n for r,n in receipt['paid_profiles'][o].items()},'fresh local profile binding') + local[o]=dict(macros=macros,real_component_primitives=z['real_component_primitive_bound'],prefix_bits=receipt['local'][o]['prefix_bits_upper']) + providers[k]=dict(children=sum(lp.values()),local=local,wrappers=entering+cold,profile=lp) + native_bindings[str(k)]={x:sha(d/x) for x in ('CANONICAL-WORD.json.gz','LOCAL-PROGRAMS.json.gz','LOCAL-CHECKS.json','INDEPENDENT-LOCAL-REPLAY.json')} + dt={tuple(d['call']):d.get('variant',1) for d in dispatch};need(len(dt)==len(dispatch),'dispatch uniqueness') + selected=[];paid=collections.Counter();counts=collections.Counter() + for s in range(9): + for r in range(T): + k=dt.get((s,r),0);need(k in providers,'missing actual provider');p=providers[k];o='backward' if s%2 else 'forward';z=p['local'][o] + selected.append(dict(stage=s,replica=r,variant=k,orientation=o,macros=z['macros'],real_component_primitives=z['real_component_primitives'],wrappers=2*p['wrappers']));paid.update(p['profile']);counts[k]+=1 + idle={int(r):n for r,n in audit['idle_profile'].items()};local_paid=dict(paid);paid.update(idle) + need(dict(paid)=={int(r):n for r,n in audit['profile'].items()},'complete invoice profile');mass=sum(r*n for r,n in paid.items());need(mass==65088*T and 73*896*T-mass==320*T,'complete rank mass') + adapters={k:16*(max(z['macros'] for z in p['local'].values())+p['children']+224+480+8)+64*73 for k,p in providers.items()} + primitive={k:max(z['real_component_primitives'] for z in p['local'].values())+adapters[k]*compiler for k,p in providers.items()} + scalar=sum(x['real_component_primitives'] for x in selected);macros=sum(x['macros'] for x in selected);wrapper_factors=sum(x['wrappers'] for x in selected)*144 + bank_groups=(T+7)//8;parent_live=896*T+4536*bank_groups;parent_physical=parent_live+514;parent_idle=2016*T;parent_banks=504*bank_groups + bridges,shifts,moves=2*112*nc,4*112*T,8*112*T + need(sum(idle.values())<=parent_idle,'complete remainder reserve') + nonlocal_items=(4*112*T*9+2*112*T*9+2*nc*480+parent_idle+9*parent_banks+bridges+shifts+moves+parent_live+parent_physical+wrapper_factors) + outside=8*nonlocal_items+64*73 + pervertex=scalar+bridges+shifts+moves+parent_live+(nc*max(adapters.values())+outside)*compiler+64*parent_physical + live,physical=896*T,896*T+490;rebased=pervertex+65*(physical-parent_physical)+(live-parent_live) + need(prior['compiler']==compiler and prior['charged_prefix_bits']<=payload,'retained allowance interface') + used=max(pervertex,rebased,prior['conservative_pervertex_used']+pervertex) + prefix=max(z['prefix_bits'] for p in providers.values() for z in p['local'].values())+37+nc+nc+4;need(prefixk and piv[j]>>k&1:piv[j]^=piv[k] + return tuple(piv[k] for k in sorted(piv,reverse=True)) + +def contained(a,b):return basis(a+b)==b + +def registers(e):return e[1:3] if e[0]=='add' else e[1:2] + +def apply(e,rows,dual=False): + if e[0]=='add': + t,s=e[1:3];q=F(e[3],e[4]);require(t!=s,'self add') + if dual:t,s,q=s,t,-q + dst=rows[t] + for k,x in list(rows[s].items()): + a=dst.get(k,F(0))+q*x + if a:dst[k]=a + else:dst.pop(k,None) + elif e[0]=='scale': + t=e[1];q=F(e[2],e[3]);require(q!=0,'zero scale') + if dual:q=1/q + rows[t]={k:q*x for k,x in rows[t].items()} + else:raise RuntimeError('unknown scalar primitive') + +def invert(e): + r=list(e) + if r[0]=='add':r[3]=-r[3] + else:r[2],r[3]=r[3],r[2] + return r + +def check_parent_interface(word,main): + # Read only the retained boundary data. No builder or local checker is imported. + relative="research/community-k492-audit/pr622/replay/baseline558/complex-global/base/split-centres/CANONICAL-WORD.json.gz" + path=main/relative;raw=path.read_bytes() + require(hashlib.sha256(raw).hexdigest()=="66d3c3c70983224650643a0a05a21ac6c6959f84d0f4528650601016f5a76844",'parent canonical input pin') + parent=json.loads(gzip.decompress(raw)) + tau=lambda x:x^(43 if (x&43).bit_count()%2 else 0) + ports=parent['ports'];v=word['report']['v'] + require(len(ports)==len(set(ports))==v,'parent port count') + require(set(map(tau,word['ports']))==set(ports),'transported source/target ports') + moved={i:ports.index(tau(p)) for i,p in enumerate(word['ports'])} + centers=[moved.get(r,r) for r in word['centers']] + actual=[list(basis([tau(x) for x in frame])) for frame in word['center_frames']] + expected=[parent['frames'][f] for f in parent['center_frames']] + require(len(centers)==len(set(centers))==len(actual)==8,'eight distinct centre carriers') + require(actual==expected and all(len(f)==8 for f in actual),'ordered centre frame interface') + return dict(parent_path=relative,parent_file_sha256=hashlib.sha256(raw).hexdigest(), + transport_tau=43,ordered_frame_bases_match=True,all_ports_match=True, + transported_centers=centers,source_centers=[r for r in centers if r=2*v} + for e in w['precondition']:apply(e,dirt) + compensation=[['add',y,k,-a.numerator,a.denominator,[]] for y in range(v,2*v) for k,a in sorted(dirt[y].items())] + entering=set(map(int,w.get('start_extra',{})));lowends=set(map(int,w.get('helper_final',{}))) + coldends=lowends-entering + require(not any(e[2] in entering for e in compensation),'nonzero entrance response') + require(not any(r in entering|coldends for e in w['precondition']+compensation for r in registers(e)), 'pre-wrapper touch of residual helper') + require(all(e[-1]==[] for e in w['precondition']+compensation),'nonzero frame precondition') + early=w.get('early_cleanup',[]);earlyids={i for i,U in early} + require(len(earlyids)==len(early),'duplicate early cleanup gate') + tail=[w['cleanup'][i][:-1]+[U] for i,U in early] + cleanup=[e for i,e in enumerate(w['cleanup']) if i not in earlyids] + prefix=w['precondition']+compensation+main + program=prefix+tail+cleanup + for dual in (False,True): + actual=ident() + for e in program:apply(e,actual,dual) + expected=ident() + for t in range(v):expected[t if dual else v+t][v+t if dual else t]=F(-1 if dual else 1) + bad=[i for i in range(n) if actual[i]!=expected[i]] + require(not bad,'all-column endpoint failure '+str((dual,bad[:8]))) + print('endpoint', 'dual' if dual else 'forward','PASS',flush=True) + full=basis([1<>i)&1)<>j&1);a[j],a[k]=a[k],a[j] + for i in range(n): + if i!=j and a[i]>>j&1:a[i]^=a[j] + assert [r&((1<>n for r in a) +def basis_extend(cols,n): + out=[] + for x in list(cols)+[1<len(out):out.append(x) + assert len(out)==n + return tuple(out) +def nullspace(rows,n): + a=list(rows);p=[];k=0 + for j in range(n): + t=next((i for i in range(k,len(a)) if a[i]>>j&1),None) + if t is None:continue + a[t],a[k]=a[k],a[t] + for i in range(len(a)): + if i!=k and a[i]>>j&1:a[i]^=a[k] + p.append(j);k+=1 + return tuple((1<>j)&1)<>i&1:out=pmul(out,T[i]) + for i in range(n): + if z>>i&1:out=pmul(out,T[n+i]) + return out +def compose(A,B):return tuple(apply(A,p) for p in B) +def inverse(T): + n=len(T)//2;cols=[x|(z<>n;u,v,p=apply(T,(x,z,0));assert (u,v)==identity(n)[j][:2];out.append((x,z,(-p)%4)) + return tuple(out) +def qvalue(Q,alpha,x,n): + return (sum(alpha[i] for i in range(n) if x>>i&1)+2*sum(parity((Q[i]>>(i+1))&(x>>(i+1))) for i in range(n) if x>>i&1))%4 +def mul_i(a,p): + x,y=a;p%=4 + return [(x,y),(-y,x),(-x,-y),(y,-x)][p] +@dataclass +class Op: + n:int + tab:tuple + circuit:list + def then(self,b): + assert self.n==b.n + return Op(self.n,compose(b.tab,self.tab),self.circuit+b.circuit) + def adjoint(self): + circ=[] + for e in reversed(self.circuit): + if e[0]=='P':circ.append(('P',inv(e[1],self.n))) + elif e[0]=='D':circ.append(('D',e[1],tuple((-x)%4 for x in e[2]))) + elif e[0]=='C':circ.append(('C',e[1],-e[2])) + elif e[0]=='phase':circ.append(('phase',(-e[1])%4)) + else:circ.append(e) + return Op(self.n,inverse(self.tab),circ) + def zero_state(self,basis=0): + N=1<>i)&1 for i in range(n)) + assert all(alpha[i]%2==(Q[i]>>i)&1 for i in range(n)) + return Op(n,tuple([(1<>i&1 else 0,1<>i&1 else 0) for i in range(n)]),[('C',q,sgn)]) +def xgate(n,b):return Op(n,tuple([(1<>i)&1)) for i in range(n)]),[('X',b)]) +def fourier(n,axes=None): + out=ident(n) + for i in range(n) if axes is None else axes:out=out.then(cgate(n,1<len(selected):picks.append(j);selected.append(x) + assert len(picks)==r and all(x>>r==0 for x in Bcols) + Br=transpose(selected,r);Bi=inv(Br,r);Dr=transpose([Dcols[j]&((1<> k & 1: + x ^= pivots[k] + if x: + k = x.bit_length() - 1 + for j in pivots: + if pivots[j] >> k & 1: + pivots[j] ^= x + pivots[k] = x + return tuple(pivots[k] for k in sorted(pivots, reverse=True)) + + +def apply(e, rows): + if e[0] == 'scale': + _, target, a, b, *_ = e + q = Q(a, b) + assert q + rows[target] = {j: q*x for j, x in rows[target].items()} + else: + _, target, source, a, b, *_ = e + assert target != source + q = Q(a, b) + for j, x in list(rows[source].items()): + value = rows[target].get(j, Q(0)) + q*x + if value: + rows[target][j] = value + else: + rows[target].pop(j, None) + + +def inverse(e): + e = copy.deepcopy(e) + if e[0] == 'add': + e[3] *= -1 + else: + e[2], e[3] = e[3], e[2] + return e + + +def dual(e): + e = inverse(e) + if e[0] == 'add': + e[1], e[2] = e[2], e[1] + return e + + +def state_maps(prefix, n): + """P = exact state map of the prefix (precondition + compensation + A + cut + B), and P^-1 (rows as sparse dicts).""" + P = [{r: Q(1)} for r in range(n)] + for e in prefix: + apply(e, P) + Pinv = [{r: Q(1)} for r in range(n)] + for e in reversed(prefix): + apply(inverse(e), Pinv) + return P, Pinv + + +def cone_violations(P, Pinv, hpe, mapping, endB, final, frames): + """COLD-HPE / CONE PRE-CHECK. Necessary conditions for helper h (raw index) to end at U = final[h] under ANY + monotone common-frame cleanup of the end-of-B state P (frames only climb, every gate at a common frame): + row (J26-H dependency bound): every g in supp(row h of P^-1) has end-of-B frame <= U -- h is rebuilt from them; + column (dirt-column lemma): every g != h with P[g][h] != 0 has end-of-B frame <= U -- the column of P at h, + restricted to rows whose frame is not <= U, changes only by invertible row operations unless h is read at a + frame not <= U, so it can reach e_h only if it is already zero there. + Both are implied by the exact endpoint replay plus the frame checks below; here they fail FAST, with the reason.""" + inside = lambda a, b: basis(frames[a] + frames[b]) == frames[b] + viol = [] + for h in hpe: + U = final[mapping[h]] + viol += [('row', h, g) for g, x in sorted(Pinv[h].items()) if x and not inside(endB[mapping[g]], U)] + viol += [('column', h, g) for g in range(len(P)) if g != h and P[g].get(h) and not inside(endB[mapping[g]], U)] + return viol + + +def run(raw_path, routing_path, out): + start_time = time.monotonic() + word, routing = read(raw_path), read(routing_path) + v, h, helpers = word['report']['v'], word['report']['h'], word['report']['R'] + assert h == 9 and v == 112 and routing['v'] == v + n = 2*v + helpers + ident = lambda: [{r: Q(1)} for r in range(n)] + main = word['A'] + word['cut'] + word['B'] + assert all(not v <= e[2] < 2*v for e in word['A'] + word['B'] + if e[0] == 'add' and not v <= e[1] < 2*v) + matrix = ident() + for e in main: + apply(e, matrix) + dirty = [{} for _ in range(n)] + for r in range(v, 2*v): + dirty[r] = {j: x for j, x in matrix[r].items() if j >= 2*v} + for e in word['precondition']: + apply(e, dirty) + compensation = [['add', r, j, -q.numerator, q.denominator, []] + for r in range(v, 2*v) for j, q in sorted(dirty[r].items())] + entering = set(map(int, word.get('start_extra', {}))) + assert all(e[2] not in entering for e in compensation), 'zero-frame compensation reads an entering helper' + cleanup = [inverse(e) for e in reversed(word['A'] + word['B']) + if not v <= e[1] < 2*v] + if 'refactored_cleanup' in word: + # REFACTORED CLEANUP (cold low-frame ends): the cleanup is not the literal reversed inverse of A+B but another exact + # factorisation of the same inverse. Nothing about it is trusted: it may only touch non-target registers (T rows + # stay the compensated data accumulators), every gate is dyadic (checked below), and the arbitrary-dirt endpoint + # replay below must be exact in BOTH orientations for the full reordered program. Inherited words keep the literal + # assertion (the else branch), so their outputs are unchanged. + assert all(not v <= r < 2*v for e in word['cleanup'] for r in ([e[1]] + ([e[2]] if e[0] == 'add' else []))), 'refactored cleanup touches a target' + assert all(e[0] in ('add', 'scale') for e in word['cleanup']) + cleanup = word['cleanup'] + else: + assert [e[:-1] for e in cleanup] == [e[:-1] for e in word['cleanup']], 'cleanup is not the literal reversed inverse of A+B' + # HPE: hyperplane-ended helpers. 'early_cleanup' = [[cleanup index, frame vectors], ...] are cleanup gates executed + # right after B (before the final climbs) at the given frame; 'helper_final' = {helper: frame vectors} replaces FULL as + # that helper's terminal frame. The scalar program is the reordered one and is replayed exactly below, so a move that + # does not commute with the skipped cleanup prefix is rejected by the arbitrary-dirt endpoint assertion. + early = [(int(i), f) for i, f in word.get('early_cleanup', [])] + helper_final = {int(r): f for r, f in word.get('helper_final', {}).items()} + early_idx = [i for i, _ in early] + assert len(set(early_idx)) == len(early_idx) and all(0 <= i < len(cleanup) for i in early_idx) + assert all(2*v <= r < n for r in helper_final) + # COLD-HPE: a COLD helper (not in start_extra, entrance frame 0 = bottom) may also end at a proper subspace U. + # It is the E = bottom instance of #593's theorems: its wrappers are the (0, U) recipes R_{0,U}, L_{0,U} (checked + # exactly by hpe_adapters_local), emitted as residual_adapter events like an entering helper's. + cold_hpe = sorted(r for r in helper_final if r not in entering) + # COLD-HPE wrapper order: R_{0,U}^-1 is emitted with the entry adapters, after the zero-frame precondition and + # compensation, so (exactly as for an entering helper, asserted above) nothing before it may touch a cold-ended helper. + assert all(r not in set(cold_hpe) for e in word['precondition'] + compensation for r in ([e[1]] + ([e[2]] if e[0] == 'add' else []))), 'zero-frame precondition/compensation touches a cold hyperplane-ended helper before its wrapper' + # ENTERING helpers (start frame E != 0): their wrapper R_E^-1 precedes every gate on them, so the zero-frame precondition + # and compensation may not touch them either (mirrors hpe_emit_local's start-frame-0 rule here, at the scalar audit). + assert all(r not in entering for e in word['precondition'] + compensation for r in ([e[1]] + ([e[2]] if e[0] == 'add' else []))), 'zero-frame precondition/compensation touches an entering helper' + tail =[word['cleanup'][i][:-1] + [f] for i, f in early] + rest = [e for i, e in enumerate(word['cleanup']) if i not in set(early_idx)] + program = word['precondition'] + compensation + main + tail + rest + for backward in (False, True): + actual = ident() + for e in program: + apply(dual(e) if backward else e, actual) + expected = ident() + for t in range(v): + expected[t if backward else v+t][v+t if backward else t] = Q(-1 if backward else 1) + assert actual == expected, ('arbitrary-dirt endpoint', backward) + # The native scalar compiler allows dyadic additions and signed binary scales. + for e in program: + q = Q(e[3], e[4]) if e[0] == 'add' else Q(e[2], e[3]) + assert q.denominator & (q.denominator-1) == 0 + if e[0] == 'scale': + a = abs(q.numerator) + assert a and a & (a-1) == 0 + + tau = lambda x: x ^ (43 if (x & 43).bit_count() % 2 else 0) + ports = routing['ports'] + assert len(set(ports)) == v and set(map(tau, word['ports'])) == set(ports) + mapping = {i: ports.index(tau(p)) for i, p in enumerate(word['ports'])} + mapping.update({v+i: v+mapping[i] for i in range(v)}) + mapping.update({r: r for r in range(2*v, n)}) + full = tuple(1 << i for i in range(h-1, -1, -1)) + frames, frame_ids = [(), full], {(): 0, full: 1} + + def fid(vectors): + frame = basis(vectors) + if frame not in frame_ids: + frame_ids[frame] = len(frames) + frames.append(frame) + return frame_ids[frame] + + def transform(e): + e = copy.deepcopy(e) + e[1] = mapping[e[1]] + if e[0] == 'add': + e[2] = mapping[e[2]] + if e[-1] is not None: + e[-1] = fid([tau(x) for x in e[-1]]) + return e + + canonical = {key: [transform(e) for e in word[key]] + for key in ('A', 'B', 'cut', 'cleanup', 'precondition')} + canonical['compensation'] = [transform(e) for e in compensation] + if tail: + canonical['tail'] = [transform(e) for e in tail] # HPE (absent for inherited words: identical output) + canonical['cleanup'] = [transform(e) for e in rest] # HPE (full cleanup minus the early gates) + canonical['start'] = [fid([p]) for p in ports] + [0]*(v+helpers) + for r, frame in word.get('start_extra', {}).items(): + assert 2*v <= int(r) < n + canonical['start'][int(r)] = fid([tau(x) for x in frame]) + canonical['final'] = ([1]*v + + [fid(x for x in range(1, 1 << h) if (x & p).bit_count() % 2 == 0) for p in ports] + + [1]*helpers) + for r, frame in helper_final.items(): # HPE + canonical['final'][r] = fid([tau(x) for x in frame]) + canonical.update(h=h, v=v, R=helpers, ports=ports, frames=frames, + centers=[mapping[r] for r in word['centers']], + center_frames=[fid(tau(x) for x in frame) for frame in word['center_frames']]) + levels = {mapping[v+int(t)]-v: fid(tau(x) for x in frame) + for t, frame in word.get('target_levels', {}).items()} + canonical['target_levels'] = {str(t): f for t, f in levels.items()} + current, paid, edges = canonical['start'].copy(), Counter(), set() + + def climb(r, f): + old = current[r] + assert basis(frames[old] + frames[f]) == frames[f], ('nonmonotone', r, old, f) + if old != f: + degree = len(frames[f]) - len(frames[old]) + assert degree > 0 + paid[degree] += 1 + edges.add((old, f)) + current[r] = f + + for part in ('A', 'B'): + if part == 'B': + assert all(current[r] == f for r, f in zip(canonical['centers'], canonical['center_frames'])) + assert all(current[v+t] == levels.get(t, 0) for t in range(v)) + for r, frame in zip(canonical['centers'], canonical['center_frames']): + served = {levels.get(e[1]-v, 0) for e in canonical['cut'] if e[2] == r} + old = frame + for f in sorted(served, key=lambda f: -len(frames[f])): + assert basis(frames[old] + frames[f]) == frames[old] + if old != f: + paid[len(frames[old])-len(frames[f])] += 1 + edges.add((old, f)) + edges.add((f, old)) + old = f + for e in canonical[part]: + for r in [e[1]] + ([e[2]] if e[0] == 'add' else []): + climb(r, e[-1]) + if helper_final: # COLD-HPE / CONE PRE-CHECK at the end-of-B frames + P, Pinv = state_maps(word['precondition'] + compensation + main, n) + cone = cone_violations(P, Pinv, sorted(helper_final), mapping, current.copy(), canonical['final'], frames) + assert not cone, ('hpe cone pre-check (row / column)', cone[:8]) + for e in canonical.get('tail', []): # HPE: early cleanup gates at their common frame + for r in [e[1]] + ([e[2]] if e[0] == 'add' else []): + climb(r, e[-1]) + for r, f in enumerate(canonical['final']): + climb(r, f) + # HPE: the remaining cleanup runs at FULL, so it may touch only registers whose terminal frame is FULL; a + # hyperplane-ended helper is touched by nothing after its tail gates. + for e in canonical['cleanup']: + assert all(canonical['final'][r] == 1 for r in [e[1]] + ([e[2]] if e[0] == 'add' else [])), ('cleanup on non-FULL end', e) + assert all(len(frames[canonical['final'][r]]) < h for r in helper_final) + assert dict(paid) == {int(r): count for r, count in word['report']['local_profile'].items()}, 'paid local profile differs from the reported local_profile' + canonical['local_profile'] = dict(sorted(paid.items())) + canonical['edges'] = sorted(edges) + out.mkdir(parents=True, exist_ok=False) + payload = json.dumps(canonical, sort_keys=True, separators=(',', ':')).encode() + (out/'CANONICAL-WORD.json.gz').write_bytes(gzip.compress(payload, mtime=0)) + (out/'FULL-WORD.json.gz').write_bytes(gzip.compress(json.dumps(word, sort_keys=True, separators=(',', ':')).encode(), mtime=0)) + receipt = dict(status='PASS_CHANGED_WORD_ALL_COLUMNS_AND_NATIVE_FRAMES', + input_content_sha256=content_hash(raw_path), routing_content_sha256=content_hash(routing_path), + canonical_content_sha256=hashlib.sha256(payload).hexdigest(), + live_columns_each_orientation=n, helpers=helpers, + compensation_additions=len(compensation), scalar_operations=len(program), + center_rank_sum=sum(map(len, word['center_frames'])), + local_profile=dict(sorted(paid.items())), local_rank_mass=sum(r*z for r, z in paid.items()), + widths=[len(frames[canonical['final'][r]])-len(frames[canonical['start'][r]]) for r in range(2*v, n)], + frames=len(frames), directed_edges=len(edges), + tau=43, target_port_order_matches_baseline=True, + seconds=time.monotonic()-start_time, + scope='Fresh exact forward and inverse-transpose scalar replay on every arbitrary input; all native frame chains and dyadic primitives. Phase lowering, wrappers, global owners and global assembly are separate.') + if tail or helper_final: + receipt.update(hyperplane_ended_helpers=sorted(helper_final), early_cleanup_gates=len(tail)) + if cold_hpe: # COLD-HPE (absent for words without cold ends) + receipt.update(cold_hyperplane_ended_helpers=cold_hpe) + if 'refactored_cleanup' in word: # REFACTORED CLEANUP (absent for inherited words) + receipt.update(refactored_cleanup_gates=len(word['cleanup']), refactored_cleanup=word['refactored_cleanup']) + (out/'SCALAR-FRAME-AUDIT.json').write_text(json.dumps(receipt, indent=2)+'\n') + print(json.dumps({k: value for k, value in receipt.items() if k != 'widths'}, indent=2), flush=True) + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--raw', type=Path, required=True) + parser.add_argument('--routing', type=Path, required=True) + parser.add_argument('--out', type=Path, required=True) + args = parser.parse_args() + run(args.raw, args.routing, args.out) diff --git a/research/crosscall-kernel-demotion/local/vendor/hpe_audit_local.py b/research/crosscall-kernel-demotion/local/vendor/hpe_audit_local.py new file mode 100644 index 0000000000..17bccb64fd --- /dev/null +++ b/research/crosscall-kernel-demotion/local/vendor/hpe_audit_local.py @@ -0,0 +1,171 @@ +# Local-only extraction of the attributed PR514 / PR433 independent replay. +# Prepared for icekylinx with OpenAI Codex assistance. Apache-2.0. +# The complete local checker and its negative controls are retained verbatim. +# Global hosting is verified separately for the changed 112-port geometry. +import copy,gzip,hashlib,json,sys +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path +OUT=Path(sys.argv[1]) +c=json.load(gzip.open(OUT/'CANONICAL-WORD.json.gz')) +ir={'local_programs':json.load(gzip.open(OUT/'LOCAL-PROGRAMS.json.gz'))} +v,R,h=c['v'],c['R'],c['h'];n=2*v+R;frames=c['frames'] +levels={int(t):f for t,f in c.get('target_levels',{}).items()} +entering=[r for r,f in enumerate(c['start']) if r>=2*v and f!=0] +plain={r for r in range(n) if r not in set(entering)} + +def contains(a,b): + for x in a: + for y in b: + if x>>(y.bit_length()-1)&1:x^=y + if x:return False + return True +hpe={r for r in range(2*v,n) if c['final'][r]!=1} # HPE: helpers whose terminal frame is a proper subspace U of FULL +assert all(len(frames[c['final'][r]])0 + hist[rank]+=1;cur[r]=b + elif tag=='center': + _,k,a,b,rank=event + assert phases[-1]=='centers' and private=={('C',k):a} + cf=c['center_frames'][k];cr=len(frames[cf]) + # GK: stepwise descent cf -> served levels -> lowest (forward), reversed ascent (backward); each step is a nested child + assert contains(frames[a],frames[b]) if back else contains(frames[b],frames[a]) + assert rank==abs(len(frames[a])-len(frames[b]))>0 + chain.setdefault(k,[]).append((a,b)) + private['C',k]=b;hist[rank]+=1;centers.append(k) + elif tag=='scalar': + _,e,f=event;op=e[0];target=tuple(e[1]);source=tuple(e[2]) if op in ('copy','add') else None + if target[0]=='C' and op=='clear': + assert private.get(target,f)==f + private.pop(target,None) + else: + for r in (target,source): + if r is None:continue + if r[0]=='L':assert cur[r[1]]==f and (r[1] not in wset or (r[1] in pre_seen and r[1] not in post_seen)),('common frame / wrapper order',r,cur[r[1]],f) + else: + if r==target and r not in private:private[r]=f + assert private[r]==f + if op=='clear':rows[target]={};norm[target]=Q(0) + elif op=='copy':rows[target]=dict(rows[source]);norm[target]=norm[source] + elif op=='scale': + q=Q(e[2],e[3]);a,b=abs(q.numerator),q.denominator + assert a&(a-1)==0 and b&(b-1)==0 + rows[target]={j:q*x for j,x in rows[target].items()};norm[target]*=abs(q) + else: + q=Q(e[3],e[4]);a,b=abs(q.numerator),q.denominator + assert source!=target and b&(b-1)==0 + # Independent symbolic replay of the cleared coefficient work. + w=0 + for bit in bin(a)[2:]:w=2*w+int(bit) + assert Q(w,b)*(1 if q>0 else -1)==q + prefix=max(prefix,Q(a)*norm[source]) + norm[target]=norm.get(target,Q(0))+abs(q)*norm[source] + row=rows.setdefault(target,{}) + for j,x in list(rows[source].items()): + z=row.get(j,Q(0))+q*x + if z:row[j]=z + else:row.pop(j,None) + prefix=max(prefix,norm[target]) + else:raise AssertionError(tag) + assert phases==allowed and set(centers)==set(range(len(c['centers']))) and not private + assert sorted(r for k,r,_ in wrappers if k=='pre')==wrapped and sorted(r for k,r,_ in wrappers if k=='post')==wrapped # GK + for k,st in chain.items(): # GK: the steps of each centre chain link up and end at the centre frame + cf=c['center_frames'][k] + if back:assert st[-1][1]==cf and all(st[i][1]==st[i+1][0] for i in range(len(st)-1)) + else:assert st[0][0]==cf and all(st[i][1]==st[i+1][0] for i in range(len(st)-1)) + assert all(not row for reg,row in rows.items() if reg[0]=='C') + for r in range(n): + expected={r:Q(1)} + if back and r>p&1:x^=b[p] + if x: + p=x.bit_length()-1 + for q in b: + if b[q]>>p&1:b[q]^=x + b[p]=x + return tuple(b[p] for p in sorted(b,reverse=True)) +def dual(e): + e=list(e) + if e[0]=='add':e[1],e[2]=e[2],e[1];e[3]*=-1 + else:e[2],e[3]=e[3],e[2] + return e +def scalar(e,back): + e=dual(e) if back else list(e) + if e[0]=='add':return ['add',['L',e[1]],['L',e[2]],e[3],e[4]] + return ['scale',['L',e[1]],e[2],e[3]] +def primitive_bound(e): + if e[0] in ('clear','copy'):return 1 + q=Q(e[3],e[4]) if e[0]=='add' else Q(e[2],e[3]) + a,b=abs(q.numerator),q.denominator + assert b&(b-1)==0 + if e[0]=='scale': + assert a&(a-1)==0 + return abs(a.bit_length()-b.bit_length())+int(q<0) + # Exact binary Horner multiplication on a cleared private stream, repeated + # halving, signed accumulation into the target, then clear the private stream. + return 3+(a.bit_length()-1)+a.bit_count()+(b.bit_length()-1) + +def emit(back): + out=[];cur=c['start'].copy() + def event(e):out.append(e) + def scal(e,f):event(['scalar',e,f]) + event(['phase','zero_frame_precondition']) + for e in c['precondition']+c['compensation']: + regs=[e[1]]+([e[2]] if e[0]=='add' else []) + assert all(c['start'][r]==0 for r in regs) + scal(scalar(e,back),0) + event(['phase','entry_adapters']) + # GK: a helper that starts at a nonzero entrance frame has NO entry adapter; its paid wrapper R_E^-1 (Lemma A) precedes every gate + # that touches it and L_E^-1 follows the full-frame cleanup. Words without entrances emit PR #433's events. + entering=[r for r,f in enumerate(c['start']) if r>=2*v and f!=0] + hpe={r for r in range(2*v,n) if c['final'][r]!=1} # HPE: hyperplane-ended helpers (terminal frame != FULL) + # COLD-HPE: a cold helper (start frame 0) ending at U also carries the paid wrappers R_{0,U}^-1 / L_{0,U}^-1 (the + # E = bottom instance of #593); without cold ends wrapped == entering and the event stream is the inherited one. + wrapped=sorted(set(entering)|hpe) + for r,f in enumerate(c['start']): + if r in wrapped:event(['residual_adapter','pre',r,f]+([c['final'][r]] if c['final'][r]!=1 else [])) # HPE: R_{E,U}^-1 names U + else:event(['adapter','old_to_new',r,f]) + def climb(r,f,part): + old=cur[r] + if old==f:return + assert basis(frames[old]+frames[f])==tuple(frames[f]) + rank=len(frames[f])-len(frames[old]);assert rank>0 + event(['climb',part,r,old,f,rank]);cur[r]=f + # HPE: 'cleanup_tail' = early cleanup gates at their own frames; emitted only when the word has them, so a word + # without hyperplane-ended helpers yields exactly the inherited event stream. + for part in ('A','centers','B')+(('cleanup_tail',) if c.get('tail') else ())+('final',): + event(['phase',part]) + if part in ('A','B','cleanup_tail'): + for e in (c['tail'] if part=='cleanup_tail' else c[part]): + regs=[e[1]]+([e[2]] if e[0]=='add' else []) + for r in regs:climb(r,e[-1],part) + scal(scalar(e,back),e[-1]) + elif part=='centers': + # GK: targets sit at their nonzero-frame-compensation level (0 at the defaults); a centre copy descends + # cf -> served levels (descending chain) -> lowest served level and scatters into each target at its level + lv=lambda r:c.get('target_levels',{}).get(str(r-v),0) + assert all(cur[r]==lv(r) for r in range(v,2*v)) + for k,r in enumerate(c['centers']): + cf=c['center_frames'][k];assert cur[r]==cf + terms=[e for e in c['cut'] if e[2]==r] + path=[cf]+sorted({lv(e[1]) for e in terms}-{cf},key=lambda x:-len(frames[x])) + C=['C',k] + if not back: + scal(['clear',C],cf);scal(['copy',C,['L',r]],cf) + for a in range(len(path)): + if a>0:event(['center',k,path[a-1],path[a],len(frames[path[a-1]])-len(frames[path[a]])]) + for e in terms: + if lv(e[1])==path[a]:scal(['add',['L',e[1]],C,e[3],e[4]],path[a]) + scal(['clear',C],path[-1]) + else: + scal(['clear',C],path[-1]) + for a in range(len(path)-1,-1,-1): + for e in terms: + if lv(e[1])==path[a]:scal(['add',C,['L',e[1]],e[3],e[4]],path[a]) + if a>0:event(['center',k,path[a],path[a-1],len(frames[path[a-1]])-len(frames[path[a]])]) + scal(['add',['L',r],C,-1,1],cf);scal(['clear',C],cf) + else: + for r,f in enumerate(c['final']):climb(r,f,part) + event(['phase','exit_adapters']) + for r,f in enumerate(c['final']): + if r not in hpe:event(['adapter','new_to_old',r,f]) # HPE: no old-convention exit for a helper that ends at U; its post wrapper is L_{E,U}^-1 + event(['phase','full_frame_cleanup']) + for e in c['cleanup']: + regs=[e[1]]+([e[2]] if e[0]=='add' else []) + assert all(c['final'][r]==1 for r in regs) + scal(scalar(e,back),1) + for r in wrapped:event(['residual_adapter','post',r,c['start'][r]]+([c['final'][r]] if r in hpe else [])) # HPE: 5th field = terminal frame U # GK: L_E^-1 after the full-frame cleanup + event(['phase','done']) + return out + +def check_local(events,back): + # Literal scalar replay of the emitted stream, including center lifetimes. + state={('L',r):{r:Q(1)} for r in range(n)};live=[];paid=Counter();prims=0;macros=0 + for e in events: + if e[0]=='climb':assert not live;paid[e[5]]+=1 + elif e[0]=='center':assert live==[e[1]];paid[e[4]]+=1 + elif e[0]=='scalar': + op=e[1];tag=op[0];t=tuple(op[1]);macros+=1;prims+=2*primitive_bound(op) + if tag=='clear': + state[t]={} + if t[0]=='C' and t[1] in live:live.remove(t[1]) + elif tag=='copy':state[t]=dict(state.get(tuple(op[2]),{}));live.append(t[1]) + elif tag=='scale':state[t]={j:Q(op[2],op[3])*x for j,x in state[t].items()} + else: + s=tuple(op[2]);q=Q(op[3],op[4]);row=state.setdefault(t,{}) + if t[0]=='C' and t[1] not in live:live.append(t[1]) + for j,x in list(state.get(s,{}).items()): + z=row.get(j,Q(0))+q*x + if z:row[j]=z + else:row.pop(j,None) + assert not live and all(not row for r,row in state.items() if r[0]=='C') + for r in range(n): + expected={r:Q(1)} + if back and r5 into1->4, replacing four rank-four jumps by rank-three jumps. All eight outgoing climbs change5->6 into4->6, replacing eight rank-one jumps by rank-two jumps. All later jumps remain unchanged. The exact local profile change is therefore + + -8H1 +8H2 +4H3 -4H4. + +Each of the four starting helpers has residual width increased4->5. The construction accordingly requires four additional pending coordinates; nothing is free. The scalar word and exact704-column transfer matrices are unchanged. Concrete complete providers also require valid low-end cones and exact Clifford adapters; those were freshly checked for every selected joint prefix used in the submission. + +A codimension-one subspace of E is the kernel of a unique nonzero covectorlambda overF2. All31 nonzero covectors are enumerated, and the condition q inker(lambda) is lambda(q)=0. Since q is nonzero, this is a four-dimensional subspace of the dual and contains15 nonzero covectors. Hence each island has precisely15 valid monotone traces in this stated literal class. HYPERPLANE-SCREEN.json exhausts all93 cases and independently agrees with these masks:15 admitted and16 rejected per island. + +The chosen651 frame isspan(139,96,25,7), which contains30=25 XOR7. The former choice span(267,139,96,25) missed30 and failed nesting. Enumerating subspaces rather than merely deleting the last displayed basis vector exposes the previously missed constructive route. + +This is a sufficient explicit frame construction and exact universal invoice within a defined class, not a standalone failure barrier. It does not claim optimality over other circuits or frames, nor a physical/global witness for every enumerated subspace. The delivered prefixes use literal selected U and pass complete arbitrary-dirt, frame, cone, native-program and changed-phase checks; global owner and outer pricing checks remain separate. diff --git a/research/crosscall-kernel-demotion/notes/cells/HYPERPLANE-SCREEN.json b/research/crosscall-kernel-demotion/notes/cells/HYPERPLANE-SCREEN.json new file mode 100644 index 0000000000..13c4e1c0da --- /dev/null +++ b/research/crosscall-kernel-demotion/notes/cells/HYPERPLANE-SCREEN.json @@ -0,0 +1,4885 @@ +{ + "seconds": 6.709743600000365, + "source_sha256": "b0b9ffd88347cc8c8662fab3d28f65a50bca3d7e98a1337fbaf8c898303201db", + "results": [ + { + "group": 627, + "lambda_": 1, + "helpers": [ + 627, + 629, + 630, + 631 + ], + "indices": [ + 403, + 405, + 406, + 407 + ], + "before": [ + 390, + 68, + 34, + 24, + 1 + ], + "after": [ + 68, + 34, + 24, + 1 + ], + "frames": [ + [ + "B", + 384 + ], + [ + "B", + 385 + ], + [ + "B", + 386 + ], + [ + "B", + 387 + ], + [ + "B", + 388 + ], + [ + "B", + 389 + ], + [ + "B", + 390 + ], + [ + "B", + 391 + ], + [ + "B", + 392 + ], + [ + "B", + 393 + ], + [ + "B", + 394 + ], + [ + "B", + 395 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "e0514d0937e21c4feae283662ee8c2ea6cd7c2c92458512e63d4cbce5c668183", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 627, + "lambda_": 2, + "helpers": [ + 627, + 629, + 630, + 631 + ], + "indices": [ + 403, + 405, + 406, + 407 + ], + "before": [ + 390, + 68, + 34, + 24, + 1 + ], + "after": [ + 390, + 34, + 24, + 1 + ], + "frames": [ + [ + "B", + 384 + ], + [ + "B", + 385 + ], + [ + "B", + 386 + ], + [ + "B", + 387 + ], + [ + "B", + 388 + ], + [ + "B", + 389 + ], + [ + "B", + 390 + ], + [ + "B", + 391 + ], + [ + "B", + 392 + ], + [ + "B", + 393 + ], + [ + "B", + 394 + ], + [ + "B", + 395 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "c9673bfd5907d34adf278332daba8650a2d0d94e3763793ca128fe5f572c6bef", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 627, + "lambda_": 3, + "helpers": [ + 627, + 629, + 630, + 631 + ], + "indices": [ + 403, + 405, + 406, + 407 + ], + "before": [ + 390, + 68, + 34, + 24, + 1 + ], + "after": [ + 450, + 34, + 24, + 1 + ], + "frames": [ + [ + "B", + 384 + ], + [ + "B", + 385 + ], + [ + "B", + 386 + ], + [ + "B", + 387 + ], + [ + "B", + 388 + ], + [ + "B", + 389 + ], + [ + "B", + 390 + ], + [ + "B", + 391 + ], + [ + "B", + 392 + ], + [ + "B", + 393 + ], + [ + "B", + 394 + ], + [ + "B", + 395 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "83473e33ab74681acb5655c270bee1240dbd9be6a681d8992e51ded674ab68b1", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 627, + "lambda_": 4, + "helpers": [ + 627, + 629, + 630, + 631 + ], + "indices": [ + 403, + 405, + 406, + 407 + ], + "before": [ + 390, + 68, + 34, + 24, + 1 + ], + "after": [ + 390, + 68, + 24, + 1 + ], + "frames": [ + [ + "B", + 384 + ], + [ + "B", + 385 + ], + [ + "B", + 386 + ], + [ + "B", + 387 + ], + [ + "B", + 388 + ], + [ + "B", + 389 + ], + [ + "B", + 390 + ], + [ + "B", + 391 + ], + [ + "B", + 392 + ], + [ + "B", + 393 + ], + [ + "B", + 394 + ], + [ + "B", + 395 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "b701d7d9a705d0cd2b1edbefeec7c08c04798a00d4a422cf813c9f7bdb29f91f", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 627, + "lambda_": 5, + "helpers": [ + 627, + 629, + 630, + 631 + ], + "indices": [ + 403, + 405, + 406, + 407 + ], + "before": [ + 390, + 68, + 34, + 24, + 1 + ], + "after": [ + 420, + 68, + 24, + 1 + ], + "frames": [ + [ + "B", + 384 + ], + [ + "B", + 385 + ], + [ + "B", + 386 + ], + [ + "B", + 387 + ], + [ + "B", + 388 + ], + [ + "B", + 389 + ], + [ + "B", + 390 + ], + [ + "B", + 391 + ], + [ + "B", + 392 + ], + [ + "B", + 393 + ], + [ + "B", + 394 + ], + [ + "B", + 395 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "99424a779ac31d91f01b5ca6f8118d3805758d77eafd0562709aa4275d4ab2ff", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 627, + "lambda_": 6, + "helpers": [ + 627, + 629, + 630, + 631 + ], + "indices": [ + 403, + 405, + 406, + 407 + ], + "before": [ + 390, + 68, + 34, + 24, + 1 + ], + "after": [ + 390, + 102, + 24, + 1 + ], + "frames": [ + [ + "B", + 384 + ], + [ + "B", + 385 + ], + [ + "B", + 386 + ], + [ + "B", + 387 + ], + [ + "B", + 388 + ], + [ + "B", + 389 + ], + [ + "B", + 390 + ], + [ + "B", + 391 + ], + [ + "B", + 392 + ], + [ + "B", + 393 + ], + [ + "B", + 394 + ], + [ + "B", + 395 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "a3aafc12fbc966b92bfff559af5c6bb0b310e4fcab8f34185d91e8f97cf6a0a8", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 627, + "lambda_": 7, + "helpers": [ + 627, + 629, + 630, + 631 + ], + "indices": [ + 403, + 405, + 406, + 407 + ], + "before": [ + 390, + 68, + 34, + 24, + 1 + ], + "after": [ + 420, + 102, + 24, + 1 + ], + "frames": [ + [ + "B", + 384 + ], + [ + "B", + 385 + ], + [ + "B", + 386 + ], + [ + "B", + 387 + ], + [ + "B", + 388 + ], + [ + "B", + 389 + ], + [ + "B", + 390 + ], + [ + "B", + 391 + ], + [ + "B", + 392 + ], + [ + "B", + 393 + ], + [ + "B", + 394 + ], + [ + "B", + 395 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "94a107a3482af4371d4ddc24b950478c7b76d4a41b12d4daadb997348628ff5f", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 627, + "lambda_": 8, + "status": "nonmonotone", + "reason": "('nest', 624, (24,), (390, 68, 34, 1))" + }, + { + "group": 627, + "lambda_": 9, + "status": "nonmonotone", + "reason": "('nest', 624, (24,), (414, 68, 34, 1))" + }, + { + "group": 627, + "lambda_": 10, + "status": "nonmonotone", + "reason": "('nest', 624, (24,), (390, 92, 34, 1))" + }, + { + "group": 627, + "lambda_": 11, + "status": "nonmonotone", + "reason": "('nest', 624, (24,), (414, 92, 34, 1))" + }, + { + "group": 627, + "lambda_": 12, + "status": "nonmonotone", + "reason": "('nest', 624, (24,), (390, 68, 58, 1))" + }, + { + "group": 627, + "lambda_": 13, + "status": "nonmonotone", + "reason": "('nest', 624, (24,), (414, 68, 58, 1))" + }, + { + "group": 627, + "lambda_": 14, + "status": "nonmonotone", + "reason": "('nest', 624, (24,), (390, 92, 58, 1))" + }, + { + "group": 627, + "lambda_": 15, + "status": "nonmonotone", + "reason": "('nest', 624, (24,), (414, 92, 58, 1))" + }, + { + "group": 627, + "lambda_": 16, + "helpers": [ + 627, + 629, + 630, + 631 + ], + "indices": [ + 403, + 405, + 406, + 407 + ], + "before": [ + 390, + 68, + 34, + 24, + 1 + ], + "after": [ + 390, + 68, + 34, + 24 + ], + "frames": [ + [ + "B", + 384 + ], + [ + "B", + 385 + ], + [ + "B", + 386 + ], + [ + "B", + 387 + ], + [ + "B", + 388 + ], + [ + "B", + 389 + ], + [ + "B", + 390 + ], + [ + "B", + 391 + ], + [ + "B", + 392 + ], + [ + "B", + 393 + ], + [ + "B", + 394 + ], + [ + "B", + 395 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "f2d6dabb64f8030e388bc8396b48a41bc225700f8f641c675614d473c08c7c63", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 627, + "lambda_": 17, + "helpers": [ + 627, + 629, + 630, + 631 + ], + "indices": [ + 403, + 405, + 406, + 407 + ], + "before": [ + 390, + 68, + 34, + 24, + 1 + ], + "after": [ + 391, + 68, + 34, + 24 + ], + "frames": [ + [ + "B", + 384 + ], + [ + "B", + 385 + ], + [ + "B", + 386 + ], + [ + "B", + 387 + ], + [ + "B", + 388 + ], + [ + "B", + 389 + ], + [ + "B", + 390 + ], + [ + "B", + 391 + ], + [ + "B", + 392 + ], + [ + "B", + 393 + ], + [ + "B", + 394 + ], + [ + "B", + 395 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "fc7ac3230a95aa3853a42a457c7b314d45bdc375f8af744660213d4b910cc489", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 627, + "lambda_": 18, + "helpers": [ + 627, + 629, + 630, + 631 + ], + "indices": [ + 403, + 405, + 406, + 407 + ], + "before": [ + 390, + 68, + 34, + 24, + 1 + ], + "after": [ + 390, + 69, + 34, + 24 + ], + "frames": [ + [ + "B", + 384 + ], + [ + "B", + 385 + ], + [ + "B", + 386 + ], + [ + "B", + 387 + ], + [ + "B", + 388 + ], + [ + "B", + 389 + ], + [ + "B", + 390 + ], + [ + "B", + 391 + ], + [ + "B", + 392 + ], + [ + "B", + 393 + ], + [ + "B", + 394 + ], + [ + "B", + 395 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "64b409b5eb9084c152665779044623fbad0d67ff9d64b575c5d05f2b23374ae6", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 627, + "lambda_": 19, + "helpers": [ + 627, + 629, + 630, + 631 + ], + "indices": [ + 403, + 405, + 406, + 407 + ], + "before": [ + 390, + 68, + 34, + 24, + 1 + ], + "after": [ + 391, + 69, + 34, + 24 + ], + "frames": [ + [ + "B", + 384 + ], + [ + "B", + 385 + ], + [ + "B", + 386 + ], + [ + "B", + 387 + ], + [ + "B", + 388 + ], + [ + "B", + 389 + ], + [ + "B", + 390 + ], + [ + "B", + 391 + ], + [ + "B", + 392 + ], + [ + "B", + 393 + ], + [ + "B", + 394 + ], + [ + "B", + 395 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "b291c41e41b07544201f74497b7b441efed0be7eaeb27374d41751d858c9f31b", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 627, + "lambda_": 20, + "helpers": [ + 627, + 629, + 630, + 631 + ], + "indices": [ + 403, + 405, + 406, + 407 + ], + "before": [ + 390, + 68, + 34, + 24, + 1 + ], + "after": [ + 390, + 68, + 35, + 24 + ], + "frames": [ + [ + "B", + 384 + ], + [ + "B", + 385 + ], + [ + "B", + 386 + ], + [ + "B", + 387 + ], + [ + "B", + 388 + ], + [ + "B", + 389 + ], + [ + "B", + 390 + ], + [ + "B", + 391 + ], + [ + "B", + 392 + ], + [ + "B", + 393 + ], + [ + "B", + 394 + ], + [ + "B", + 395 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "ea40305ca173932ecbefd346d34809606a4d04fac39ac9471782e215952d1036", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 627, + "lambda_": 21, + "helpers": [ + 627, + 629, + 630, + 631 + ], + "indices": [ + 403, + 405, + 406, + 407 + ], + "before": [ + 390, + 68, + 34, + 24, + 1 + ], + "after": [ + 391, + 68, + 35, + 24 + ], + "frames": [ + [ + "B", + 384 + ], + [ + "B", + 385 + ], + [ + "B", + 386 + ], + [ + "B", + 387 + ], + [ + "B", + 388 + ], + [ + "B", + 389 + ], + [ + "B", + 390 + ], + [ + "B", + 391 + ], + [ + "B", + 392 + ], + [ + "B", + 393 + ], + [ + "B", + 394 + ], + [ + "B", + 395 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "c3761f64b9598a2bdbb343097031e85dc8cef25ec1939260ed379589054ce395", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 627, + "lambda_": 22, + "helpers": [ + 627, + 629, + 630, + 631 + ], + "indices": [ + 403, + 405, + 406, + 407 + ], + "before": [ + 390, + 68, + 34, + 24, + 1 + ], + "after": [ + 390, + 69, + 35, + 24 + ], + "frames": [ + [ + "B", + 384 + ], + [ + "B", + 385 + ], + [ + "B", + 386 + ], + [ + "B", + 387 + ], + [ + "B", + 388 + ], + [ + "B", + 389 + ], + [ + "B", + 390 + ], + [ + "B", + 391 + ], + [ + "B", + 392 + ], + [ + "B", + 393 + ], + [ + "B", + 394 + ], + [ + "B", + 395 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "720759e5e8b4ed5af1702377191180c9f6124434872ef3e8fea8169bd5d1150d", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 627, + "lambda_": 23, + "helpers": [ + 627, + 629, + 630, + 631 + ], + "indices": [ + 403, + 405, + 406, + 407 + ], + "before": [ + 390, + 68, + 34, + 24, + 1 + ], + "after": [ + 391, + 69, + 35, + 24 + ], + "frames": [ + [ + "B", + 384 + ], + [ + "B", + 385 + ], + [ + "B", + 386 + ], + [ + "B", + 387 + ], + [ + "B", + 388 + ], + [ + "B", + 389 + ], + [ + "B", + 390 + ], + [ + "B", + 391 + ], + [ + "B", + 392 + ], + [ + "B", + 393 + ], + [ + "B", + 394 + ], + [ + "B", + 395 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "e96605dc16841fce57266ddff099a869e5e83c58d7c7404aeef67e266c7e39c7", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 627, + "lambda_": 24, + "status": "nonmonotone", + "reason": "('nest', 624, (24,), (390, 68, 34, 25))" + }, + { + "group": 627, + "lambda_": 25, + "status": "nonmonotone", + "reason": "('nest', 624, (24,), (391, 68, 34, 25))" + }, + { + "group": 627, + "lambda_": 26, + "status": "nonmonotone", + "reason": "('nest', 624, (24,), (390, 69, 34, 25))" + }, + { + "group": 627, + "lambda_": 27, + "status": "nonmonotone", + "reason": "('nest', 624, (24,), (391, 69, 34, 25))" + }, + { + "group": 627, + "lambda_": 28, + "status": "nonmonotone", + "reason": "('nest', 624, (24,), (390, 68, 35, 25))" + }, + { + "group": 627, + "lambda_": 29, + "status": "nonmonotone", + "reason": "('nest', 624, (24,), (391, 68, 35, 25))" + }, + { + "group": 627, + "lambda_": 30, + "status": "nonmonotone", + "reason": "('nest', 624, (24,), (390, 69, 35, 25))" + }, + { + "group": 627, + "lambda_": 31, + "status": "nonmonotone", + "reason": "('nest', 624, (24,), (391, 69, 35, 25))" + }, + { + "group": 635, + "lambda_": 1, + "helpers": [ + 635, + 637, + 638, + 639 + ], + "indices": [ + 411, + 413, + 414, + 415 + ], + "before": [ + 298, + 170, + 102, + 30, + 1 + ], + "after": [ + 170, + 102, + 30, + 1 + ], + "frames": [ + [ + "B", + 372 + ], + [ + "B", + 373 + ], + [ + "B", + 374 + ], + [ + "B", + 375 + ], + [ + "B", + 376 + ], + [ + "B", + 377 + ], + [ + "B", + 378 + ], + [ + "B", + 379 + ], + [ + "B", + 380 + ], + [ + "B", + 381 + ], + [ + "B", + 382 + ], + [ + "B", + 383 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "05ad720ee236d6b6e51095c3b5ff8df2e8c8a524d83b1439d05268730c127457", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 635, + "lambda_": 2, + "helpers": [ + 635, + 637, + 638, + 639 + ], + "indices": [ + 411, + 413, + 414, + 415 + ], + "before": [ + 298, + 170, + 102, + 30, + 1 + ], + "after": [ + 298, + 102, + 30, + 1 + ], + "frames": [ + [ + "B", + 372 + ], + [ + "B", + 373 + ], + [ + "B", + 374 + ], + [ + "B", + 375 + ], + [ + "B", + 376 + ], + [ + "B", + 377 + ], + [ + "B", + 378 + ], + [ + "B", + 379 + ], + [ + "B", + 380 + ], + [ + "B", + 381 + ], + [ + "B", + 382 + ], + [ + "B", + 383 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "ab7e2396f58655479ae201b35942676710b393007c9ec94252b992ad39915902", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 635, + "lambda_": 3, + "helpers": [ + 635, + 637, + 638, + 639 + ], + "indices": [ + 411, + 413, + 414, + 415 + ], + "before": [ + 298, + 170, + 102, + 30, + 1 + ], + "after": [ + 384, + 102, + 30, + 1 + ], + "frames": [ + [ + "B", + 372 + ], + [ + "B", + 373 + ], + [ + "B", + 374 + ], + [ + "B", + 375 + ], + [ + "B", + 376 + ], + [ + "B", + 377 + ], + [ + "B", + 378 + ], + [ + "B", + 379 + ], + [ + "B", + 380 + ], + [ + "B", + 381 + ], + [ + "B", + 382 + ], + [ + "B", + 383 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "15e424fb570799ef7dc2d13827394ebc95c64b24e32886dd754f76c8840ef9ab", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 635, + "lambda_": 4, + "helpers": [ + 635, + 637, + 638, + 639 + ], + "indices": [ + 411, + 413, + 414, + 415 + ], + "before": [ + 298, + 170, + 102, + 30, + 1 + ], + "after": [ + 298, + 170, + 30, + 1 + ], + "frames": [ + [ + "B", + 372 + ], + [ + "B", + 373 + ], + [ + "B", + 374 + ], + [ + "B", + 375 + ], + [ + "B", + 376 + ], + [ + "B", + 377 + ], + [ + "B", + 378 + ], + [ + "B", + 379 + ], + [ + "B", + 380 + ], + [ + "B", + 381 + ], + [ + "B", + 382 + ], + [ + "B", + 383 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "0b2e4ec789b4a10c43d7ceecc945c36a2de9575ef5a379b86150d0497bd377d4", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 635, + "lambda_": 5, + "helpers": [ + 635, + 637, + 638, + 639 + ], + "indices": [ + 411, + 413, + 414, + 415 + ], + "before": [ + 298, + 170, + 102, + 30, + 1 + ], + "after": [ + 332, + 170, + 30, + 1 + ], + "frames": [ + [ + "B", + 372 + ], + [ + "B", + 373 + ], + [ + "B", + 374 + ], + [ + "B", + 375 + ], + [ + "B", + 376 + ], + [ + "B", + 377 + ], + [ + "B", + 378 + ], + [ + "B", + 379 + ], + [ + "B", + 380 + ], + [ + "B", + 381 + ], + [ + "B", + 382 + ], + [ + "B", + 383 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "eeda863b22eee97205fcc47f0f36b42ac79cd365bfe9c60df5ab97de1d0eb3a6", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 635, + "lambda_": 6, + "helpers": [ + 635, + 637, + 638, + 639 + ], + "indices": [ + 411, + 413, + 414, + 415 + ], + "before": [ + 298, + 170, + 102, + 30, + 1 + ], + "after": [ + 298, + 204, + 30, + 1 + ], + "frames": [ + [ + "B", + 372 + ], + [ + "B", + 373 + ], + [ + "B", + 374 + ], + [ + "B", + 375 + ], + [ + "B", + 376 + ], + [ + "B", + 377 + ], + [ + "B", + 378 + ], + [ + "B", + 379 + ], + [ + "B", + 380 + ], + [ + "B", + 381 + ], + [ + "B", + 382 + ], + [ + "B", + 383 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "799d1f796074385faccfbc3b7e87bd29af7bc7e96758571ed617d57fde3a6550", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 635, + "lambda_": 7, + "helpers": [ + 635, + 637, + 638, + 639 + ], + "indices": [ + 411, + 413, + 414, + 415 + ], + "before": [ + 298, + 170, + 102, + 30, + 1 + ], + "after": [ + 332, + 204, + 30, + 1 + ], + "frames": [ + [ + "B", + 372 + ], + [ + "B", + 373 + ], + [ + "B", + 374 + ], + [ + "B", + 375 + ], + [ + "B", + 376 + ], + [ + "B", + 377 + ], + [ + "B", + 378 + ], + [ + "B", + 379 + ], + [ + "B", + 380 + ], + [ + "B", + 381 + ], + [ + "B", + 382 + ], + [ + "B", + 383 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "0ffcddaf794470499027eba6e74c8a776f7fa4f6c6ad12532385dc3ef136a4f1", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 635, + "lambda_": 8, + "status": "nonmonotone", + "reason": "('nest', 632, (30,), (298, 170, 102, 1))" + }, + { + "group": 635, + "lambda_": 9, + "status": "nonmonotone", + "reason": "('nest', 632, (30,), (308, 170, 102, 1))" + }, + { + "group": 635, + "lambda_": 10, + "status": "nonmonotone", + "reason": "('nest', 632, (30,), (298, 180, 102, 1))" + }, + { + "group": 635, + "lambda_": 11, + "status": "nonmonotone", + "reason": "('nest', 632, (30,), (308, 180, 102, 1))" + }, + { + "group": 635, + "lambda_": 12, + "status": "nonmonotone", + "reason": "('nest', 632, (30,), (298, 170, 120, 1))" + }, + { + "group": 635, + "lambda_": 13, + "status": "nonmonotone", + "reason": "('nest', 632, (30,), (308, 170, 120, 1))" + }, + { + "group": 635, + "lambda_": 14, + "status": "nonmonotone", + "reason": "('nest', 632, (30,), (298, 180, 120, 1))" + }, + { + "group": 635, + "lambda_": 15, + "status": "nonmonotone", + "reason": "('nest', 632, (30,), (308, 180, 120, 1))" + }, + { + "group": 635, + "lambda_": 16, + "helpers": [ + 635, + 637, + 638, + 639 + ], + "indices": [ + 411, + 413, + 414, + 415 + ], + "before": [ + 298, + 170, + 102, + 30, + 1 + ], + "after": [ + 298, + 170, + 102, + 30 + ], + "frames": [ + [ + "B", + 372 + ], + [ + "B", + 373 + ], + [ + "B", + 374 + ], + [ + "B", + 375 + ], + [ + "B", + 376 + ], + [ + "B", + 377 + ], + [ + "B", + 378 + ], + [ + "B", + 379 + ], + [ + "B", + 380 + ], + [ + "B", + 381 + ], + [ + "B", + 382 + ], + [ + "B", + 383 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "40d1b40e834cec8f8f69a7e6853893b54f696baa5f946bee6b16c808d929dcb0", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 635, + "lambda_": 17, + "helpers": [ + 635, + 637, + 638, + 639 + ], + "indices": [ + 411, + 413, + 414, + 415 + ], + "before": [ + 298, + 170, + 102, + 30, + 1 + ], + "after": [ + 299, + 170, + 102, + 30 + ], + "frames": [ + [ + "B", + 372 + ], + [ + "B", + 373 + ], + [ + "B", + 374 + ], + [ + "B", + 375 + ], + [ + "B", + 376 + ], + [ + "B", + 377 + ], + [ + "B", + 378 + ], + [ + "B", + 379 + ], + [ + "B", + 380 + ], + [ + "B", + 381 + ], + [ + "B", + 382 + ], + [ + "B", + 383 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "932aae94aafdedf21ec6ab7e710d7d4780e05d1311fbdd26a77dd1cc29dddd79", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 635, + "lambda_": 18, + "helpers": [ + 635, + 637, + 638, + 639 + ], + "indices": [ + 411, + 413, + 414, + 415 + ], + "before": [ + 298, + 170, + 102, + 30, + 1 + ], + "after": [ + 298, + 171, + 102, + 30 + ], + "frames": [ + [ + "B", + 372 + ], + [ + "B", + 373 + ], + [ + "B", + 374 + ], + [ + "B", + 375 + ], + [ + "B", + 376 + ], + [ + "B", + 377 + ], + [ + "B", + 378 + ], + [ + "B", + 379 + ], + [ + "B", + 380 + ], + [ + "B", + 381 + ], + [ + "B", + 382 + ], + [ + "B", + 383 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "dd00dd90c1223bed3fd6257d2254597fcf859a7bbdbcd76dce298d1a854b9a7e", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 635, + "lambda_": 19, + "helpers": [ + 635, + 637, + 638, + 639 + ], + "indices": [ + 411, + 413, + 414, + 415 + ], + "before": [ + 298, + 170, + 102, + 30, + 1 + ], + "after": [ + 299, + 171, + 102, + 30 + ], + "frames": [ + [ + "B", + 372 + ], + [ + "B", + 373 + ], + [ + "B", + 374 + ], + [ + "B", + 375 + ], + [ + "B", + 376 + ], + [ + "B", + 377 + ], + [ + "B", + 378 + ], + [ + "B", + 379 + ], + [ + "B", + 380 + ], + [ + "B", + 381 + ], + [ + "B", + 382 + ], + [ + "B", + 383 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "f69d303c8b6b784557117c12e6d8eb0b2018b2a12cc97ba0637b014495605494", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 635, + "lambda_": 20, + "helpers": [ + 635, + 637, + 638, + 639 + ], + "indices": [ + 411, + 413, + 414, + 415 + ], + "before": [ + 298, + 170, + 102, + 30, + 1 + ], + "after": [ + 298, + 170, + 103, + 30 + ], + "frames": [ + [ + "B", + 372 + ], + [ + "B", + 373 + ], + [ + "B", + 374 + ], + [ + "B", + 375 + ], + [ + "B", + 376 + ], + [ + "B", + 377 + ], + [ + "B", + 378 + ], + [ + "B", + 379 + ], + [ + "B", + 380 + ], + [ + "B", + 381 + ], + [ + "B", + 382 + ], + [ + "B", + 383 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "69cc791440c14be3e2d02389558639d4583c79558ea1550ba4c7196e0ece135a", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 635, + "lambda_": 21, + "helpers": [ + 635, + 637, + 638, + 639 + ], + "indices": [ + 411, + 413, + 414, + 415 + ], + "before": [ + 298, + 170, + 102, + 30, + 1 + ], + "after": [ + 299, + 170, + 103, + 30 + ], + "frames": [ + [ + "B", + 372 + ], + [ + "B", + 373 + ], + [ + "B", + 374 + ], + [ + "B", + 375 + ], + [ + "B", + 376 + ], + [ + "B", + 377 + ], + [ + "B", + 378 + ], + [ + "B", + 379 + ], + [ + "B", + 380 + ], + [ + "B", + 381 + ], + [ + "B", + 382 + ], + [ + "B", + 383 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "d68e84b6e20e6c2c483ff83c9a21d657af85aa859850c9e9bd39e934e2d05d38", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 635, + "lambda_": 22, + "helpers": [ + 635, + 637, + 638, + 639 + ], + "indices": [ + 411, + 413, + 414, + 415 + ], + "before": [ + 298, + 170, + 102, + 30, + 1 + ], + "after": [ + 298, + 171, + 103, + 30 + ], + "frames": [ + [ + "B", + 372 + ], + [ + "B", + 373 + ], + [ + "B", + 374 + ], + [ + "B", + 375 + ], + [ + "B", + 376 + ], + [ + "B", + 377 + ], + [ + "B", + 378 + ], + [ + "B", + 379 + ], + [ + "B", + 380 + ], + [ + "B", + 381 + ], + [ + "B", + 382 + ], + [ + "B", + 383 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "a312572e010e05784c5ae6a3f732598a9945350fd4608a9dda4c7047f5f04a8d", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 635, + "lambda_": 23, + "helpers": [ + 635, + 637, + 638, + 639 + ], + "indices": [ + 411, + 413, + 414, + 415 + ], + "before": [ + 298, + 170, + 102, + 30, + 1 + ], + "after": [ + 299, + 171, + 103, + 30 + ], + "frames": [ + [ + "B", + 372 + ], + [ + "B", + 373 + ], + [ + "B", + 374 + ], + [ + "B", + 375 + ], + [ + "B", + 376 + ], + [ + "B", + 377 + ], + [ + "B", + 378 + ], + [ + "B", + 379 + ], + [ + "B", + 380 + ], + [ + "B", + 381 + ], + [ + "B", + 382 + ], + [ + "B", + 383 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "dae10958f14f8407d46e734c68ee6d3bdd80a2400c67e977b1ecc7a1c465947c", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 635, + "lambda_": 24, + "status": "nonmonotone", + "reason": "('nest', 632, (30,), (298, 170, 102, 31))" + }, + { + "group": 635, + "lambda_": 25, + "status": "nonmonotone", + "reason": "('nest', 632, (30,), (299, 170, 102, 31))" + }, + { + "group": 635, + "lambda_": 26, + "status": "nonmonotone", + "reason": "('nest', 632, (30,), (298, 171, 102, 31))" + }, + { + "group": 635, + "lambda_": 27, + "status": "nonmonotone", + "reason": "('nest', 632, (30,), (299, 171, 102, 31))" + }, + { + "group": 635, + "lambda_": 28, + "status": "nonmonotone", + "reason": "('nest', 632, (30,), (298, 170, 103, 31))" + }, + { + "group": 635, + "lambda_": 29, + "status": "nonmonotone", + "reason": "('nest', 632, (30,), (299, 170, 103, 31))" + }, + { + "group": 635, + "lambda_": 30, + "status": "nonmonotone", + "reason": "('nest', 632, (30,), (298, 171, 103, 31))" + }, + { + "group": 635, + "lambda_": 31, + "status": "nonmonotone", + "reason": "('nest', 632, (30,), (299, 171, 103, 31))" + }, + { + "group": 651, + "lambda_": 1, + "helpers": [ + 651, + 653, + 654, + 655 + ], + "indices": [ + 427, + 429, + 430, + 431 + ], + "before": [ + 267, + 139, + 96, + 25, + 7 + ], + "after": [ + 139, + 96, + 25, + 7 + ], + "frames": [ + [ + "B", + 432 + ], + [ + "B", + 433 + ], + [ + "B", + 434 + ], + [ + "B", + 435 + ], + [ + "B", + 436 + ], + [ + "B", + 437 + ], + [ + "B", + 438 + ], + [ + "B", + 439 + ], + [ + "B", + 440 + ], + [ + "B", + 441 + ], + [ + "B", + 442 + ], + [ + "B", + 443 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "7bd2ada25b6881a7fcf64d8875aa2e52f7a7537360efcc966053b20096aee21f", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 651, + "lambda_": 2, + "helpers": [ + 651, + 653, + 654, + 655 + ], + "indices": [ + 427, + 429, + 430, + 431 + ], + "before": [ + 267, + 139, + 96, + 25, + 7 + ], + "after": [ + 267, + 96, + 25, + 7 + ], + "frames": [ + [ + "B", + 432 + ], + [ + "B", + 433 + ], + [ + "B", + 434 + ], + [ + "B", + 435 + ], + [ + "B", + 436 + ], + [ + "B", + 437 + ], + [ + "B", + 438 + ], + [ + "B", + 439 + ], + [ + "B", + 440 + ], + [ + "B", + 441 + ], + [ + "B", + 442 + ], + [ + "B", + 443 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "fe0bfbeaed2ce6ece3349a0aa8f6dd545b450ada77be387a7a3f66e5b11cc9ce", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 651, + "lambda_": 3, + "helpers": [ + 651, + 653, + 654, + 655 + ], + "indices": [ + 427, + 429, + 430, + 431 + ], + "before": [ + 267, + 139, + 96, + 25, + 7 + ], + "after": [ + 384, + 96, + 25, + 7 + ], + "frames": [ + [ + "B", + 432 + ], + [ + "B", + 433 + ], + [ + "B", + 434 + ], + [ + "B", + 435 + ], + [ + "B", + 436 + ], + [ + "B", + 437 + ], + [ + "B", + 438 + ], + [ + "B", + 439 + ], + [ + "B", + 440 + ], + [ + "B", + 441 + ], + [ + "B", + 442 + ], + [ + "B", + 443 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "96898b17eb99edb5c22170e055fa1e5e98e7894f333d0cd66bc33b9ba68d75c5", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 651, + "lambda_": 4, + "helpers": [ + 651, + 653, + 654, + 655 + ], + "indices": [ + 427, + 429, + 430, + 431 + ], + "before": [ + 267, + 139, + 96, + 25, + 7 + ], + "after": [ + 267, + 139, + 25, + 7 + ], + "frames": [ + [ + "B", + 432 + ], + [ + "B", + 433 + ], + [ + "B", + 434 + ], + [ + "B", + 435 + ], + [ + "B", + 436 + ], + [ + "B", + 437 + ], + [ + "B", + 438 + ], + [ + "B", + 439 + ], + [ + "B", + 440 + ], + [ + "B", + 441 + ], + [ + "B", + 442 + ], + [ + "B", + 443 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "1809cd2bdffe9713fd6c26f1f90c6c56a6c6f29c1bc18430c7d0f6b2c6728e6a", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 651, + "lambda_": 5, + "helpers": [ + 651, + 653, + 654, + 655 + ], + "indices": [ + 427, + 429, + 430, + 431 + ], + "before": [ + 267, + 139, + 96, + 25, + 7 + ], + "after": [ + 363, + 139, + 25, + 7 + ], + "frames": [ + [ + "B", + 432 + ], + [ + "B", + 433 + ], + [ + "B", + 434 + ], + [ + "B", + 435 + ], + [ + "B", + 436 + ], + [ + "B", + 437 + ], + [ + "B", + 438 + ], + [ + "B", + 439 + ], + [ + "B", + 440 + ], + [ + "B", + 441 + ], + [ + "B", + 442 + ], + [ + "B", + 443 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "2cc6a31d107ac6079f3c5c9ffd7e8f86c67069f72b4f34f7895249f7221ea23a", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 651, + "lambda_": 6, + "helpers": [ + 651, + 653, + 654, + 655 + ], + "indices": [ + 427, + 429, + 430, + 431 + ], + "before": [ + 267, + 139, + 96, + 25, + 7 + ], + "after": [ + 267, + 235, + 25, + 7 + ], + "frames": [ + [ + "B", + 432 + ], + [ + "B", + 433 + ], + [ + "B", + 434 + ], + [ + "B", + 435 + ], + [ + "B", + 436 + ], + [ + "B", + 437 + ], + [ + "B", + 438 + ], + [ + "B", + 439 + ], + [ + "B", + 440 + ], + [ + "B", + 441 + ], + [ + "B", + 442 + ], + [ + "B", + 443 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "88bad88dd1e057d89d123fe9ed0013b5dd535125f2af08af3c61869d5963ed14", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 651, + "lambda_": 7, + "helpers": [ + 651, + 653, + 654, + 655 + ], + "indices": [ + 427, + 429, + 430, + 431 + ], + "before": [ + 267, + 139, + 96, + 25, + 7 + ], + "after": [ + 363, + 235, + 25, + 7 + ], + "frames": [ + [ + "B", + 432 + ], + [ + "B", + 433 + ], + [ + "B", + 434 + ], + [ + "B", + 435 + ], + [ + "B", + 436 + ], + [ + "B", + 437 + ], + [ + "B", + 438 + ], + [ + "B", + 439 + ], + [ + "B", + 440 + ], + [ + "B", + 441 + ], + [ + "B", + 442 + ], + [ + "B", + 443 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "79c78df4877e4caaf39cd53fca5f22ef1f4f2c5012835cdffaefc25b8dbd785b", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 651, + "lambda_": 8, + "status": "nonmonotone", + "reason": "('nest', 648, (30,), (267, 139, 96, 7))" + }, + { + "group": 651, + "lambda_": 9, + "status": "nonmonotone", + "reason": "('nest', 648, (30,), (274, 139, 96, 7))" + }, + { + "group": 651, + "lambda_": 10, + "status": "nonmonotone", + "reason": "('nest', 648, (30,), (267, 146, 96, 7))" + }, + { + "group": 651, + "lambda_": 11, + "status": "nonmonotone", + "reason": "('nest', 648, (30,), (274, 146, 96, 7))" + }, + { + "group": 651, + "lambda_": 12, + "status": "nonmonotone", + "reason": "('nest', 648, (30,), (267, 139, 121, 7))" + }, + { + "group": 651, + "lambda_": 13, + "status": "nonmonotone", + "reason": "('nest', 648, (30,), (274, 139, 121, 7))" + }, + { + "group": 651, + "lambda_": 14, + "status": "nonmonotone", + "reason": "('nest', 648, (30,), (267, 146, 121, 7))" + }, + { + "group": 651, + "lambda_": 15, + "status": "nonmonotone", + "reason": "('nest', 648, (30,), (274, 146, 121, 7))" + }, + { + "group": 651, + "lambda_": 16, + "status": "nonmonotone", + "reason": "('nest', 648, (30,), (267, 139, 96, 25))" + }, + { + "group": 651, + "lambda_": 17, + "status": "nonmonotone", + "reason": "('nest', 648, (30,), (268, 139, 96, 25))" + }, + { + "group": 651, + "lambda_": 18, + "status": "nonmonotone", + "reason": "('nest', 648, (30,), (267, 140, 96, 25))" + }, + { + "group": 651, + "lambda_": 19, + "status": "nonmonotone", + "reason": "('nest', 648, (30,), (268, 140, 96, 25))" + }, + { + "group": 651, + "lambda_": 20, + "status": "nonmonotone", + "reason": "('nest', 648, (30,), (267, 139, 103, 25))" + }, + { + "group": 651, + "lambda_": 21, + "status": "nonmonotone", + "reason": "('nest', 648, (30,), (268, 139, 103, 25))" + }, + { + "group": 651, + "lambda_": 22, + "status": "nonmonotone", + "reason": "('nest', 648, (30,), (267, 140, 103, 25))" + }, + { + "group": 651, + "lambda_": 23, + "status": "nonmonotone", + "reason": "('nest', 648, (30,), (268, 140, 103, 25))" + }, + { + "group": 651, + "lambda_": 24, + "helpers": [ + 651, + 653, + 654, + 655 + ], + "indices": [ + 427, + 429, + 430, + 431 + ], + "before": [ + 267, + 139, + 96, + 25, + 7 + ], + "after": [ + 267, + 139, + 96, + 30 + ], + "frames": [ + [ + "B", + 432 + ], + [ + "B", + 433 + ], + [ + "B", + 434 + ], + [ + "B", + 435 + ], + [ + "B", + 436 + ], + [ + "B", + 437 + ], + [ + "B", + 438 + ], + [ + "B", + 439 + ], + [ + "B", + 440 + ], + [ + "B", + 441 + ], + [ + "B", + 442 + ], + [ + "B", + 443 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "860a53d596f71926bcbf578ffb23f17cadd38c9a48f88b4056bcb20c52aafd1d", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 651, + "lambda_": 25, + "helpers": [ + 651, + 653, + 654, + 655 + ], + "indices": [ + 427, + 429, + 430, + 431 + ], + "before": [ + 267, + 139, + 96, + 25, + 7 + ], + "after": [ + 268, + 139, + 96, + 30 + ], + "frames": [ + [ + "B", + 432 + ], + [ + "B", + 433 + ], + [ + "B", + 434 + ], + [ + "B", + 435 + ], + [ + "B", + 436 + ], + [ + "B", + 437 + ], + [ + "B", + 438 + ], + [ + "B", + 439 + ], + [ + "B", + 440 + ], + [ + "B", + 441 + ], + [ + "B", + 442 + ], + [ + "B", + 443 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "df7d9d15e040eca0113d37f8628d8f75a32c5300f013a0fb1e44eeda0c4ea8dd", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 651, + "lambda_": 26, + "helpers": [ + 651, + 653, + 654, + 655 + ], + "indices": [ + 427, + 429, + 430, + 431 + ], + "before": [ + 267, + 139, + 96, + 25, + 7 + ], + "after": [ + 267, + 140, + 96, + 30 + ], + "frames": [ + [ + "B", + 432 + ], + [ + "B", + 433 + ], + [ + "B", + 434 + ], + [ + "B", + 435 + ], + [ + "B", + 436 + ], + [ + "B", + 437 + ], + [ + "B", + 438 + ], + [ + "B", + 439 + ], + [ + "B", + 440 + ], + [ + "B", + 441 + ], + [ + "B", + 442 + ], + [ + "B", + 443 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "f757812f7701b5e09758bfcbc0e344fd052c9b87b30b399c554ddafb05c8b93f", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 651, + "lambda_": 27, + "helpers": [ + 651, + 653, + 654, + 655 + ], + "indices": [ + 427, + 429, + 430, + 431 + ], + "before": [ + 267, + 139, + 96, + 25, + 7 + ], + "after": [ + 268, + 140, + 96, + 30 + ], + "frames": [ + [ + "B", + 432 + ], + [ + "B", + 433 + ], + [ + "B", + 434 + ], + [ + "B", + 435 + ], + [ + "B", + 436 + ], + [ + "B", + 437 + ], + [ + "B", + 438 + ], + [ + "B", + 439 + ], + [ + "B", + 440 + ], + [ + "B", + 441 + ], + [ + "B", + 442 + ], + [ + "B", + 443 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "23e041a2cef5d3a8427c2feb2e997d204fdca2089a53d69b242829e10a4619e4", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 651, + "lambda_": 28, + "helpers": [ + 651, + 653, + 654, + 655 + ], + "indices": [ + 427, + 429, + 430, + 431 + ], + "before": [ + 267, + 139, + 96, + 25, + 7 + ], + "after": [ + 267, + 139, + 103, + 30 + ], + "frames": [ + [ + "B", + 432 + ], + [ + "B", + 433 + ], + [ + "B", + 434 + ], + [ + "B", + 435 + ], + [ + "B", + 436 + ], + [ + "B", + 437 + ], + [ + "B", + 438 + ], + [ + "B", + 439 + ], + [ + "B", + 440 + ], + [ + "B", + 441 + ], + [ + "B", + 442 + ], + [ + "B", + 443 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "82475c88aeac311a2e05424a3197ba186f912ab5fe06727a991ed00f610ed86d", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 651, + "lambda_": 29, + "helpers": [ + 651, + 653, + 654, + 655 + ], + "indices": [ + 427, + 429, + 430, + 431 + ], + "before": [ + 267, + 139, + 96, + 25, + 7 + ], + "after": [ + 268, + 139, + 103, + 30 + ], + "frames": [ + [ + "B", + 432 + ], + [ + "B", + 433 + ], + [ + "B", + 434 + ], + [ + "B", + 435 + ], + [ + "B", + 436 + ], + [ + "B", + 437 + ], + [ + "B", + 438 + ], + [ + "B", + 439 + ], + [ + "B", + 440 + ], + [ + "B", + 441 + ], + [ + "B", + 442 + ], + [ + "B", + 443 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "675bf03e4f41d72ed357d09a1e2535c9b5f38609f70a4c09ba5475e4fe1dafa8", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 651, + "lambda_": 30, + "helpers": [ + 651, + 653, + 654, + 655 + ], + "indices": [ + 427, + 429, + 430, + 431 + ], + "before": [ + 267, + 139, + 96, + 25, + 7 + ], + "after": [ + 267, + 140, + 103, + 30 + ], + "frames": [ + [ + "B", + 432 + ], + [ + "B", + 433 + ], + [ + "B", + 434 + ], + [ + "B", + 435 + ], + [ + "B", + 436 + ], + [ + "B", + 437 + ], + [ + "B", + 438 + ], + [ + "B", + 439 + ], + [ + "B", + 440 + ], + [ + "B", + 441 + ], + [ + "B", + 442 + ], + [ + "B", + 443 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "702819037bfe5135efd96b89079c9c87fcb12685d66c605a5c23ca3046ddfd57", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + }, + { + "group": 651, + "lambda_": 31, + "helpers": [ + 651, + 653, + 654, + 655 + ], + "indices": [ + 427, + 429, + 430, + 431 + ], + "before": [ + 267, + 139, + 96, + 25, + 7 + ], + "after": [ + 268, + 140, + 103, + 30 + ], + "frames": [ + [ + "B", + 432 + ], + [ + "B", + 433 + ], + [ + "B", + 434 + ], + [ + "B", + 435 + ], + [ + "B", + 436 + ], + [ + "B", + 437 + ], + [ + "B", + 438 + ], + [ + "B", + 439 + ], + [ + "B", + 440 + ], + [ + "B", + 441 + ], + [ + "B", + 442 + ], + [ + "B", + 443 + ] + ], + "status": "framechains-pass", + "delta": { + "1": -8, + "4": -4, + "3": 4, + "2": 8 + }, + "with_four_rank1_gaps": { + "1": -12, + "4": -4, + "3": 4, + "2": 8 + }, + "nomination_moment_delta": -0.0035177796510819093, + "content_sha256": "1c15b8623703ef14d65743211ab9a5b65dfd734ff23631ac4bdf098030d40223", + "profile": { + "1": 2364, + "2": 502, + "3": 416, + "4": 126, + "5": 82, + "8": 8 + } + } + ], + "scope": "Complete31hyperplanes per remainingrank5island; onlywholemonotone framechain+momentnomination, nofullcone/globalprice yet." +} \ No newline at end of file diff --git a/research/crosscall-kernel-demotion/notes/cells/OPENAI-MECHANISMS.md b/research/crosscall-kernel-demotion/notes/cells/OPENAI-MECHANISMS.md new file mode 100644 index 0000000000..a43172ebc5 --- /dev/null +++ b/research/crosscall-kernel-demotion/notes/cells/OPENAI-MECHANISMS.md @@ -0,0 +1,39 @@ +# Two fresh OpenAI mechanisms used in the local extension + +The source snapshot is openai/math commit fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. Exact source hashes, declaration statements and line numbers are recorded in OPENAI-SOURCE-LEDGER.json. These sources were inspected; no new Lean build or kernel replay was run in this research round. + +## Coordinate-sector projection and complete hyperplane selection + +Source: `lean/OAI/RepresentationTheory/UniversalSquare/Specht/SplitFlag.lean`, declarations `OAI.Saxl.FlagColumns.coordinateProjection_pair` at line48 and `coordinateProjection_idempotent` at line57. Their finite coordinate masks are self-adjoint for the coefficient pairing and idempotent. A chosen sector is represented exactly by its membership predicate, rather than by a particular displayed list of generators. + +We apply that representation to entrance-frame labels. Fix an independent basis E=(v0,...,v4) of a five-dimensional F2 space. Every nonzero covector lambda gives a codimension-one sector U_lambda={sum c_i v_i : lambda dot c=0}. There are exactly31 such sectors. Conversely every four-dimensional subspace U of E has a one-dimensional annihilator in the dual; over F2 that annihilator has a unique nonzero element. Therefore enumerating lambda=1,...,31 enumerates every possible codimension-one entrance frame exactly once. + +The finite coordinate mask is a search/proof representation. It is NOT a free physical projection inserted into the multiplication circuit. The actual construction lowers literal entrance and common-gate frame annotations, keeps every scalar instruction unchanged, and pays the resulting residual and wrapper ranks. All physical correctness is established by the actual scalar/frame/phase audits described below. + +This distinction matters on island651. The prior deletion chose span(267,139,96,25), which does not contain the required previous frame direction30. The new sector is span(139,96,25,7); it contains30 because25 XOR7=30. Its common gates can therefore run at the smaller frame while retaining nesting. This is a concrete additional demotion island that the prior chosen basis deletion missed. + +The complete scout checked31 sectors on each of627/635/651:93 total. Each island has15 whole-chain-admitted candidates and16 rejected by nesting, for45 admitted candidates. The artifact HYPERPLANE-SCREEN.json records every covector and result. Completeness applies only to this precisely defined literal-frame class: lower that island's four entrances and all its old-E common A/B gates to a single codimension-one U, with the rest of the word fixed. The scout does not prove arbitrary-circuit optimality, global feasibility of every candidate, or a new kappa by itself. We selected one admitted sector per island and fully checked the resulting three joint prefix providers. + +## Transporters as independent colour-fibre bijections + +Source: `lean/OAI/LinearAlgebra/MatrixState/Postselection.lean`, `OAI.RowColumn.WordOrbits.transporterEquiv` at line15 and `card_transporters` at line37. The explicit equivalence identifies every colour-preserving permutation of finite labelled objects with independent bijections between the corresponding colour fibres. + +Here the objects are whole-helper roles, and the initial colour is the complete invocation and old residual width. A bijection within the width-four fibre of one call transports the entire physical owner label: replica, child, port, copy and family. It leaves the call time and old reserved rank unchanged and preserves distinct physical families. Thus selected newly widened roles can be moved into the width-four positions whose pending families contain one available coordinate. The remaining fibre is completed to an actual permutation, so no unchanged role disappears or duplicates. + +This supplies a sufficient constructive relocation rule once every chosen destination has the required extra unit, a valid active window and a complete disjoint chart. It does not infer feasibility from equal histograms alone. After the permutation, each changed width is increased4->5, all chronological offsets are rebuilt, and every remainder is debited. The actual owner checker must verify windows, disjoint physical factors and every73-axis chart. The independent owner worker constructs and checks that concrete map; an unknown matching gadget or unpaid coordinate is not assumed. + +The scalar block is unchanged and all four helper entrance-dirt responses vanish. Fresh exact wrapper checks therefore turn each changed residual into its actual five-coordinate transform and identity on the four spectators, including global phase. Together with the owner permutation and paid remainder, this gives the entire required pending transform under the inherited public hosting contract. + +## Concrete local providers + +The parent is the exact public PR1148 raw word, semantic hash b0b9ffd88347cc8c8662fab3d28f65a50bca3d7e98a1337fbaf8c898303201db. It already includes the three603/611/619 demotions and eight rank-seven ends. + +We add prefixes of627,635,651. All entrance and B-record annotation sets are explicitly disjoint. That fact only shows that literal edits commute; it does not establish a cost saving. Each complete joint word was independently reconstructed and recounted. For extra selector k=1,2,3 the measured local profile is + + (2372-8k) H1 +(494+8k) H2 +(412+4k) H3 +(130-4k) H4 +82 H5 +8 H8. + +The actual width inventory is (44-4k) width-four helpers, (44+4k) width-five,38 width-seven,114 width-eight and240 width-nine helpers. Each extra group uses four additional coordinates; the global owner map must pay all of them. + +Every new provider passed704 arbitrary-input columns in both orientations, all monotone frame chains, zero entrance-dirt response, every low-end inverse-row/dirty-column cone, native transport, both emitted local programs and25 corruption controls. All9k newly introduced directed phase edges and k changed residual wrappers passed fresh exact lowering and independently decoded tableau/zero-state equality, with10k global-phase mutations rejected. The parent native geometry was source-bound; its unchanged phases and endpoint adapters remain inherited from PR1148. + +The portable checker at three-extra-prefix/portable/check_local.py reconstructs the provider from the pinned full parent word and literal patches. Selector3 passed independently in16.14 seconds. Global owner/precision/outer pricing is handled separately; no advertised kappa gains are added. All-size/compiler, realization, tape/precision and analytic obligations remain explicit inherited premises. diff --git a/research/crosscall-kernel-demotion/notes/cells/OPENAI-SOURCE-LEDGER.json b/research/crosscall-kernel-demotion/notes/cells/OPENAI-SOURCE-LEDGER.json new file mode 100644 index 0000000000..c3f3066262 --- /dev/null +++ b/research/crosscall-kernel-demotion/notes/cells/OPENAI-SOURCE-LEDGER.json @@ -0,0 +1,44 @@ +[ + { + "source": "F:\\proof\\leanlibs-20261009\\openai-math-fd4aeeb2\\src\\lean\\OAI\\RepresentationTheory\\UniversalSquare\\Specht\\SplitFlag.lean", + "sha256": "fc9fe067365381c6c2fbb7fbd3d94ad7fbbdea44312fa9d1423fb0d4f78b2b08", + "declarations": [ + { + "name": "coordinateProjection_pair", + "line": 48, + "statement": "lemma coordinateProjection_pair {n d : \u2115} (P : (Fin n \u2192 Fin d) \u2192 Prop)\n (x y : WordSpace n d) :\n dotProduct (coordinateProjection P x) y = dotProduct x (coordinateProjection P y) := by" + }, + { + "name": "coordinateProjection_idempotent", + "line": 57, + "statement": "lemma coordinateProjection_idempotent {n d : \u2115} (P : (Fin n \u2192 Fin d) \u2192 Prop)\n (x : WordSpace n d) :\n coordinateProjection P (coordinateProjection P x) = coordinateProjection P x := by" + } + ], + "evidence": "Exact source inspected; no fresh Lean kernel replay in this research round", + "repository": "https://github.com/openai/math", + "commit": "fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb", + "repository_path": "lean/OAI/RepresentationTheory/UniversalSquare/Specht/SplitFlag.lean", + "source_url": "https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/RepresentationTheory/UniversalSquare/Specht/SplitFlag.lean" + }, + { + "source": "F:\\proof\\leanlibs-20261009\\openai-math-fd4aeeb2\\src\\lean\\OAI\\LinearAlgebra\\MatrixState\\Postselection.lean", + "sha256": "275bfb2ad70f8066ae6da4b25b9ca4b1b87af7c52774b57f95e9c156be5e9de5", + "declarations": [ + { + "name": "transporterEquiv", + "line": 15, + "statement": "def transporterEquiv (a b : S \u2192 A) :\n {p : Equiv.Perm S // \u2200 x, b (p x) = a x} \u2243\n (\u2200 c : A, {x : S // a x = c} \u2243 {x : S // b x = c}) where" + }, + { + "name": "card_transporters", + "line": 37, + "statement": "lemma card_transporters (a b : S \u2192 A) (he : counts a = counts b) :\n Fintype.card {p : Equiv.Perm S // \u2200 x, b (p x) = a x} =\n \u220f c : A, (Fintype.card {x : S // a x = c})! := by" + } + ], + "evidence": "Exact source inspected; no fresh Lean kernel replay in this research round", + "repository": "https://github.com/openai/math", + "commit": "fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb", + "repository_path": "lean/OAI/LinearAlgebra/MatrixState/Postselection.lean", + "source_url": "https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/LinearAlgebra/MatrixState/Postselection.lean" + } +] \ No newline at end of file diff --git a/research/crosscall-kernel-demotion/notes/cells/PR-SYNOPSIS.md b/research/crosscall-kernel-demotion/notes/cells/PR-SYNOPSIS.md new file mode 100644 index 0000000000..e827ff42f7 --- /dev/null +++ b/research/crosscall-kernel-demotion/notes/cells/PR-SYNOPSIS.md @@ -0,0 +1,18 @@ +# Full-body public sweep + +Frozen snapshot through PR1153. Read bodies1121..1131 and1148. These are published claims, not new independent certification. + +- [PR1121](https://github.com/CrocSwap/integer-mult-bounds/pull/1121): rank-seven ends on seven-slot k8, T16ownerpacking; reported0.001672965558289236. +- [PR1122](https://github.com/CrocSwap/integer-mult-bounds/pull/1122): R439 bitABCstar composition1062+980 saves848ADDs, profileunchanged: no kappa. +- [PR1123](https://github.com/CrocSwap/integer-mult-bounds/pull/1123): concave cost reversals between T16maps; scopedmajorization audit, no supplier. +- [PR1124](https://github.com/CrocSwap/integer-mult-bounds/pull/1124): eighth triangleX54 plusrank7ends,T16;0.001673005344598825. +- [PR1125](https://github.com/CrocSwap/integer-mult-bounds/pull/1125): P104 asynchronouscarrier width/costbound, no supplier. +- [PR1126](https://github.com/CrocSwap/integer-mult-bounds/pull/1126): 21ADDpositive-lift minimum alleightK8leaver cells; fixedendpointclass, no kappa. +- [PR1127](https://github.com/CrocSwap/integer-mult-bounds/pull/1127): 405Steinberg3to2bitzrewrites,810ADDs saved, sameframes/profile, no kappa. +- [PR1128](https://github.com/CrocSwap/integer-mult-bounds/pull/1128): bitwidth7restoration/dirtboundary obstruction, sixearlycandidatesnotconstructions. +- [PR1129](https://github.com/CrocSwap/integer-mult-bounds/pull/1129): attainingT37R480ownerflow+fixedinventorybound;0.001674097969905390. +- [PR1130](https://github.com/CrocSwap/integer-mult-bounds/pull/1130): X54+rank7endsT16repack;0.001673006105142741. +- [PR1131](https://github.com/CrocSwap/integer-mult-bounds/pull/1131): independentlyattains1129T37withdifferentcallorder/fullcoldreplay, samevalue. +- [PR1148](https://github.com/CrocSwap/integer-mult-bounds/pull/1148): 8rank7ends+12entrances5->4+refittedframes+T16packing;0.001675121647789207, hypotheticalceiling0.001675129371412064. + +Mostpromising localroute: reconstruct1148actualrawword, then combine remaining disjoint entrance islands using freshwhole-word profiling,704-column arbitrary-dirt/cone audits and changedphase/adapters. Do not add announced gains;1129/1146/1152owner words must match the exact changed widths. diff --git a/research/crosscall-kernel-demotion/notes/lead/OPENAI-MECHANISMS.md b/research/crosscall-kernel-demotion/notes/lead/OPENAI-MECHANISMS.md new file mode 100644 index 0000000000..966c53df9d --- /dev/null +++ b/research/crosscall-kernel-demotion/notes/lead/OPENAI-MECHANISMS.md @@ -0,0 +1,78 @@ +# Two distinct OpenAI mechanisms: root assembly worker + +These sources were inspected in the registered OpenAI math tree. The exact +repository paths, source hashes and declaration lines are in OPENAI-SOURCES.json. +This round does not compile Lean or assert a new kernel certificate. The source +collection is https://github.com/openai/math . + +## 1. CapacityScan: prefix checks have an exact complete-load meaning + +Source: OAI.Computability.BinPackingGap.CapacityScan.scan_eq_true_iff and +scan_initial_eq_true_iff_load, in +`lean/OAI/Computability/BinPacking/Packing/CapacityScan.lean`. +For valid nonnegative item widths, the early-rejecting scan accepts exactly when +the completed load of the labelled container does not exceed one. + +Adaptation: scale each physical child's capacity to its integer axis rank. For a +fixed literal final owner table, group role widths by actual physical identity +(owner replica, child, port). Scan those widths in execution order with pointer +s_0=0 and s_{j+1}=s_j+w_j. Accept iff all w_j are positive integers, each role's +saved offset is s_j, and s_k <= C. Positivity gives s_j <= s_k, so this is exactly +a sufficient nonoverlap/capacity certificate: the blocks [s_j,s_{j+1}) are +disjoint and contained in [0,C), and [s_k,C) is the one complete paid remainder. +The per-call family-uniqueness and inactivity-window checks remain separate and +mandatory. No scalar rank count licenses borrowing an active owner. + +This prevents a candidate's aggregate spare-rank count from being mistaken for a +physical construction. It also explains why end shrinkage must precede a fresh +scan of the final assignment rather than being added as a free gain. The literal +owner audit applies this sufficient scan, computes every remainder, and exposes +negative controls for wrong offsets and over-capacity loads. + +## 2. Arithmetic program composition preserves semantics and exact charged cost + +Source: Program.eval_mapInput / cost_mapInput, Program.eval_mapSource / +cost_mapSource, and Program.Substituted.correct / cost_eq, in +`lean/OAI/LinearAlgebra/MatrixMultiplication/Arithmetic/ProgramComposition.lean`. +Relabelling source inputs leaves a program's gate cost unchanged. Composing two +explicit programs through fixed wires has the stated composed semantics and +cost equal to the sum of the actual two gate costs. + +Adaptation: let P_{k,o} be the actual emitted local program of provider k in +orientation o. At call c, dispatch selects one k(c), and the whole-owner chart +supplies a fixed embedding of its input labels into physical coordinates. This +relabel does not erase any scalar gate of P_{k(c),o(c)}. For arbitrary initial +dirty data, the freshly checked provider contract gives its transformation and +restoration; composing through the exact embeddings is therefore sufficient for +the literal sequence of local calls. Its local primitive cost is + + sum_c primitive_count(P_{k(c),o(c)}). + +Wrappers, chart construction, dispatch, movement, parent work, recursive child +calls, precision and recovery are additional costs, not covered by a source +relabel. The fresh finite invoice charges these explicitly and adds the complete +new bill to the retained old allowance. All prefix, tape and row inequalities +must hold on this charged bill before the price can be delivered. + +This is the reason a call-dependent portfolio is legal without declaring all +providers to execute at every call. It supplies an exact sufficient composition, +not a weighted average of separately claimed kappa values. The complete positive +paid histogram, including every residual block, is then independently priced by +two exact rational engines and the retained strict outer recipe. + +## Frozen routes and early falsifiers + +The frontier was read through PR1153; PR1148 has the highest explicit construction +claim in that snapshot. PR1152's new T37 flow is a useful compatible stock source, +but the simple attempt to install PR1148 while preserving its rank-48 tails +fails the improvement test. Exact arithmetic screening gives +0.001672752546014868, below both PR1152 and PR1148. This says nothing about a +different actual T37 packing; it stops that one representation early. + +The selected route instead retains PR1148's concrete T16 table and admits extra +local demotions only at calls for which actual legal donor axes can be assigned. +The local worker enumerates codimension-one frames rather than assuming the last +basis vector is the only removable direction. Each selected provider must pass +fresh full-column, emitted-program and phase checks. The final owner witness, +complete profile and fresh invoice remain the sufficient assembly obligations. +No unchecked candidate receives a numerical gain. diff --git a/research/crosscall-kernel-demotion/notes/lead/OPENAI-SOURCES.json b/research/crosscall-kernel-demotion/notes/lead/OPENAI-SOURCES.json new file mode 100644 index 0000000000..be03f5b53a --- /dev/null +++ b/research/crosscall-kernel-demotion/notes/lead/OPENAI-SOURCES.json @@ -0,0 +1,48 @@ +[ + { + "repository_path": "lean/OAI/Computability/BinPacking/Packing/CapacityScan.lean", + "sha256": "4a715fae10561891c79121c3f5d31640a4456e45d03efaccf844dd37a6a363b2", + "declarations": [ + { + "line": 18, + "text": "theorem scan_eq_true_iff (label : Nat) (items : RawInstance)" + }, + { + "line": 58, + "text": "theorem scan_initial_eq_true_iff_load (label : Nat) (items : RawInstance)" + } + ], + "evidence": "SOURCE_INSPECTED; no fresh Lean kernel replay" + }, + { + "repository_path": "lean/OAI/LinearAlgebra/MatrixMultiplication/Arithmetic/ProgramComposition.lean", + "sha256": "f300f78c9825345a9cea31f049a1767483674ba9d966dc08bbac6b27804d8ccc", + "declarations": [ + { + "line": 30, + "text": "@[simp] theorem cost_mapInput (f : Input \u2192 Input') (g : Gate F Input Register) :" + }, + { + "line": 55, + "text": "@[simp] theorem cost_mapSource (f : Input \u2192 Input' \u2295 F) (g : Gate F Input Register) :" + }, + { + "line": 87, + "text": "@[simp] theorem cost_mapInput (f : Input \u2192 Input') {r : \u2115} (p : Program F Input r) :" + }, + { + "line": 111, + "text": "@[simp] theorem cost_mapSource (f : Input \u2192 Input' \u2295 F) {r : \u2115}" + }, + { + "line": 126, + "text": "cost_eq : program.cost = p.cost + q.cost" + }, + { + "line": 154, + "text": "def substitute {r : \u2115} (p : Program F Input r) :" + } + ], + "evidence": "SOURCE_INSPECTED; no fresh Lean kernel replay" + } +] diff --git a/research/crosscall-kernel-demotion/notes/owners/LAST-GROUP-SEARCH.json b/research/crosscall-kernel-demotion/notes/owners/LAST-GROUP-SEARCH.json new file mode 100644 index 0000000000..4d40dcf7e4 --- /dev/null +++ b/research/crosscall-kernel-demotion/notes/owners/LAST-GROUP-SEARCH.json @@ -0,0 +1,6 @@ +{ + "status": "NO_REALIZED_LAST_GROUP_WITHIN_BUDGET", + "seconds": 0.029277400000864873, + "attempts": 26768, + "witness": null +} diff --git a/research/crosscall-kernel-demotion/notes/owners/OPENAI-SOURCE-LEDGER.json b/research/crosscall-kernel-demotion/notes/owners/OPENAI-SOURCE-LEDGER.json new file mode 100644 index 0000000000..5c54755690 --- /dev/null +++ b/research/crosscall-kernel-demotion/notes/owners/OPENAI-SOURCE-LEDGER.json @@ -0,0 +1,34 @@ +{ + "status": "SOURCE_ADAPTATION_LEDGER_NO_NEW_LEAN_COMPILATION", + "mechanisms": [ + { + "source_path": "D:\\proof\\external\\openai-math\\lean\\OAI\\Combinatorics\\SecondNeighborhood\\MatchingExchange.lean", + "sha256": "d1e471048ffd97cb08e76aadf5d9ce8a2066c33ff41af45185ff3e11e5228411", + "theorems": [ + "OAI.SeymourSecondNeighborhood.Bipartite.exists_matching_saturating_left_of_card_lt", + "OAI.SeymourSecondNeighborhood.Bipartite.exists_matching_one_larger_saturating_left" + ], + "application": "Monotone whole-role cross-call augmentation with a literal matching of target roles to unit-slack donor slots. Previously installed prefix groups remain installed; four new literal width increases consume four distinct physical gaps. No global maximum-matching claim.", + "repository_relative_path": "lean/OAI/Combinatorics/SecondNeighborhood/MatchingExchange.lean", + "source_commit": "adc7f1241b42e322a6451854ab7e4b4c146bf78a", + "public_source_url": "https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/SecondNeighborhood/MatchingExchange.lean", + "source_revision_check": "Local sources match HEAD for these two files; source retrieval only, no new kernel verification." + }, + { + "source_path": "D:\\proof\\external\\openai-math\\lean\\OAI\\Computability\\BinPacking\\Inventory\\PhysicalPoolLift.lean", + "sha256": "f711bdddadfda7cf6b6f16b28f3596c57bbdbbaa6092f10ddc8fbaab75bdc50e", + "statements": [ + "OAI.BinPackingGap.PoolTemplates.base_global", + "OAI.BinPackingGap.PoolTemplates.base_flag", + "OAI.BinPackingGap.PoolTemplates.global_flag", + "OAI.BinPackingGap.PoolTemplates.capacity", + "OAI.BinPackingGap.PoolTemplates.template_coverage" + ], + "application": "A physical donor template consists of unchanged occupied coordinates, one four-axis borrowed block and one real unclaimed axis. Explicit disjointness/capacity is checked before each width-five installation; no fractional solution is asserted to be an integral owner map.", + "repository_relative_path": "lean/OAI/Computability/BinPacking/Inventory/PhysicalPoolLift.lean", + "source_commit": "adc7f1241b42e322a6451854ab7e4b4c146bf78a", + "public_source_url": "https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/BinPacking/Inventory/PhysicalPoolLift.lean", + "source_revision_check": "Local sources match HEAD for these two files; source retrieval only, no new kernel verification." + } + ] +} diff --git a/research/crosscall-kernel-demotion/notes/owners/OWNERS-PROOF.md b/research/crosscall-kernel-demotion/notes/owners/OWNERS-PROOF.md new file mode 100644 index 0000000000..2a616eacbb --- /dev/null +++ b/research/crosscall-kernel-demotion/notes/owners/OWNERS-PROOF.md @@ -0,0 +1,35 @@ +# Sufficient cross-call donor augmentation + +Fix the source-pinned PR1148 local provider, exact call order, pending-owner windows and physical phase charts. The three additional provider islands are ordered 627,635,651, with helper indices 403/405/406/407,411/413/414/415,427/429/430/431. Fresh concrete local replay checks each actual prefix k=1,2,3 on arbitrary dirty inputs in both orientations. Its width inventory changes exactly 4k roles from four to five and its complete local paid difference is kL, where L=-8H1+8H2+4H3-4H4. + +## Literal pair replacement + +Let role i at call t have width four and owner A; let role j at call u have width four and owner B. The sufficient conditions are: A and B are distinct physical families; A's window contains u and B's contains t; after removing these two roles neither incoming call collides with another use of its assigned family; and B has one actually unclaimed axis. Exchange the two owner labels, retain the role identities and call times, and increase only i's width to five. A's load is unchanged. B's load increases by one within its capacity. All other loads and roles stay fixed. If i already belongs to a unit-slack owner, leave its owner label unchanged and grow it directly. + +For a whole island, choose four different such gap families and install all four roles atomically. A failed attempted island restores its rows, loads and busy-family sets. An accepted island retains all previous prefix groups. Final offsets are rebuilt in chronological call/helper order. The role map therefore preserves every literal helper occurrence, per-call family uniqueness, inactive windows and disjoint coordinate blocks. The unchanged source-dependent local dirty-restoration contract composes on those explicit axes. This is a sufficient realization proof, not just a matching or capacity obstruction. + +The underlying target-to-donor-slot graph is bipartite. The OpenAI MatchingExchange theorem's mechanism is an augmentation that preserves the previously matched left vertices. Here every accepted whole island supplies its actual new four-edge extension; existence is not inferred from a heuristic or an unproved matching oracle. Physical slots retain their exact family/call compatibility rather than being identified solely by width. + +The donor's physical decomposition is: all other occupied coordinates as the base; its existing four-axis borrowed block as the global choice; and its actual unclaimed axis as the flag choice. These sets are pairwise disjoint and their total rank fits capacity. This specializes the explicit disjoint-pool and capacity hypotheses of OpenAI PhysicalPoolLift. Its fractional-cover conclusions are not used to claim an integral physical map. The final literal owner table and independent actual-chart audit supply the integral witness. + +## Universal strict saving + +Each accepted island adds L locally and removes four rank-one pending remainders. Thus the complete paid change is Delta=-12H1+8H2+4H3-4H4, with zero rank mass. For every 0 < b < 1, the paid moment of Delta is strictly negative. + +Proof: set alpha=1-b, u=2^alpha in(1,2), p=ln(3)/ln(2) in(4/3,2). Dividing out the positive factor 73^b, the change is h(u)=-12+8u+4u^p-4u^2. Since p(p-1)u^(p-2)<2 on [1,2], h''(u)<0. Its endpoint derivative h'(2)=6p-8 is strictly positive, so h is strictly increasing on [1,2]. Since h(2)=0, h(u)<0 whenever u<2. The exact rational moment certificate supplies the achieved finite endpoint; this argument supplies the all-admitted-exponent sufficient comparison. + +## Frozen realized witness + +42 islands are installed by within-call exchanges and self-donors, then 47 further islands by legal cross-call exchanges, for 89 extra islands in 52 calls. Providers0,1,2,3 occur 92,30,7,15 times. The exact final paid profile is + +{1:340860,2:71848,3:59684,4:18364,5:11808,8:1152,24:1,48:4918}. + +Rank mass 1041408 and deficit 5120 remain unchanged. The final map differs in 1409 complete records from the source-pinned public PR1148 table. Its actual pending-remainder profile is {1:4,24:1,48:4918}, with 4923 positive remainders. The independent current-source geometry checker verifies all 69,120 roles, all 144 calls, every actual provider width, every unclaimed axis and 10,271 actual orthogonal 73-column chart types, rejecting 13 targeted controls. The finite invoice separately passes nine guards and four controls. All native provider and inherited all-size/analytic scopes remain explicit. + +The bounded last-group experiment realized no further group: the four remaining gap families had no common recipient call, and the tested one-neutral-relocation/short-augmentation class produced no witness. This is not a global optimum or an exclusion of longer or different transformations. The 89 table is held fixed. + +## Exact result and source scope + +Conditional native kappa 0.001675224519162937; conservative kappa 0.001675224516317980. Native gain over frozen PR1148 is 0.000000102871373730. Two exact rational moment engines and all 47 strict outer inequalities are checked by the root. The user uploads the package manually; no publication or push occurred. + +The initial T37 combination with PR1152 was explicitly rejected after exact pricing showed that naive width adaptation would worsen its moment. Its metadata and compatible local inventory were read, but its numerical claim is not added to this T16 result. PR1129/1131 remain structural context. No private Claude handoff, WSL, C++, GPU, Lean compilation or background computation is used in this round. Native Windows Python computations run at BelowNormal priority and have bounded single-process passes. diff --git a/research/crosscall-kernel-demotion/notes/recurrence/OPENAI-SOURCES.json b/research/crosscall-kernel-demotion/notes/recurrence/OPENAI-SOURCES.json new file mode 100644 index 0000000000..611dbd635a --- /dev/null +++ b/research/crosscall-kernel-demotion/notes/recurrence/OPENAI-SOURCES.json @@ -0,0 +1,13 @@ +{ + "scope": "Exact source inspection of downloaded OpenAI modules; no fresh Lean build or new axiom audit in this round", + "sources": [ + { + "path": "D:\\proof\\external\\openai-math\\lean\\OAI\\LinearAlgebra\\MatrixMultiplication\\AuxiliarySeparation\\Tensor\\DirectSum.lean", + "sha256": "8f320a57fb1a726d81fea6f967a6c7d1c0c708cc2ddccbefc7514ffd3739756b" + }, + { + "path": "D:\\proof\\external\\openai-math\\lean\\OAI\\Probability\\SignedSweeps\\TensorCommutant.lean", + "sha256": "83aff53acdef8b2ee7330de3d8270284c67449f18ee36d50dbbf99cb599fc7a9" + } + ] +} diff --git a/research/crosscall-kernel-demotion/notes/recurrence/RESULTS.md b/research/crosscall-kernel-demotion/notes/recurrence/RESULTS.md new file mode 100644 index 0000000000..14a7e680f0 --- /dev/null +++ b/research/crosscall-kernel-demotion/notes/recurrence/RESULTS.md @@ -0,0 +1,17 @@ +# Final recurrence lane handoff + +Complete. No active jobs. Native bounded Windows Python only; no WSL, C++, GPU or Lean builds. + +Final root conditional kappa0.001675224519162937. Actual candidate is owners/t16-crosscall,89 extra demotion groups over52 calls; T37 geometry P37.json is a separate sufficient transport interface, not a claimed constructed improvement. + +Final independent finite evidence: +- T16-CROSSCALL-FINAL-AUDIT.json: fresh source windows, all pending children, all actual73-column charts and13 meaningful mutations; PASS3.73s. +- T16-CROSSCALL-AUDIT.json and -SIGMAS/-REMAINDERS.json.gz retain the earlier same-witness full chart/remainder payloads. +- T16-CROSSCALL-INVOICE.json: complete fresh mixed bill, all9strict inequalities and4 controls; actual adapter count387120, local cap10039700351134, used allowance6467145011279720. +- The final table is frozen; owner worker's bounded last4gap search produced no90th-group witness. + +Portable code frozen: audit_owner_table.py, audit_candidate.py, finite_invoice.py. SourceSPEC is the actual PR1148 SPEC; the unchanged canonical base is independently recounted against it, with scalar semantic admission explicitly inherited. Changed variant native folders k1..3 supply source-bound fresh scalar/frame profiles and actual widths. Dispatch.helpers must equal exactly the canonical per-variant width difference; every change adds1axis. All changed tables and every pending complement are rebuilt; no old admission receipt is reused. + +Two distinct source-inspected OpenAI mechanisms and sufficient mathematical uses: MatrixMultiplication.AuxiliarySeparation.Tensor.DirectSum block/restriction transport; SignedSweeps.TensorCommutant joint histogram/orbit finite physical permutation. Exact paths, statements and source hashes are in SUFFICIENT-TRANSPORT.md and OPENAI-SOURCES.json. No new Lean certification is claimed. + +Conditional interfaces remain explicit. Final root pricing/packaging is separate, with no live refresh, publication or push. diff --git a/research/crosscall-kernel-demotion/notes/recurrence/SUFFICIENT-TRANSPORT.md b/research/crosscall-kernel-demotion/notes/recurrence/SUFFICIENT-TRANSPORT.md new file mode 100644 index 0000000000..5dd14470b3 --- /dev/null +++ b/research/crosscall-kernel-demotion/notes/recurrence/SUFFICIENT-TRANSPORT.md @@ -0,0 +1,64 @@ +# Sufficient replica transport and exact labelled physical lifting + +This round freezes public PRs through1153. The strongest claimed input is PR1148's changed-entrance/eight-end T16 word; PR1152 gives a different two-end T37 owner schedule. Their advertised exponent gains are never added. A new construction must place the ACTUAL selected local word on one literal replica geometry and price its single complete paid histogram. + +## Mechanism1: explicit direct-sum transport + +Source: D:/proof/external/openai-math/lean/OAI/LinearAlgebra/MatrixMultiplication/AuxiliarySeparation/Tensor/DirectSum.lean. + +Exact declarations in namespace OAI.MatrixMultiplication.AuxiliarySeparation: + +- `sumTensor_restrict`: independently restricting each summand with its three coordinate maps is exactly restriction of their direct sum by the block-diagonal maps. +- `sumTensor_assoc` and `sumTensor_comm`: reassociation and interchange are explicit coordinate permutations, with no hidden identification of physical spaces. +- `sumTensor_product` / `product_sumTensor`: tensoring distributes over a binary direct sum through explicitly given coordinate equivalences. + +Concrete sufficient use: replica-local DATA streams are disjoint blocks of896 families. The parent source recipe applies the same admitted data identity on each block. Splitting37 replicas into8+8+8+8+5 changes only those explicit block coordinates. Inducting the direct-sum restriction identity transports the admitted local data action to all37 blocks. A chronological interleave may reorder independent replica steps while preserving every replica's original30-event projection. Borrowed helper families are handled separately by literal inactivity windows and the complete-call dirty-restoration invariant; direct-sum algebra alone does not permit helper aliasing. + +The partial five-lane group must retain the whole source bank packet and pay its complementary axes. This gives the correct dedicated-bank envelope: + + data =896*T, + bank_groups=ceil(T/8), + bank_stock=4536*bank_groups, + parent_live=data+bank_stock, + parent_physical=parent_live+514. + +ForT37 this is55,832 live and56,346 physical, not the incorrectly linearly scaled54,131. The hosted actual stock is33,152 live plus480 helpers,8 centres and2 coefficient streams =33,642. The finite invoice retains and charges the larger envelope. + +## Mechanism2: joint-label orbit gives an actual permutation + +Source: D:/proof/external/openai-math/lean/OAI/Probability/SignedSweeps/TensorCommutant.lean. + +Exact declarations in namespace OAI.SignedSweeps: + +- `wordHistogram_eq_orbit`: if two finite words have equal complete histograms, there is a position permutation g with z(g(i))=w(i) for every i. +- `wordCommutant_histogram_constant`: for an operator commuting with all position permutations, equality of complete joint input/output label histograms implies equality of the corresponding matrix entries. + +Concrete sufficient use: a frozen finite flow supplies labelled donor occurrences and an actual supplier supplies labelled helper requests. Use the COMPLETE labels(calltime,width,provider/admitted variant,eligibility/window class), not width alone. Equality of these histograms supplies a literal label-preserving bijection. One deterministic implementation sorts each label fiber by original occurrence position and pairs those lists. This is an exact finite physical lift, not a solver or unknown allocation oracle. A fresh verifier must still check actual family identity, per-call distinctness, full inactivity interval, chronological reserved axes and pending complements. + +After the lift, normalize only genuinely interchangeable tensor-coordinate factors. The commutant theorem explains why a complete joint signature suffices when the factor operator is invariant under those coordinate permutations. Frame direction, exact phase and spectator type must be in the signature whenever they differ. This is no claim that arbitrary same-rank frames or arbitrary helper roles can be exchanged. + +## Sufficient changed-map semantics + +For every admitted complete local call, the data action is independent of arbitrary borrowed helper dirt, and each borrowed family restores except for its declared normalized residual factor. Require that every assigned family is inactive throughout that complete call and no two roles in the call alias it. For each pending child, reserve disjoint chronological coordinate factors and keep the explicitly paid transform on their complement. The product of hosted factors and the remainder is exactly the original pending transform. Induction over actual source events proves the full data endpoint and dirty restoration. Each replica projects to the original30 source events, with the two global tails retained. No free value-bearing scratch is introduced. + +Our T-variable checker reconstructs all real last-touch-to-idle windows from the current ROUND20 source and actual phase-axis ranks. It derives every73-column chart from the actual port basis and pending axes, including spectators and all unused pending children. An old T16 SPEC contributes only its inherited LOCAL interface; its call-order/mass receipt is never reused as admission of a new T37 table. + +## Runtime accounting + +Fresh literal native words supply actual per-provider macro/event counts, paid local profiles, helper entry/exit dimensions, ordered wrapper selection and prefix bounds. The new complete call dispatch and actual idle remainder table supply the global totals. ForT replicas, the controller has9*T complete calls,9*T bridge events,2016*T conservative parent idle-child slots and the explicit bank envelope above. The global prefix bound is max(localprefix)+37+18*T+4. AtT37 with localprefix68 it is775, charged at1024. The row guard is freshly computed with that1024-bit reserve, rather than reusing the T16 row coefficient. + +The historical pinned invoice contributes ONLY its already charged prior allowance; the entire fresh mixed bill is added again under the original overcharge policy. All nine finite inequalities, complete profile/mass/deficit and exact outer price are recomputed. The inherited compiler, physical/common-label realization and analytic-transfer contracts remain explicit. Source inspection and these finite checks are not a fresh Lean certification or an unconditional multiplication theorem. + +## Final admitted finite candidate of this round + +The T37 mandatory transport was investigated but did not supply the final witness. The delivered construction instead uses PR1148's actual T16 geometry with89 additional entrance-demotion groups over52 complete calls. The source PR1148 three-group changes are already in the baseline word; only the additional627/635/651 prefixes are counted here. Their actual joint native words are admitted independently, not extrapolated by adding local estimates. + +The independent audit derives every dispatched helper set from the difference between actual canonical base widths and the selected variant's canonical widths. It requires every changed width to increase by exactly one axis and checks that the literal dispatch.helpers equals that exact derived set. Wrong helper metadata, wrong variant selection and forgotten widened dispatch are rejected. The concrete demand/slot bijections preserve complete call/window/type signatures, providing the sufficient physical lift described above. + +Final literal counts:69,120 roles,144 complete calls,92 default calls,30 variant1 calls,7 variant2 calls and15 variant3 calls. The complete new profile is {1:340860,2:71848,3:59684,4:18364,5:11808,8:1152,24:1,48:4918}; mass1,041,408 and deficit5,120. The actual idle profile is {1:4,24:1,48:4918}, with4,923 paid remainder children. There are10,271 distinct actual73-column charts; every chart and spectator is reconstructed fresh. Cross-replica roles number59,621. The chart stream SHA-256 is cebea57525f840cfc3e50f178c3b13c8961f09b284fba303ea8d493e8e9f7ad0. + +The actual current source-event expansion reconstructs all288 positive-rank child windows and the480 replica-local source events. All pending children, including unused ones, have their actual physical axis rank and basis containment checked; distinct pending children on the same physical pair/side have disjoint axes. Per-call physical family uniqueness, exact original last-touch-to-idle windows and chronological axis prefixes are checked literally. Thirteen meaningful owner, source, chart and dispatch controls reject. The final independent replay took3.73seconds. + +The changed source has3,498 local children, not the preceding round's3,494. The fresh adapter count is therefore387,120, and the local primitive bound is10,039,700,351,134. The complete primitive total is28,625,376; scalar macros2,835,792; paid wrapper factors9,953,280. Fresh per-vertex is3,589,198,021,555,152. Add the source-bound prior charged allowance2,877,946,989,724,568 to obtain6,467,145,011,279,720. All nine strict finite inequalities and four invoice controls pass; actual prefix397 is charged at512 and row16,469 is below20,161. These new numbers must not be replaced by the preceding round's smaller adapter count or per-vertex bill. + +The root's two exact moment engines and strict outer assembly certify conditional kappa0.001675224519162937, improving the frozen public PR1148 value0.001675121647789207 by0.000000102871373730. Unchanged baseline scalar semantics remain inherited from the exact source admission; its actual canonical frames/widths/profile are freshly recounted. Changed native variants are freshly checked by the cell worker. Universal compiler, physical/common-label realization and analytic obligations retain their explicit source scope. No full historical public re-verification, Lean build, C++, GPU, WSL or background service was launched for this lane. diff --git a/research/crosscall-kernel-demotion/pricing.py b/research/crosscall-kernel-demotion/pricing.py new file mode 100644 index 0000000000..026d9d37eb --- /dev/null +++ b/research/crosscall-kernel-demotion/pricing.py @@ -0,0 +1,47 @@ +from fractions import Fraction as Q +from decimal import Decimal, localcontext +import json,importlib.util,gzip +from pathlib import Path + +def need(x,label): + if not x:raise RuntimeError(label) +def decimal(q): + with localcontext()as ctx: + ctx.prec=65 + return str(Decimal(q.numerator)/Decimal(q.denominator)) +def encode(x): + if isinstance(x,Q):return str(x) + if isinstance(x,dict):return {str(k):encode(v)for k,v in x.items()} + if isinstance(x,(list,tuple)):return [encode(v)for v in x] + return x +def price(H,bit,M,B,A,bad=False): + cert=M.certify(H,73,14336,bad);b=Q(cert['lower']);intervals=[] + for z,accept in [(b,True),(b+Q(1,10**24),False)]: + i=M.moment(H,73,14336,z,bad);j=B.moment(73,14336,list(H.items()),z) + if bad: + c=B.moment(73,14336,[(1,32*73*73*sum(H.values()))],z) + j=(j[0]+c[0]/10**16,j[1]+c[1]/10**16) + need(i[1]<1 and j[1]<1 if accept else i[0]>1 and j[0]>1,'two rational moment signs') + intervals.append({'b':z,'accepted':accept,'mercator':[v-1 for v in i],'base_two':[v-1 for v in j]}) + eta=beta=Q(1,10**24);s=min(bit,(1-beta)*b)-Q(1,10**27) + need(00,'bootstrap gap') + cut=max(ceil(36/gap**2),ceil(2*(4+512)/gap)) + need(cut*gap**2>=36 and cut*gap>=2*(4+512),'charged finite cutoff') + cuts.append({'a':a,'gap':gap,'cutoff_log2':cut}) + q=a*(1-2*eta);margin=(1-eta)*q/(1+q);ticks=margin*10**18 + k=Q((ticks.numerator-1)//ticks.denominator,10**18) + bridge={'semantic':{'C0':{'base':2,'exponent':210000},'strict_literal_gap':1},'rows':{'degree_gap':Q(10**6)-Q(51*20161,25)}} + outer=A.assembly(a,b,bridge,k,eta=eta,beta=beta) + need(len(outer['strict_constraints'])==47 and all(v>0 for v in outer['strict_constraints'].values()),'47 strict outer inequalities') + controls=[] + for name,kk,ee,be in [('next_grid',k+Q(1,10**18),eta,beta),('zero_eta',k,Q(0),beta),('zero_beta',k,eta,Q(0)),('unit_beta',k,eta,Q(1))]: + try:A.assembly(a,b,bridge,kk,eta=ee,beta=be) + except AssertionError:controls.append(name) + else:raise RuntimeError('outer control accepted: '+name) + return {'complex_lower':b,'kappa':k,'kappa_decimal':decimal(k),'moment_checks':intervals,'outer_constraints':outer['strict_constraints'],'outer_controls':controls,'bootstrap':cuts} + diff --git a/research/crosscall-kernel-demotion/vendor/engines/base_two_moment.py b/research/crosscall-kernel-demotion/vendor/engines/base_two_moment.py new file mode 100644 index 0000000000..14a90fa0e7 --- /dev/null +++ b/research/crosscall-kernel-demotion/vendor/engines/base_two_moment.py @@ -0,0 +1,63 @@ +#!/usr/bin/env python3 +"""Maintainer arithmetic cross-check of the pinned PR39 certificate. + +Uses no producer/checker imports. Counts are inputs, not proved by this script. +80-term rational logarithms and 12-term exponentials independently enclose +the two moments. The accompanying written review addresses their realization. +""" +import argparse +from fractions import Fraction as Q +from hashlib import sha256 +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +GRID = 10**30 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def log_unit(x): + require(1 <= x <= 2, "logarithm range") + z = (x-1)/(x+1) + lo = 2*sum((z**(2*j+1)/(2*j+1) for j in range(80)), Q(0)) + return lo, lo+2*z**161/(161*(1-z*z)) + + +def log_bounds(x): + k = 0 + while x > 2: + x /= 2 + k += 1 + lo, hi = log_unit(x) + l2, u2 = log_unit(Q(2)) + lo, hi = lo+k*l2, hi+k*u2 + # Outward rational rounding keeps later certificates compact. + return Q((lo*GRID).__floor__(), GRID), Q((hi*GRID).__ceil__(), GRID) + + +def exp_bounds(x): + require(0 <= x < 1, "exponential range") + term = total = Q(1) + for j in range(1, 13): + term *= x/j + total += term + tail = term*x/13/(1-x/14) + return total, total+tail + + +def moment(m, W, entries, saving): + lo = hi = Q(0) + for t, count in entries: + t, count = int(t), int(count) + require(0 < t < m and count > 0, "improper child") + l, u = log_bounds(Q(m, t)) + lower = exp_bounds(saving*l)[0] + upper = exp_bounds(saving*u)[1] + lo += Q(t*count, m*W)*lower + hi += Q(t*count, m*W)*upper + return Q((lo*GRID).__floor__(), GRID), Q((hi*GRID).__ceil__(), GRID) + diff --git a/research/crosscall-kernel-demotion/vendor/engines/moment.py b/research/crosscall-kernel-demotion/vendor/engines/moment.py new file mode 100644 index 0000000000..7d697cb452 --- /dev/null +++ b/research/crosscall-kernel-demotion/vendor/engines/moment.py @@ -0,0 +1,113 @@ +"""Independent prospective ordinary five-stage cost, never supplier admission. + +Consumes a raw one-invocation ledger made from the actual source/internal/target +paths. No packed profile is used as an input. Missing physical/finite/compiler +obligations must remain explicit in the accompanying report. +""" +from collections import Counter +from decimal import Decimal, localcontext, ROUND_FLOOR +from fractions import Fraction as F +from functools import lru_cache +from math import factorial +import hashlib, json, sys +from pathlib import Path + +DYAD = 1 << 224 + +def floor(x): return F(x.numerator*DYAD//x.denominator, DYAD) +def ceil(x): return -floor(-x) + +@lru_cache(None) +def logarithm(x): + """Mercator bounds after binary reduction; ln(2) via two Mercator sums. + + For 1 <= y < 2, log(y) is an alternating series in z=y-1. + We instead reduce to 1 <= y < 3/2, and bound log(3/2) and + log(2) by the same alternating series at z=1/2 and z=1/3, + using log(2)=log(3/2)+log(4/3). All sums are exact rationals. + """ + assert x >= 1 + k = 0 + while x >= 2: x /= 2; k += 1 + j = int(x >= F(3, 2)) + if j: x /= F(3, 2) + def mercator(y): + z=y-1 + assert 0 <= z <= F(1,2) + # An even partial sum is below log; the next term bounds its tail. + t=z; s=F(0) + for n in range(1, 225): + s += (t if n & 1 else -t)/n + t *= z + return s, s+t/225 + a,b=mercator(x); c,d=mercator(F(3,2)); e,f=mercator(F(4,3)) + return floor(a+(k+j)*c+k*e), ceil(b+(k+j)*d+k*f) + +def exponential(l,u): + assert 0 <= l <= u < F(1,10) + def poly(x): + s=t=F(1) + for j in range(1,25): t=t*x/j; s+=t + return s,t + lo,_=poly(l);hi,last=poly(u) + return floor(lo),ceil(hi+last*u/25/(1-u/26)) + +def moment(H,m,W,a,bad=False): + lo=hi=F(0) + for r,n in H.items(): + assert 0 < r < m and n > 0 + l,u=logarithm(F(m,r)); e,f=exponential(a*l,a*u) + p=F(r*n,m*W);lo+=p*e;hi+=p*f + if bad: + # Existing envelope shape, only conditionally portable to the new cover. + l,u=logarithm(F(m));e,f=exponential(a*l,a*u) + p=F(32*m*sum(H.values()),10**16*W) + lo+=p*e;hi+=p*f + return floor(lo),ceil(hi) + +def decimal(x): + with localcontext() as c: + c.prec=70 + return str(Decimal(x.numerator)/Decimal(x.denominator)) + +def certify(H,m,W,bad=False): + with localcontext() as c: + c.prec=70 + terms=[(Decimal(r*n)/Decimal(m*W),(Decimal(m)/Decimal(r)).ln()) for r,n in H.items()] + fallback=Decimal(32*m*sum(H.values()))/Decimal(10**16*W) if bad else Decimal(0) + lm=Decimal(m).ln();lo=Decimal(0);hi=Decimal('.003') + for _ in range(210): + a=(lo+hi)/2 + if sum(p*(a*l).exp() for p,l in terms)+fallback*(a*lm).exp()<1:lo=a + else:hi=a + q=int(((lo+hi)/2*10**24).to_integral_value(rounding=ROUND_FLOOR)) + lo=F(q,10**24);hi=lo+F(1,10**24) + lv=moment(H,m,W,lo,bad);hv=moment(H,m,W,hi,bad) + assert lv[1]<10 for v in slacks.values()),{k:str(v) for k,v in slacks.items() if v<=0} + assert min(margins.values())==minimum + assert margins['balanced_prefix']-minimum==eta and 1-eps-r==eta/2 + assert 1-eps*(1+c)==eta-eps*eta/4 + return dict(parameters=dict(a_bit=a,a_complex=b,tau=tau,sigma=sigma, + eta=eta,beta=beta,q=q,c=c,epsilon=eps,lambda_=lam, + lambda_prime=lp,alpha_squared_power=r,delta=delta, + C0=bridge['semantic']['C0'],C1=1,kappa=kappa), + strict_constraints=slacks,margins=margins,minimum_margin=minimum, + absorption_gap=minimum-kappa, + recurrence=dict(internal=internal,leaf=leaf,reservations=1-c)) diff --git a/research/crosscall-kernel-demotion/vendor/pr1148/CLAIM.json b/research/crosscall-kernel-demotion/vendor/pr1148/CLAIM.json new file mode 100644 index 0000000000..a49532ec86 --- /dev/null +++ b/research/crosscall-kernel-demotion/vendor/pr1148/CLAIM.json @@ -0,0 +1,29 @@ +{ + "status": "PASS_THREE_DEMOTIONS_COMPLETE_ADMISSION", + "kappa": "1675121647789207/1000000000000000000", + "kappa_decimal": "0.001675121647789207", + "previous_kappa": "0.001674622497877364", + "gain_percent": "0.029806712406867100374241200", + "complex_lower": "13423459109255787537/8000000000000000000000", + "bit_lower": "1733427039589844234749/1000000000000000000000000", + "global_profile": { + "1": 341928, + "2": 71136, + "3": 59328, + "4": 18720, + "5": 11808, + "8": 1152, + "24": 1, + "48": 4918 + }, + "local_profile": { + "1": 2372, + "2": 494, + "3": 412, + "4": 130, + "5": 82, + "8": 8 + }, + "scope": "Conditional native exact-complex witness with twelve helper entrances lowered from dimension five to four, refitted local recursive frames, whole-helper T16 hosting, and the unchanged PR589 bit supplier. Scalar operations and their order are unchanged. PR559 exact-cover recurrence correction, bit bad-residue surcharge, and H1-H5 retained. All-size compiler, common-label/mutable-source realization, whole-call hosting, precision/tape and analytic transfer remain assumptions. No unconditional theorem or full Lean certification. The earlier fixed-local-interface ceiling does not cover this changed word.", + "fixed_family_grid_upper": "0.001675129371412064" +} diff --git a/research/crosscall-kernel-demotion/vendor/pr1148/NOTICE.md b/research/crosscall-kernel-demotion/vendor/pr1148/NOTICE.md new file mode 100644 index 0000000000..9f759cfade --- /dev/null +++ b/research/crosscall-kernel-demotion/vendor/pr1148/NOTICE.md @@ -0,0 +1,7 @@ +Apache-2.0. Prepared for Thomas DiFiore with OpenAI Codex assistance. + +* `../k8-eight-ends` and `../k8-eight-ends-t16` supply the unchanged scalar word, endpoint construction, initial owner map, and pinned T16 controller. Their notices retain the PR1018, PR1030, PR864, PR858, PR870, PR1074, and earlier E8, k8, frame, owner, and bit-supplier credits. +* PR1111 by seslly / shipstuff, commit `381831ea554ea983e16224dabed8921b7d0ffdbc`, supplied the entrance-demotion lead: reversing a promotion can profitably trade wider helpers for a different recursive profile. Its README/PR claim was consulted; no PR1111 code or owner payload is consumed. This package instead screens all codimension-one subspaces of the six current dimension-five groups, composes three groups on the eight-endpoint word, and constructs its own complete T16 owner assignment. The older promotion mechanism is credited to PR664 and its descendants. +* The frame refit uses the preceding adaptation of PR864's complete frame model (navinor / Claude). Solver output is nomination data; independent native replay and unchanged global engines decide admission. +* The coordinated pattern-pricing search is retained from `../k8-eight-ends-t16`. Earlier owner algorithms and signed duals are credited in its notice. The bound adapts jon314159's PR942 certificate and chafreaky's PR795/890 prices, using the existing two rational arithmetic engines. +* The fresh native and global checks retain every inherited analytic, compiler, boundary, common-label, hosting, precision/tape, and bit H1–H5 assumption. This package does not claim original authorship of those constructions or an unconditional theorem. diff --git a/research/crosscall-kernel-demotion/vendor/pr1148/OWNERS.json.gz b/research/crosscall-kernel-demotion/vendor/pr1148/OWNERS.json.gz new file mode 100644 index 0000000000..7bd0fecafe Binary files /dev/null and b/research/crosscall-kernel-demotion/vendor/pr1148/OWNERS.json.gz differ diff --git a/research/crosscall-kernel-demotion/vendor/pr1148/PLAN.json.gz b/research/crosscall-kernel-demotion/vendor/pr1148/PLAN.json.gz new file mode 100644 index 0000000000..864cdd212f Binary files /dev/null and b/research/crosscall-kernel-demotion/vendor/pr1148/PLAN.json.gz differ diff --git a/research/crosscall-kernel-demotion/vendor/pr1148/SOURCE-PINS.json b/research/crosscall-kernel-demotion/vendor/pr1148/SOURCE-PINS.json new file mode 100644 index 0000000000..57ce7f32fc --- /dev/null +++ b/research/crosscall-kernel-demotion/vendor/pr1148/SOURCE-PINS.json @@ -0,0 +1,221 @@ +{ + "research/community-k492-audit/pr622/replay/baseline558/complex-global/base/split-centres/CANONICAL-WORD.json.gz": "66d3c3c70983224650643a0a05a21ac6c6959f84d0f4528650601016f5a76844", + "research/community-k492-audit/pr622/replay/baseline558/complex-global/base/split-centres/CLIFFORD-RECIPES.json": "534ace870cabe515987e00f50f71550030965006ea18978e0924590ac6944345", + "research/community-k492-audit/pr622/replay/baseline558/complex-global/base/split-centres/CLIFFORD-REVIEW.json": "ee9b86428278392d2c933f76d60e51f5af90d4ab67e4d3937ed2fa416e7755ab", + "research/community-k492-audit/pr622/replay/baseline558/complex-global/base/split-centres/INDEPENDENT-LOCAL-REPLAY.json": "ad3f2b941127688f98ce6872d00f110644f1c2b156f8adad1b6700e838ed0e26", + "research/community-k492-audit/pr622/replay/baseline558/complex-global/base/split-centres/INDEPENDENT-REPLAY.json": "ad3f2b941127688f98ce6872d00f110644f1c2b156f8adad1b6700e838ed0e26", + "research/community-k492-audit/pr622/replay/baseline558/complex-global/base/split-centres/INTEGRATION.json": "5c14538134dfffbc58fa4b4d2f26b270ec5f56d17d4bf23752c82964f45171db", + "research/community-k492-audit/pr622/replay/baseline558/complex-global/base/split-centres/LOCAL-CHECKS.json": "79177449e404403964ce1b2f4a9a8bd49e1916daba3123d7fd7f5cfd1f1ac0ea", + "research/community-k492-audit/pr622/replay/baseline558/complex-global/base/split-centres/LOCAL-PROGRAMS.json.gz": "99a18eede965accf65943e490b8d2b2ffb9f1c9bc6babdb825413a80cbea2cde", + "research/community-k492-audit/pr622/replay/baseline558/complex-global/base/split-centres/RESIDUAL-ADAPTERS.json": "baafef737acc16dafbe1150896feb16744f3d669fa123bb2bff19ecc4e71b275", + "research/community-k492-audit/pr622/replay/baseline558/complex-global/base/split-centres/SCALAR-FRAME-AUDIT.json": "73b3601a6239502475a272ea0c46945fd42034486aaf43e66a212eb4f012ca44", + "research/community-k492-audit/pr622/replay/baseline558/complex-global/base/split-centres/WRAPPER-CHECKS.json": "9a09146e686c4f535b04fdef3753fe01dad8f5e8881a69408a91394acb5b48f5", + "research/community-k492-audit/pr622/replay/baseline558/complex-global/base/work/complex-nine-native/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "research/community-k492-audit/pr622/replay/baseline558/complex-global/controller-input/split-centres/CANONICAL-WORD.json.gz": "de2be0f4b6d24ace368fd5b834b7a00f9625d0a1824c4ff969f2db5f115db667", + "research/complex-k492-owner-repair/vendor/multicold/code/assemble.py": "3fedbccb09d469f8ee366b4302e51448de6d25793a78a12c5f9a8d9667a755eb", + "research/complex-k492-owner-repair/vendor/multicold/code/assembly_controls.py": "a0f2349ba8fe8404b8b76c869f12dd7e250a775b2e05b3c9c00e6889ad4c8a45", + "research/complex-k492-owner-repair/vendor/multicold/code/audit_allcold.py": "7950e5c01488a9146bdbaf19ab4fd0c33cd25a4d63fb56ef995ef2e45ac7ec1a", + "research/complex-k492-owner-repair/vendor/multicold/code/audit_kernel_controls.py": "5100459211f43ba048bf82c3942bbedb8b224272b24722a14f0dcd808a38aafa", + "research/complex-k492-owner-repair/vendor/multicold/code/audit_multicold_controls.py": "3ff631f0bdc7e707d4296ff441802cc26da9c6556650469f09ab7253558b4017", + "research/complex-k492-owner-repair/vendor/multicold/code/bind_providers_portable.py": "01e62fee1f1dcf1b7b34338d555dacd5cd1d7d10d6b9a605d0913d959f8c7ecf", + "research/complex-k492-owner-repair/vendor/multicold/code/build_cold_kernel.py": "aa556a1988f7d4c52bd82fd2a648769f7094bd75ba79582c15ec441d710e213b", + "research/complex-k492-owner-repair/vendor/multicold/code/build_four_portable.py": "417b1dc4dca485dfbbaa820e552cae9bf3932bbace6ea16ce93aa0590c3c184e", + "research/complex-k492-owner-repair/vendor/multicold/code/build_multicut_kernels.py": "6ab3d73f81d5b2fb884a93a336ef1940e118d419d425b3356bab3b97f774c9aa", + "research/complex-k492-owner-repair/vendor/multicold/code/emit_allcold.py": "9d6c75af63fa8f53973734ccb1eef983511f4337ce644436a693fd8fb9ef8fe2", + "research/complex-k492-owner-repair/vendor/multicold/code/invoice_allcold.py": "ff8fee775ad97926454f3ad1183f8e05de654e276150e579ce612f3eb2f98d44", + "research/complex-k492-owner-repair/vendor/multicold/code/phase_timing_controls.py": "dcc4adfd139d6f65a88bdc6d183ea3777d4e4f688d2169dd41b54964f05591bb", + "research/complex-k492-owner-repair/vendor/multicold/code/run_portable.py": "322d29d43dbee8130cde15d4bf05396698b5e3dfe3735813899db91cc0ba7955", + "research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098", + "research/complex-k492-owner-repair/vendor/multicold/engines/moment.py": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482", + "research/complex-k492-owner-repair/vendor/multicold/engines/outer.py": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c", + "research/complex-k492-owner-repair/vendor/multicold/inputs/PR543-EXPECTED.json": "06eccee9f6b77e140833df83407e7996dc948c17d49b0779ab171fbe463fd28d", + "research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/code/phases_full.py": "a273c325ffd6793d5b63b79a289a9d2bbc9292e6940fb5a926924f3708627af4", + "research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/complex-global/vendor531/code/prepare_supplier_base.py": "f5eae94aca965d0008bc07cff8245ccb7509042ccad457d3bcb7d51c1e9409f0", + "research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/complex-global/vendor531/evidence/audit/PREFIX-AND-INVOICE.json": "ce1bfa49be88ae67a404f606a11db2232b7e1f2610d4418058e39749d86d8478", + "research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/complex-global/vendor535/inputs/ROUND20-PARENT-TEMPLATE.json.gz": "025448abdf2012d327e50a009084e1501690d05e650300d2982836aa0350ae00", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/assemble.py": "1b1a9024ac910dc9b9d9e30150684e1fa9cb228a4c1c275b75ab04b57fdef1dd", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/assembly_controls.py": "8a365b95c412d75d10db5bb59309d47cd56c5f8a77566f940a05977795130ce8", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/audit_allcold.py": "cea021ae79658ca7ca4d07f1e1a70bdb4947afaf95b362114c11032c0fef889a", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/bind_providers_portable.py": "2eb5c262bf481b3bec9ceaec654fa46ff6fc3a89b13d4906a29a55a89e35feea", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/build_cold_end.py": "864b4701dd73afd0c9d99761b7a749f3354c48985730f17054e18c052996a668", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/build_frame_regroup.py": "e2549ccc7a90008831be3b59aeb37b47db696640f5f5c2b72dd888b2f1e7e5c9", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/build_gate_moves.py": "08bf1c2652307aeefbab089fdaf02f82e2c396ca23a1eb68e294a67e74c44252", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/build_hpe.py": "ba2001695d8c7547a82260c3b016e01dac686e95a61757ca124eb9879078ea8e", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/build_port_stage.py": "beb0d30fde1b9a30db091880b38c4a8ec906da3f715c43de7db8bf7932526e72", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/cold_end_controls.py": "0c404f49e90457520f1788ee6741c9ac154a5814c54ad6cb83b59c44552ebc84", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/construct_k_triangle.py": "66fc460df8eb8067efe3d8a3f9e97a7244aacd7bf11650a6ce656e868ce053da", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/emit_allcold.py": "fe26f10fe5d30ed407a37540a45ef94f44576dd241d09e19aef5db1efb072746", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/generated_identity.py": "c8af22719c0f3097a991a3f6ccac8f090afd2faba554745733d9ea88f2c25708", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/generated_identity_controls.py": "a7b93207a673575d1fddc3e579153349c145c8f08d4575ae0a5d1e3cffec01de", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_adapters_local.py": "eb0b5c6c7161e18dc22168da3211448d321586edd15bcfb4b4741174d36993cf", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_audit_and_transport.py": "c9a05ff291016b870b4fc925b317abd9c3a604c73ffc8920dfdbbeb475e20aa3", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_audit_local.py": "6bd9a1e279c9c9e4f3767d9f82e537b559292906feb2ddab02f380fb6523a810", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_controls_atc.py": "63aa3909b5bfd3bf270c313bebb5c46e7789c67a8f2439f568bc4b2b4a35d17b", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_emit_local.py": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/invoice_allcold.py": "141bd2fd58bbfb5b8d0fc8f56f61c45586d5608a5af3487c6b883dd987f998ec", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/phase_timing_controls.py": "1692ccee3da4b1781408d126ee4999f3e31a505cd83c64823a404033da3a6339", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/witness.py": "00789c911a8f32cfe9d52207c7aa78305dc3fce4a8b6305ba402b7e74117103d", + "research/gauge44-leaver8/MANIFEST.json": "7c9637f06798b144274458efa145f701c61282f8b3aab1c0c900b53bdfbe1f0d", + "research/gauge44-slots/MANIFEST.json": "9a6f239b1618a43262e56735a99cc59b6f5a6e8816a794a34413e89cc33f4976", + "research/gauge44-slots/code/assemble.py": "4c270a996b380ab712f72b81173ab24f1c73203a33578f261bfbaa7e67d75aec", + "research/gauge44-slots/code/assembly_controls.py": "e4c0f7828af64fdaef1896e4448d0212bd3041805097140b8cfafd098f8a6162", + "research/gauge44-slots/code/audit_allcold.py": "a87d7f4844ca963516637d249b14a0654f67f8047b6b265ae25b0cf30963e503", + "research/gauge44-slots/code/bind_providers_portable.py": "1d39bcc7b63ac158e021454beaae897d123e174360573762aecade3cd43193f6", + "research/gauge44-slots/code/bit_supplier_controls.py": "e6d33fb61a570c3f50669412acc467a3fd06ef0b806da6a75bc296c6ba2142a5", + "research/gauge44-slots/code/emit_allcold.py": "17c110c7c8d219e79e7dce36b19c4781e7effa800086cec03384387ad9acc7aa", + "research/gauge44-slots/code/freeze_spec.py": "f96c2b9cd886596bc7ab267f77abe9d16b6cbb5a724a5ad0a1d18d540369ed93", + "research/gauge44-slots/code/generated_identity.py": "c8af22719c0f3097a991a3f6ccac8f090afd2faba554745733d9ea88f2c25708", + "research/gauge44-slots/code/invoice_allcold.py": "141bd2fd58bbfb5b8d0fc8f56f61c45586d5608a5af3487c6b883dd987f998ec", + "research/gauge44-slots/code/prepare_global.py": "8c0dae301a8f34b77a5a462f840952d08ed120576212adf5051bc09bcad874dc", + "research/gauge44-slots/code/restore_parent.py": "69b7b25ff85e9b8160e233c1d415cc6a0272019e5c486dcec14cb6c349e7024d", + "research/gauge44-slots/code/witness.py": "779c5172894b992131e85be1e592ed2a1aec8c287b872ff42007d36a7291e444", + "research/gauge44-slots/construction/leaver/PIVOT-SWAP-k8.json": "3ef7acf0cf67442a532f25b53d5fbeda76d3a84524118df8e003ca69b5cac0bb", + "research/gauge44-slots/construction/slots/SLOT-PINS-k8.json": "55dd229684febecb80638eff9c6b3986623e8539c6c956753b350209c3e0efe2", + "research/gauge44-slots/construction/slots/verify_slots.py": "bc1c0e3e3d7c81dc1649f5be82cdd2399e543d46c24879cb975877bf9b7957be", + "research/gauge44-slots/data/OWNERS.json.gz": "32ca30cd1c652ef6ad43657273a08a157e1df3545e759ab36306a0d0b516fb4a", + "research/gauge44-slots/data/PLAN.json": "1dec4ca3af6d45d82286005cae4c5e56e7253adefb117d797da55c55c891af08", + "research/gauge44-slots/data/SPEC.json": "8e95ae8087124189cbd366d0e9d1c5ebededff536ff3501927b4b2a2e8dac70e", + "research/gauge44-slots/data/UPSTREAM-PINS.json": "ccc37ab7fbf78947fe02c7f57ea672d2e4eae8454cb1158ed964c75bf423869b", + "research/gauge44-slots/hosting/reuse_owners.py": "2106fe79bd89071e62a3a25c1e444531e14fb89f88b4bdeb72d7b40c91266402", + "research/gauge44-slots/independent/audit_local.py": "03afcfc9da428b3f6edac81c1fee7f277ab81b64998efae78380b63498dec6cd", + "research/gauge44-slots/inputs/PR589-EXPECTED.json": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4", + "research/gauge44-slots/verify_global.py": "16bd5e54598592e92e210f99065348c5df261b8350fdc688072ce053d15b088a", + "research/gauge44-slots/verify_manifest.py": "723d726dbbe5b65a49caecae0f1aab664a1413fb639abfd3e826a5a538e14e5b", + "research/k8-eight-ends-t16/CLAIM.json": "4ba568cb88f86a87a6c35df444b44b6f8c006ece6351279934ede873f5d61eab", + "research/k8-eight-ends-t16/MANIFEST.json": "f1f5c145121485f644a134873069fc465f312e9144ab43975fa95f599ce06f59", + "research/k8-eight-ends-t16/NOTICE.md": "a9e85b59dde61fbff0b006923b441cbd1419e24fa9802426785bca667437fdc0", + "research/k8-eight-ends-t16/OWNERS.json.gz": "a4c79743dcc93c4260fae00b3324b97983fcd56af8bff5414243d7258a4bc97b", + "research/k8-eight-ends-t16/PLAN.json.gz": "6561ecb8db5e24dd534d0f940f91830691ab375f925b20665ca0f019718e2b7a", + "research/k8-eight-ends-t16/PROOF.md": "7084e8a9fedd0d5902e95500da70982343fa725d8b68c2c3210a7b0a7bb2e664", + "research/k8-eight-ends-t16/README.md": "7aa1a4f5348ed9408cdebb2525eaabe50776259b939d7d49f6845503f3c585c3", + "research/k8-eight-ends-t16/SEARCH.json": "bf8efc27b2ca95f4bd15ebc719d2794a0e5d2edf26fc5b4cffc8c18dcb7f6d4a", + "research/k8-eight-ends-t16/SOURCE-PINS.json": "07515a4634303b85a54b570079f0efb373b36d586c72f7b023df3d2f495ad5a3", + "research/k8-eight-ends-t16/SPEC.json": "30d4dcc96f1361fcee1562681291763f6ee8c08fb1f93da1ea4fd2a42a1d0b5d", + "research/k8-eight-ends-t16/UPSTREAM.json": "23493f74fc09ac50442d9d83b7626d4760cfa24c785ca1d96fde8175bdd39fa6", + "research/k8-eight-ends-t16/discovery/ALIASES-REFRAMED.json": "a65d322ee757815e0de08e1f3c5796b5add8c744e1c3df292af917966b09adf0", + "research/k8-eight-ends-t16/discovery/BANK-STAGES.json": "ad8a80986982b67481ed4785663d83f56516542a79dc02c9ff50c991173c2771", + "research/k8-eight-ends-t16/discovery/FINAL-SEARCH.json": "ed936c49a0c15d69388b03f7c71bee50b2726be353f8dd52c6dcc56b1c12e1bd", + "research/k8-eight-ends-t16/discovery/HELPER-ALIASES.json": "ad1e0ffa923ce6632b2b86ad00ab004b5fc28ecd1d186e3c55727d1d6e834d73", + "research/k8-eight-ends-t16/discovery/PROMOTION-GROUPS.json": "221e05ae8c2b32594490b98ca12a96fc301789d1d80752c1d5f168469f8f8c07", + "research/k8-eight-ends-t16/discovery/PROMOTION-SCREEN.json": "6b5799744b7abbf4182ad594ede3984123ec559dfed1c1f50ad4f005ce713390", + "research/k8-eight-ends-t16/discovery/RETIRABLE-HELPERS.json": "3670ce299d538c4215fab08e88e7553903dfc595b756bcbc157178b0dc913159", + "research/k8-eight-ends-t16/discovery/SWAP-SEARCH.json": "70901cb74e475b35e0cffe99fbdae6ed74e5d315b92fdf900ef3a6ef7e542258", + "research/k8-eight-ends-t16/discovery/bank_screen.py": "b6c208ab449a9371bc812a19ed13edd8121f3f042769739fab9f964959a30b78", + "research/k8-eight-ends-t16/discovery/columns12-SEARCH.json.gz": "ee6f2925af9fc0dae9c2c511a35e34fe3d9983fb2df6b14de144d1166bba495a", + "research/k8-eight-ends-t16/discovery/columns12.log.gz": "7056db81c9131f484f1b09931bd3a722fa78e03e8e5898645da2eea3df75638b", + "research/k8-eight-ends-t16/discovery/columns144-SEARCH.json.gz": "b07b6a6dd29ec3cb03fa3827767e674b4ea06b3f2a555ba332f2dcb88ff918f9", + "research/k8-eight-ends-t16/discovery/columns144.log.gz": "bcf0b3ca6bd12a9032bfd27231e5a4efe2dd3b0edf874c9a01d0ba9dc8a3889d", + "research/k8-eight-ends-t16/discovery/columns24-SEARCH.json.gz": "9049ac77892a20aeeb30ccbf2a703c2b89cdbacf4f8f68a391cae10552c948b1", + "research/k8-eight-ends-t16/discovery/columns24.log.gz": "6aedcc3e39ee3ee8d2f9d4f33fd0107a1dec002323a6bf5e7e29308beafd3f91", + "research/k8-eight-ends-t16/discovery/columns48-SEARCH.json.gz": "adafcb5f6a7169a01a71220ea7ac94b389884112d00b1e9083961d69e4bbe467", + "research/k8-eight-ends-t16/discovery/columns48.log.gz": "0d69973436734bdce8399377f617dc728f099c1da237bdb829bf1ddf20ca4c4e", + "research/k8-eight-ends-t16/discovery/columns48b-SEARCH.json.gz": "fffcdb5b4f3679ab726a3abf9a8ed97559eec7975ca39ece8a140231efaad130", + "research/k8-eight-ends-t16/discovery/columns48b.log.gz": "c811f9ea49dd8ddf80f54556c7e387172b5ecbd8998ed4bea795e7c2b12121e9", + "research/k8-eight-ends-t16/discovery/double-calls-SEARCH.json.gz": "69df67741eae2afdd3f683f4021f478000dded1322c5820023faa77067ef6a9e", + "research/k8-eight-ends-t16/discovery/double-six-SEARCH.json.gz": "0364f028731baeccbf07953a98fabbf152b3685c5dfdf309d65398946ade9883", + "research/k8-eight-ends-t16/discovery/double-triples-SEARCH.json.gz": "f0040bb71eac1612bf730791a6d32bf13c7a065f0a2772a1149ced7aa71ffc77", + "research/k8-eight-ends-t16/discovery/helper_aliases.py": "3b996c21bf97e950e785c2f7f3ce025ce59c754c3679f97023ababfc5ac0b295", + "research/k8-eight-ends-t16/discovery/make_start.py": "3ba975c7947a3b74959a7e83a580a6f7b36e90d075157bac304a097d20e2cafd", + "research/k8-eight-ends-t16/discovery/promotion_groups.py": "5244da8cffc5f56698c134ca36230bcddbbdea935bc633e4975de50b47d785d2", + "research/k8-eight-ends-t16/discovery/reframe_aliases.py": "5e6342d583a7f3b99c940b6382527a000803eb728267fb4c101371b2b2128d89", + "research/k8-eight-ends-t16/discovery/search_calls.py": "273d3b3e1de5644af5a13a2c7cb18a34a3689b80830b614d7d2ed1da998a90ee", + "research/k8-eight-ends-t16/discovery/search_columns.py": "edbb093207e21ee4301382f00198c6eccb197949068e96c76e46a2e61dc90f82", + "research/k8-eight-ends-t16/discovery/search_uniform_blocks.py": "ab6308d536b37b14996e06b857a4f11433b3cb551444e836eb12ec560b452bb8", + "research/k8-eight-ends-t16/discovery/swap_frames.py": "cd89dd461142788817ac53c041808077d162a4d3bcfebee240307199aebadcc5", + "research/k8-eight-ends-t16/discovery/t16-calls-SEARCH.json.gz": "44df70fe291f3c0ec9ecd01791c02b9b52b29807c576353476542aaf76bbff40", + "research/k8-eight-ends-t16/discovery/t16-pairs-SEARCH.json.gz": "d32f9facc6b68c8dad2c9e4ead26aec913b076d4eb10214d18fa0c4c0b4762fa", + "research/k8-eight-ends-t16/discovery/t16-triples-SEARCH.json.gz": "57dd34fea35dee80e72a007e4cd044c50f00c1c794f03df6b0cbf292f54d8e0e", + "research/k8-eight-ends-t16/discovery/uniform-blocks-SEARCH.json.gz": "9c0a86f5befe738ebcf39badda84314150b060a911e0708d83d29a22423f149c", + "research/k8-eight-ends-t16/evidence/ADMISSION-CONTROLS.json": "6bdc8957237a01c0c5f667e2be2e889b02714fc6bc7a209672d09d5222073059", + "research/k8-eight-ends-t16/evidence/ALL-T-BOUND.json": "dde30a7151248cb9f316fe3816554dc165d050f5216e13797ceb30fe681a3a04", + "research/k8-eight-ends-t16/evidence/ASSEMBLY.json": "52c6af2fc860f7459f0fe3397639caecd5a8edf35ad76d4b22e99d19a79a2831", + "research/k8-eight-ends-t16/evidence/ASYNC-AUDIT.json": "644c15a99e207161a50eca01ddf1c7852e67504517fa4710d5490c3f65a4665a", + "research/k8-eight-ends-t16/evidence/AUDIT-LOCAL.json": "9fd252469f82b5ce5fc2f42b674445dfcac08d769768d00bede6cb5c99e9aa63", + "research/k8-eight-ends-t16/evidence/BIT-SUPPLIER-CONTROLS.json": "17939b88da6b6ad8a8220ed04ddf325679fc2f096c7d197938f10893a87383b4", + "research/k8-eight-ends-t16/evidence/END-CONTROLS.json": "e54407e7951f10c0eae5f310f49765429cf886a15dafb2afe80760715737d135", + "research/k8-eight-ends-t16/evidence/GLOBAL-PREFIX.json": "a6820bfad6fd665c08755fdff98d64069cb94dce337b0881e035a61bcb981cd2", + "research/k8-eight-ends-t16/evidence/IDLE-REMAINDER-FRAMES.json": "2d8b44b6bfe85df299bef25602529867b3316a20e41991786c2063b4c203d34c", + "research/k8-eight-ends-t16/evidence/INDEPENDENT-T16.json": "8311da24ffd4314b7d0857f7669de063fa76679af7fb67009513c513e47da5b3", + "research/k8-eight-ends-t16/evidence/NATIVE-STEPS.json": "782098b0ae9b7a87c75c47edc2e072c25a2c44d3e5417f44bf5f81ecf3d04a6e", + "research/k8-eight-ends-t16/evidence/OWNERS-AND-PROFILE.json": "f20ff5901bfe41cddf5c62d59f8c5361323f7e49b78c17d97173e9db5b3baf0f", + "research/k8-eight-ends-t16/evidence/PARENT-LIFT-RECEIPT.json": "d4705df4d65289e9ced31f625e34559fb26c1a4ca6f74559dd2e31a366b20a74", + "research/k8-eight-ends-t16/evidence/PREFIX-AND-INVOICE.json": "ef4775a3cd6bb1d52b9f43924b9bb1b378d52662c67e373fed20c1d5728caeb5", + "research/k8-eight-ends-t16/evidence/REPLAY-LOGS.json.gz": "81d8a6d5968f206177a4a1bd51baa530f1f9881867ce9925d341066dc1b33f21", + "research/k8-eight-ends-t16/evidence/REPLAY.json": "fa8db7880863b26de2999eab873f9d9b4661da651e17ac2f3b24a888efb1a341", + "research/k8-eight-ends-t16/evidence/RESULT.json": "33708ffb914369d4e25f34824bad32f2962d94027c2710df70fff83def7ec19f", + "research/k8-eight-ends-t16/evidence/STAGES.json": "b46df79356639d66a30fd50ca9d62b067037fb6072865d7399273ab20ccd3b23", + "research/k8-eight-ends-t16/independent/all_t_bound.py": "0cf8498903ef9e2a210886aa8360643b43a41f5bce33e187528835c325e3a059", + "research/k8-eight-ends-t16/vendor/pr1074/UPSTREAM-NOTICE.md": "a75967ebc34e3bf2ff2c25c08e6c7f1a61b0c0d171cfd1b62196ae2caaf2c610", + "research/k8-eight-ends-t16/vendor/pr1074/code/assemble.py": "15f6986a476bac76bcdc0bfcf51da115389b46f1950d2766b6822f757888b13a", + "research/k8-eight-ends-t16/vendor/pr1074/code/assembly_controls.py": "da7e981ae1b9f099d4e1524cb4f3ba1116011936ebe378692889b5dbfa99029d", + "research/k8-eight-ends-t16/vendor/pr1074/code/audit_allcold.py": "1467a2acb654e62552c69fb9a7c4c85f70a02120881d222313865058ab71a6cc", + "research/k8-eight-ends-t16/vendor/pr1074/code/bind_providers_portable.py": "1d39bcc7b63ac158e021454beaae897d123e174360573762aecade3cd43193f6", + "research/k8-eight-ends-t16/vendor/pr1074/code/bit_supplier_controls.py": "e6d33fb61a570c3f50669412acc467a3fd06ef0b806da6a75bc296c6ba2142a5", + "research/k8-eight-ends-t16/vendor/pr1074/code/emit_allcold.py": "354367e1fd6185a67b04f4268bcae4d502e47b18cb2131e247f5bcab5b3a769e", + "research/k8-eight-ends-t16/vendor/pr1074/code/freeze_spec.py": "5971eecac6d6fbcb53244b80f1b9d7232012dc32876fab511214a5addebbe6c2", + "research/k8-eight-ends-t16/vendor/pr1074/code/generated_identity.py": "c8af22719c0f3097a991a3f6ccac8f090afd2faba554745733d9ea88f2c25708", + "research/k8-eight-ends-t16/vendor/pr1074/code/invoice_allcold.py": "71eb57514e28ced97251e0507105f654f59885ec4d40486a780bf166098858a8", + "research/k8-eight-ends-t16/vendor/pr1074/code/prepare_global.py": "8c0dae301a8f34b77a5a462f840952d08ed120576212adf5051bc09bcad874dc", + "research/k8-eight-ends-t16/vendor/pr1074/code/restore_parent.py": "69b7b25ff85e9b8160e233c1d415cc6a0272019e5c486dcec14cb6c349e7024d", + "research/k8-eight-ends-t16/vendor/pr1074/code/witness.py": "779c5172894b992131e85be1e592ed2a1aec8c287b872ff42007d36a7291e444", + "research/k8-eight-ends-t16/vendor/pr1074/construction/leaver/PIVOT-SWAP-k8.json": "3ef7acf0cf67442a532f25b53d5fbeda76d3a84524118df8e003ca69b5cac0bb", + "research/k8-eight-ends-t16/vendor/pr1074/data/UPSTREAM-PINS.json": "ccc37ab7fbf78947fe02c7f57ea672d2e4eae8454cb1158ed964c75bf423869b", + "research/k8-eight-ends-t16/vendor/pr1074/inputs/PR589-EXPECTED.json": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4", + "research/k8-eight-ends-t16/vendor/pr1074/t16/build_parent.py": "82e274d0c7a94f9bf0468dd37f0505d0c42017559ebb4ba8c079a1f4e403d91e", + "research/k8-eight-ends-t16/vendor/pr1074/t16/indep16.py": "1beb512a1d072f81d3e8e492c8827636029686897093bd433e4d4c92d0c830c7", + "research/k8-eight-ends-t16/vendor/pr1074/t16/lift16.py": "072fe6ac032543d5106631f9b4aa36103269b64ab72061d97ec604f648830689", + "research/k8-eight-ends-t16/vendor/pr1074/verify_t16.py": "050e2dfba59911b8f29fd94422833d421367a0ad01c5e4ae916a75a235ee5e46", + "research/k8-eight-ends-t16/verify.py": "e910ca38941209be9b32c3fa6d784e84a824bef9767d2bf492f298d4889cfe92", + "research/k8-eight-ends/CLAIM.json": "65f620750f2a438316684b74cdf7cd990d59626b5c073e7dde0fd735ff3e158d", + "research/k8-eight-ends/FULL-WORD.json.gz": "d28c607df2bc4a82684d3fe47cfb3dba04e3bd14b247c7d4a62a03dff7b2836c", + "research/k8-eight-ends/MANIFEST.json": "bbdfe8589b21557ee0e0625cc485e7afef1f55fd31609bc5f4f9b30de4f6cbf9", + "research/k8-eight-ends/NOTICE.md": "820fa13161f857c221f2c4099dd2985c7ff72249dc7a0221bc00fd0c1b9760e5", + "research/k8-eight-ends/OWNERS.json.gz": "c41fdf51541ecc91af914f264967f3633570500994f8866daf642440a5d843dd", + "research/k8-eight-ends/PLAN.json.gz": "a3e9e390da3136655606ac919ec60696e2f704457ff01ef9e4d07e90534ab2d4", + "research/k8-eight-ends/PROOF.md": "1ee3b7d22a39ccb0877ca32f176786b2545dd2b86bbe986eec833b96cd17ba6b", + "research/k8-eight-ends/README.md": "0f2bc8afeff4054cb8fb62819563a6214d53af916ebf6f28bb2fcd972814362c", + "research/k8-eight-ends/RECIPE.json": "6a5d91b95bdba641ab4cc0e3c9b7f0f2adcc5ef22bef7f732d5d76cb0b6fab6c", + "research/k8-eight-ends/SEARCH.json": "f1816698aa4d7deb48ef7e98a711fdc0c74d67bd336d4b8f48b46fe191d7d1b1", + "research/k8-eight-ends/SOURCE-PINS.json": "6b85ed22262e23db1ff0518d874d4e3ee1b4317d642fabdc9747cecbd04ef420", + "research/k8-eight-ends/SPEC.json": "555cf868f29c8173b2faf8243aea30ee29f3e12f694c6cb3865a06981592af24", + "research/k8-eight-ends/build_word.py": "18691b1fad3bc798b7ad58b39b433f405e9bb4ec266af0303b563f11b07d956f", + "research/k8-eight-ends/discovery/END-COMBINATIONS.json": "db6353685f6f344a6e3a4b8476dde4858fa2fad65fe4e74abcecab93eb07a79f", + "research/k8-eight-ends/discovery/END-GROUP-SCREEN.json": "b197a014997ec869cc2768b68070e9ad3cd6d19633b366085a8061a3523fe3ef", + "research/k8-eight-ends/discovery/END-GROUPS.json": "19b456b91852df5ee2aec79a16ab454c5772bd5160d1cee42e4df6f0cb211bd4", + "research/k8-eight-ends/discovery/RETIME-CENSUS.json": "40ea9706b94cd23a6c37ab01afb6e945ab59ac43d1a61433583cf1d297cf57dd", + "research/k8-eight-ends/discovery/SEARCH-TRACES.json.gz": "eaa157000003e807fb466d6c7bfc032dc74857ae4afc5de2ca6d1bf1a631c37f", + "research/k8-eight-ends/discovery/SOURCE-CENSUS.json": "aeadcc466b01fd5a2498037f3a83dcecdde91d30327a15c684d77645489e6f69", + "research/k8-eight-ends/discovery/SOURCE-REFRAME.json": "d69170ce6443ffaf890a5e3e2b8cecdb74ba4e7b75273738ed367be5643b01a1", + "research/k8-eight-ends/discovery/combine_ends.py": "ea0e79e0bf4ea7d44cadd179fb5bb6ff13cf6cd960362a1e2e07c63c1969b7f8", + "research/k8-eight-ends/discovery/end_groups.py": "190a44e768daf0d9076158da9f00e4aa7e682e7df90749d18fbd55f1a04b9b09", + "research/k8-eight-ends/discovery/frame_model.py": "dee9899272846ee954f8daf6e9f60c9e073c86489b2a594d4d9a4a9899cbd0e9", + "research/k8-eight-ends/discovery/minimize_recipe.py": "8fa2216d1228c12a08b5e93b084ce1426ebe99b5abb7f6e614173b56bedb459d", + "research/k8-eight-ends/discovery/prepare_new.py": "b2995d74b63010aa3bd5e4cdc59666a0ca0d9d4244340c694e8eed6171231c0d", + "research/k8-eight-ends/discovery/resize_owners.py": "af9b632d51f6b4beddd87bf75d6e36eb3f58b7e467e711208f304a774f8b26f0", + "research/k8-eight-ends/discovery/retime_sources.py": "35600042b16447b24289c73a41462d4eeb6600117529df5baf4fed5aa389d898", + "research/k8-eight-ends/discovery/screen_end_groups.py": "a29814cfc5f3f86dc62272fd3cceb2fb0456a3aa25c8b183980291b744e9ab54", + "research/k8-eight-ends/discovery/search_calls.py": "5df48ab7775bfee767d71dd8c47585977922568b532c29f4528f2c8ca5ab364d", + "research/k8-eight-ends/discovery/source_census.py": "9808b026a8a7556fbf171f57ca46b32c2e33b36eeb2924e7eee24abb2a7b3853", + "research/k8-eight-ends/discovery/test_structures.py": "7c550f1c00d58fa1df668179e09c0fd9fe61c35029f548f973727f0b36706e31", + "research/k8-eight-ends/end_controls.py": "9f4a2ad05a3602be3bd89bb1a1e3fc40bb78eb3ad8de3f66aa19e44e53e30e2a", + "research/k8-eight-ends/evidence/ADMISSION-CONTROLS.json": "b7df5cb7695f8de70c674a03c10a36682d85b958340d392c8d61e9b969111179", + "research/k8-eight-ends/evidence/ASSEMBLY.json": "1cf819f87c1e550c78de98206a52e9aff04ec47022e5a63987bcd1dd5d2e51f6", + "research/k8-eight-ends/evidence/ASYNC-AUDIT.json": "2b056ae65d212cfdf4d83778b9be47dc7a9ded6626feb3a20ae2de6ead8dbb79", + "research/k8-eight-ends/evidence/AUDIT-LOCAL.json": "4ebd818fe459c8b729aaf385d6b2946e58316414a9c29c5ba6a2335d63af7ecf", + "research/k8-eight-ends/evidence/BIT-SUPPLIER-CONTROLS.json": "4fbf09922859926ed79eb4874a0c3414a13991de2ffc64d30a382e7eecb2c2a4", + "research/k8-eight-ends/evidence/CLIFFORD-REVIEW.json": "2bfc112221995431c25a7257fdda5a2e9b2631c1712a48ab428f946849cbac91", + "research/k8-eight-ends/evidence/END-CONTROLS.json": "e54407e7951f10c0eae5f310f49765429cf886a15dafb2afe80760715737d135", + "research/k8-eight-ends/evidence/ENDS-8-AUDIT.json": "5381c41fa10fdccbc5c5bdc7059ad839e508d7b8bc3a139bc8ad6b45c20b01c3", + "research/k8-eight-ends/evidence/INDEPENDENT-LOCAL-REPLAY.json": "00b418af082ad30474fcdeecd121d96af305c2686756a0ee30178fe1ccd5dd99", + "research/k8-eight-ends/evidence/LOCAL-CHECKS.json": "3f4c8aba4736091f7efee0d31668d230626e3daa1438dfed096efd04d89b91ba", + "research/k8-eight-ends/evidence/NATIVE-STEPS.json": "02f6ea9122362ba1e408e72c331ffc850a2fbd1593afb06554aa0ab5c7aee0f6", + "research/k8-eight-ends/evidence/OWNERS-AND-PROFILE.json": "a04d3db0d157b197d9395967163e155f0d8775a06db2ca4318258830e2abdaa9", + "research/k8-eight-ends/evidence/PREFIX-AND-INVOICE.json": "66650384488db73bf3d5c7742abaa9c116877845bbb4ef46d6fffe235ae7d1c0", + "research/k8-eight-ends/evidence/PREPARATION.json": "cd980d9b80de65d1bd9358d590a479fb85d75fc4e468a12539cd5a0388190e8d", + "research/k8-eight-ends/evidence/REPLAY.json": "fa6b65403a28ce8c717412b0d90dd4c702bcba7e3c530bca932f921f0dba75e2", + "research/k8-eight-ends/evidence/RESULT.json": "904b0cb2082f6f109845d30f6ee4bb6f766ea493c4cee6a637634362a30785b0", + "research/k8-eight-ends/evidence/STEPS.json": "5577123fa4422fb80f412dc3713bbd7eea5c4c50b63db635f01585457c9d2960", + "research/k8-eight-ends/evidence/WRAPPER-CHECKS.json": "b6c7fdef5893b117434f39b6561b80504482fa748e23b840f77a07b137e1d1ea", + "research/k8-eight-ends/replay_native.py": "1fb596fbafdb19140f483cd34db2994c571e3b962e33b8ea9b3ddc486e37def6", + "research/k8-eight-ends/verify.py": "d57061431e087fb755382e3b362ea7421e5ee3dfae5b3ed81ce5228278ba58b6" +} diff --git a/research/crosscall-kernel-demotion/vendor/pr1148/SPEC.json b/research/crosscall-kernel-demotion/vendor/pr1148/SPEC.json new file mode 100644 index 0000000000..a30b18a06a --- /dev/null +++ b/research/crosscall-kernel-demotion/vendor/pr1148/SPEC.json @@ -0,0 +1,1971 @@ +{ + "schema": "witness-spec/1", + "name": "k8-three-demotions", + "data": { + "plan_sha256": "d85e8bc431071895cab4b981205138957172418101e567fa9c3245a05f34405f", + "owners_sha256": "93cb570c9496725ed5204d9f890ddf337ed8c3fb1a1b980de3e905f65e71b2dd" + }, + "dispatch": [ + [ + 0, + 0, + "gauge44" + ], + [ + 0, + 8, + "gauge44" + ], + [ + 0, + 1, + "gauge44" + ], + [ + 0, + 9, + "gauge44" + ], + [ + 1, + 0, + "gauge44" + ], + [ + 1, + 8, + "gauge44" + ], + [ + 0, + 2, + "gauge44" + ], + [ + 0, + 10, + "gauge44" + ], + [ + 1, + 1, + "gauge44" + ], + [ + 1, + 9, + "gauge44" + ], + [ + 2, + 0, + "gauge44" + ], + [ + 2, + 8, + "gauge44" + ], + [ + 0, + 3, + "gauge44" + ], + [ + 0, + 11, + "gauge44" + ], + [ + 1, + 2, + "gauge44" + ], + [ + 1, + 10, + "gauge44" + ], + [ + 2, + 1, + "gauge44" + ], + [ + 2, + 9, + "gauge44" + ], + [ + 3, + 0, + "gauge44" + ], + [ + 3, + 8, + "gauge44" + ], + [ + 0, + 4, + "gauge44" + ], + [ + 0, + 12, + "gauge44" + ], + [ + 1, + 3, + "gauge44" + ], + [ + 1, + 11, + "gauge44" + ], + [ + 2, + 2, + "gauge44" + ], + [ + 2, + 10, + "gauge44" + ], + [ + 3, + 1, + "gauge44" + ], + [ + 3, + 9, + "gauge44" + ], + [ + 4, + 0, + "gauge44" + ], + [ + 4, + 8, + "gauge44" + ], + [ + 0, + 5, + "gauge44" + ], + [ + 0, + 13, + "gauge44" + ], + [ + 1, + 4, + "gauge44" + ], + [ + 1, + 12, + "gauge44" + ], + [ + 2, + 3, + "gauge44" + ], + [ + 2, + 11, + "gauge44" + ], + [ + 3, + 2, + "gauge44" + ], + [ + 3, + 10, + "gauge44" + ], + [ + 4, + 1, + "gauge44" + ], + [ + 4, + 9, + "gauge44" + ], + [ + 5, + 0, + "gauge44" + ], + [ + 5, + 8, + "gauge44" + ], + [ + 0, + 6, + "gauge44" + ], + [ + 0, + 14, + "gauge44" + ], + [ + 1, + 5, + "gauge44" + ], + [ + 1, + 13, + "gauge44" + ], + [ + 2, + 4, + "gauge44" + ], + [ + 2, + 12, + "gauge44" + ], + [ + 3, + 3, + "gauge44" + ], + [ + 3, + 11, + "gauge44" + ], + [ + 4, + 2, + "gauge44" + ], + [ + 4, + 10, + "gauge44" + ], + [ + 5, + 1, + "gauge44" + ], + [ + 5, + 9, + "gauge44" + ], + [ + 0, + 7, + "gauge44" + ], + [ + 0, + 15, + "gauge44" + ], + [ + 6, + 0, + "gauge44" + ], + [ + 6, + 8, + "gauge44" + ], + [ + 1, + 6, + "gauge44" + ], + [ + 1, + 14, + "gauge44" + ], + [ + 2, + 5, + "gauge44" + ], + [ + 2, + 13, + "gauge44" + ], + [ + 3, + 4, + "gauge44" + ], + [ + 3, + 12, + "gauge44" + ], + [ + 4, + 3, + "gauge44" + ], + [ + 4, + 11, + "gauge44" + ], + [ + 5, + 2, + "gauge44" + ], + [ + 5, + 10, + "gauge44" + ], + [ + 6, + 1, + "gauge44" + ], + [ + 6, + 9, + "gauge44" + ], + [ + 1, + 7, + "gauge44" + ], + [ + 1, + 15, + "gauge44" + ], + [ + 7, + 0, + "gauge44" + ], + [ + 7, + 8, + "gauge44" + ], + [ + 2, + 6, + "gauge44" + ], + [ + 2, + 14, + "gauge44" + ], + [ + 3, + 5, + "gauge44" + ], + [ + 3, + 13, + "gauge44" + ], + [ + 4, + 4, + "gauge44" + ], + [ + 4, + 12, + "gauge44" + ], + [ + 5, + 3, + "gauge44" + ], + [ + 5, + 11, + "gauge44" + ], + [ + 6, + 2, + "gauge44" + ], + [ + 6, + 10, + "gauge44" + ], + [ + 7, + 1, + "gauge44" + ], + [ + 7, + 9, + "gauge44" + ], + [ + 2, + 7, + "gauge44" + ], + [ + 2, + 15, + "gauge44" + ], + [ + 8, + 0, + "gauge44" + ], + [ + 8, + 8, + "gauge44" + ], + [ + 3, + 6, + "gauge44" + ], + [ + 3, + 14, + "gauge44" + ], + [ + 4, + 5, + "gauge44" + ], + [ + 4, + 13, + "gauge44" + ], + [ + 5, + 4, + "gauge44" + ], + [ + 5, + 12, + "gauge44" + ], + [ + 6, + 3, + "gauge44" + ], + [ + 6, + 11, + "gauge44" + ], + [ + 7, + 2, + "gauge44" + ], + [ + 7, + 10, + "gauge44" + ], + [ + 8, + 1, + "gauge44" + ], + [ + 8, + 9, + "gauge44" + ], + [ + 3, + 7, + "gauge44" + ], + [ + 3, + 15, + "gauge44" + ], + [ + 4, + 6, + "gauge44" + ], + [ + 4, + 14, + "gauge44" + ], + [ + 5, + 5, + "gauge44" + ], + [ + 5, + 13, + "gauge44" + ], + [ + 6, + 4, + "gauge44" + ], + [ + 6, + 12, + "gauge44" + ], + [ + 7, + 3, + "gauge44" + ], + [ + 7, + 11, + "gauge44" + ], + [ + 8, + 2, + "gauge44" + ], + [ + 8, + 10, + "gauge44" + ], + [ + 4, + 7, + "gauge44" + ], + [ + 4, + 15, + "gauge44" + ], + [ + 5, + 6, + "gauge44" + ], + [ + 5, + 14, + "gauge44" + ], + [ + 6, + 5, + "gauge44" + ], + [ + 6, + 13, + "gauge44" + ], + [ + 7, + 4, + "gauge44" + ], + [ + 7, + 12, + "gauge44" + ], + [ + 8, + 3, + "gauge44" + ], + [ + 8, + 11, + "gauge44" + ], + [ + 5, + 7, + "gauge44" + ], + [ + 5, + 15, + "gauge44" + ], + [ + 6, + 6, + "gauge44" + ], + [ + 6, + 14, + "gauge44" + ], + [ + 7, + 5, + "gauge44" + ], + [ + 7, + 13, + "gauge44" + ], + [ + 8, + 4, + "gauge44" + ], + [ + 8, + 12, + "gauge44" + ], + [ + 6, + 7, + "gauge44" + ], + [ + 6, + 15, + "gauge44" + ], + [ + 7, + 6, + "gauge44" + ], + [ + 7, + 14, + "gauge44" + ], + [ + 8, + 5, + "gauge44" + ], + [ + 8, + 13, + "gauge44" + ], + [ + 7, + 7, + "gauge44" + ], + [ + 7, + 15, + "gauge44" + ], + [ + 8, + 6, + "gauge44" + ], + [ + 8, + 14, + "gauge44" + ], + [ + 8, + 7, + "gauge44" + ], + [ + 8, + 15, + "gauge44" + ] + ], + "call_order": [ + [ + 0, + 0 + ], + [ + 0, + 8 + ], + [ + 0, + 1 + ], + [ + 0, + 9 + ], + [ + 1, + 0 + ], + [ + 1, + 8 + ], + [ + 0, + 2 + ], + [ + 0, + 10 + ], + [ + 1, + 1 + ], + [ + 1, + 9 + ], + [ + 2, + 0 + ], + [ + 2, + 8 + ], + [ + 0, + 3 + ], + [ + 0, + 11 + ], + [ + 1, + 2 + ], + [ + 1, + 10 + ], + [ + 2, + 1 + ], + [ + 2, + 9 + ], + [ + 3, + 0 + ], + [ + 3, + 8 + ], + [ + 0, + 4 + ], + [ + 0, + 12 + ], + [ + 1, + 3 + ], + [ + 1, + 11 + ], + [ + 2, + 2 + ], + [ + 2, + 10 + ], + [ + 3, + 1 + ], + [ + 3, + 9 + ], + [ + 4, + 0 + ], + [ + 4, + 8 + ], + [ + 0, + 5 + ], + [ + 0, + 13 + ], + [ + 1, + 4 + ], + [ + 1, + 12 + ], + [ + 2, + 3 + ], + [ + 2, + 11 + ], + [ + 3, + 2 + ], + [ + 3, + 10 + ], + [ + 4, + 1 + ], + [ + 4, + 9 + ], + [ + 5, + 0 + ], + [ + 5, + 8 + ], + [ + 0, + 6 + ], + [ + 0, + 14 + ], + [ + 1, + 5 + ], + [ + 1, + 13 + ], + [ + 2, + 4 + ], + [ + 2, + 12 + ], + [ + 3, + 3 + ], + [ + 3, + 11 + ], + [ + 4, + 2 + ], + [ + 4, + 10 + ], + [ + 5, + 1 + ], + [ + 5, + 9 + ], + [ + 0, + 7 + ], + [ + 0, + 15 + ], + [ + 6, + 0 + ], + [ + 6, + 8 + ], + [ + 1, + 6 + ], + [ + 1, + 14 + ], + [ + 2, + 5 + ], + [ + 2, + 13 + ], + [ + 3, + 4 + ], + [ + 3, + 12 + ], + [ + 4, + 3 + ], + [ + 4, + 11 + ], + [ + 5, + 2 + ], + [ + 5, + 10 + ], + [ + 6, + 1 + ], + [ + 6, + 9 + ], + [ + 1, + 7 + ], + [ + 1, + 15 + ], + [ + 7, + 0 + ], + [ + 7, + 8 + ], + [ + 2, + 6 + ], + [ + 2, + 14 + ], + [ + 3, + 5 + ], + [ + 3, + 13 + ], + [ + 4, + 4 + ], + [ + 4, + 12 + ], + [ + 5, + 3 + ], + [ + 5, + 11 + ], + [ + 6, + 2 + ], + [ + 6, + 10 + ], + [ + 7, + 1 + ], + [ + 7, + 9 + ], + [ + 2, + 7 + ], + [ + 2, + 15 + ], + [ + 8, + 0 + ], + [ + 8, + 8 + ], + [ + 3, + 6 + ], + [ + 3, + 14 + ], + [ + 4, + 5 + ], + [ + 4, + 13 + ], + [ + 5, + 4 + ], + [ + 5, + 12 + ], + [ + 6, + 3 + ], + [ + 6, + 11 + ], + [ + 7, + 2 + ], + [ + 7, + 10 + ], + [ + 8, + 1 + ], + [ + 8, + 9 + ], + [ + 3, + 7 + ], + [ + 3, + 15 + ], + [ + 4, + 6 + ], + [ + 4, + 14 + ], + [ + 5, + 5 + ], + [ + 5, + 13 + ], + [ + 6, + 4 + ], + [ + 6, + 12 + ], + [ + 7, + 3 + ], + [ + 7, + 11 + ], + [ + 8, + 2 + ], + [ + 8, + 10 + ], + [ + 4, + 7 + ], + [ + 4, + 15 + ], + [ + 5, + 6 + ], + [ + 5, + 14 + ], + [ + 6, + 5 + ], + [ + 6, + 13 + ], + [ + 7, + 4 + ], + [ + 7, + 12 + ], + [ + 8, + 3 + ], + [ + 8, + 11 + ], + [ + 5, + 7 + ], + [ + 5, + 15 + ], + [ + 6, + 6 + ], + [ + 6, + 14 + ], + [ + 7, + 5 + ], + [ + 7, + 13 + ], + [ + 8, + 4 + ], + [ + 8, + 12 + ], + [ + 6, + 7 + ], + [ + 6, + 15 + ], + [ + 7, + 6 + ], + [ + 7, + 14 + ], + [ + 8, + 5 + ], + [ + 8, + 13 + ], + [ + 7, + 7 + ], + [ + 7, + 15 + ], + [ + 8, + 6 + ], + [ + 8, + 14 + ], + [ + 8, + 7 + ], + [ + 8, + 15 + ] + ], + "width_spot_helpers": [ + 258, + 270, + 282, + 294 + ], + "providers": { + "gauge44": { + "inventory": { + "4": 44, + "5": 44, + "7": 38, + "8": 114, + "9": 240 + }, + "native_negative_controls": 25, + "phase_edges": 2904, + "expected_profile": { + "1": 2372, + "2": 494, + "3": 412, + "4": 130, + "5": 82, + "8": 8 + }, + "artifact_semantic_sha256": { + "CANONICAL-WORD.json.gz": "01c5f60fb0cb2ae522ec926168281023f4315d2be76d75b0c5d5b341014a8c9e", + "LOCAL-PROGRAMS.json.gz": "0b74225d802107084e08cff09a658af6cb0399daab495db6e42b6d088730c0c4", + "LOCAL-CHECKS.json": "f5acbca2609d813e77c7de46deb406a0b381cf81d242d6536125a7106b90659d", + "INDEPENDENT-LOCAL-REPLAY.json": "ae1c832371024ab7c42ed2d02f0bea552df52f84f184959a47a236484b7c2dc2", + "CLIFFORD-RECIPES.json": "803271ac4098ce1bca6d3dcc20dd9e6eb650843ad2c07d98c93e1c78f0873463", + "CLIFFORD-REVIEW.json": "046e89ed60e9745cfc27c8d98e269d0bece9271b9f99f9aa00ee916c945ccff3", + "RESIDUAL-ADAPTERS.json": "f96536a306c4202865667b2a213b7dacb0292fe5354dc412c1d6022c8d68b4cd" + }, + "entering": 192, + "entrance": 372, + "width_digest": "1223f12ba6091bbd427fdbcbddda5217d24786c471102195cdfbbca562fcf27c", + "program_hashes": { + "backward": "d8a1b20df928953caf4dbdc5d4ace9e94c8c26db07cc026805bb63300a4e6b22", + "forward": "551a1211d208774f826eea0e7f0bf1c71b2a6668fc6d5e663a154baed2b2c405" + }, + "artifacts": { + "LOCAL-CHECKS.json": "b6da3ccbc8a9422c8134b2fe351e783ea01390805afc1df433f9af38fb6f4861", + "CLIFFORD-RECIPES.json": "803271ac4098ce1bca6d3dcc20dd9e6eb650843ad2c07d98c93e1c78f0873463", + "RESIDUAL-ADAPTERS.json": "cc655002a80209e3935e7d2b9baede9437360e2d23238609712317b7fa26dc56" + }, + "complete_contract": { + "local": { + "backward": { + "events": 24771, + "macros": 19693, + "real_component_primitives": 198814, + "prefix_l1": "14824960514781440791821/64", + "prefix_bits": 68, + "coefficient_work_primitive_count": 98365, + "all_exact_columns": 704, + "dirty_helper_columns": 480, + "all_dirty_helper_columns_restored": true, + "private_centres_and_coefficient_work_cleared": true, + "pre_wrappers": 240, + "post_wrappers": 240, + "endpoint_evidence": "Hash-bound fresh INDEPENDENT-LOCAL-REPLAY.json" + }, + "forward": { + "events": 24771, + "macros": 19693, + "real_component_primitives": 198766, + "prefix_l1": "2765345294379392599/1024", + "prefix_bits": 52, + "coefficient_work_primitive_count": 98333, + "all_exact_columns": 704, + "dirty_helper_columns": 480, + "all_dirty_helper_columns_restored": true, + "private_centres_and_coefficient_work_cleared": true, + "pre_wrappers": 240, + "post_wrappers": 240, + "endpoint_evidence": "Hash-bound fresh INDEPENDENT-LOCAL-REPLAY.json" + } + }, + "helpers": 480, + "centres": 8, + "v": 112, + "h": 9, + "n": 704, + "entering_helpers": 192, + "entrance_rank": 372, + "terminal_codimension": 214, + "hyperplane_ended_helpers": 78, + "cold_hyperplane_ended_helpers": 48, + "width_inventory": { + "4": 44, + "5": 44, + "7": 38, + "8": 114, + "9": 240 + }, + "widths": [ + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 4, + 9, + 4, + 9, + 9, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 4, + 9, + 4, + 9, + 9, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 4, + 9, + 4, + 9, + 8, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 4, + 9, + 4, + 9, + 8, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 4, + 9, + 4, + 9, + 9, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 4, + 9, + 4, + 9, + 9, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 4, + 9, + 4, + 9, + 9, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 4, + 9, + 4, + 9, + 9, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 8, + 8, + 8, + 8, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 7, + 7, + 8, + 8, + 8, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 8, + 8, + 9, + 8, + 8, + 9, + 9, + 9, + 9, + 8, + 9, + 7, + 7, + 8, + 9, + 8, + 8, + 9, + 9, + 9, + 9, + 8, + 9, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 9, + 7, + 7, + 7, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 9, + 7, + 8, + 8, + 9, + 9, + 9, + 9, + 8, + 8, + 8, + 8, + 7, + 7, + 7, + 7, + 9, + 8, + 9, + 8, + 8, + 8, + 8, + 8, + 7, + 7, + 9, + 8, + 9, + 8, + 7, + 7, + 7, + 7, + 8, + 8, + 8, + 8, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 8, + 8, + 8, + 5, + 8, + 5, + 5, + 5, + 8, + 8, + 8, + 5, + 8, + 5, + 5, + 5, + 8, + 8, + 8, + 5, + 8, + 5, + 5, + 5, + 8, + 8, + 8, + 5, + 8, + 5, + 5, + 5, + 8, + 8, + 8, + 4, + 8, + 4, + 4, + 4, + 8, + 8, + 8, + 4, + 8, + 4, + 4, + 4, + 8, + 8, + 8, + 5, + 8, + 5, + 5, + 5, + 8, + 8, + 8, + 4, + 8, + 4, + 4, + 4, + 8, + 8, + 8, + 5, + 8, + 5, + 5, + 5, + 8, + 8, + 8, + 5, + 8, + 5, + 5, + 5, + 8, + 8, + 8, + 5, + 8, + 5, + 5, + 5, + 8, + 8, + 8, + 5, + 8, + 5, + 5, + 5, + 8, + 8, + 8, + 5, + 8, + 5, + 5, + 5, + 8, + 8, + 8, + 5, + 8, + 5, + 5, + 5 + ], + "local_adapters": 387120, + "local_primitive_bound": 10039700351134, + "compiler": 25934336, + "children": 3498, + "paid_profile": { + "1": 2372, + "2": 494, + "3": 412, + "4": 130, + "5": 82, + "8": 8 + }, + "program_hashes": { + "backward": "d8a1b20df928953caf4dbdc5d4ace9e94c8c26db07cc026805bb63300a4e6b22", + "forward": "551a1211d208774f826eea0e7f0bf1c71b2a6668fc6d5e663a154baed2b2c405" + }, + "semantic_artifact_sha256": { + "CANONICAL-WORD.json.gz": "01c5f60fb0cb2ae522ec926168281023f4315d2be76d75b0c5d5b341014a8c9e", + "LOCAL-PROGRAMS.json.gz": "0b74225d802107084e08cff09a658af6cb0399daab495db6e42b6d088730c0c4", + "LOCAL-CHECKS.json": "f5acbca2609d813e77c7de46deb406a0b381cf81d242d6536125a7106b90659d", + "INDEPENDENT-LOCAL-REPLAY.json": "ae1c832371024ab7c42ed2d02f0bea552df52f84f184959a47a236484b7c2dc2", + "CLIFFORD-RECIPES.json": "803271ac4098ce1bca6d3dcc20dd9e6eb650843ad2c07d98c93e1c78f0873463", + "CLIFFORD-REVIEW.json": "046e89ed60e9745cfc27c8d98e269d0bece9271b9f99f9aa00ee916c945ccff3", + "RESIDUAL-ADAPTERS.json": "f96536a306c4202865667b2a213b7dacb0292fe5354dc412c1d6022c8d68b4cd" + } + }, + "semantic_phase_sha256": "046e89ed60e9745cfc27c8d98e269d0bece9271b9f99f9aa00ee916c945ccff3", + "expected_local": { + "forward": { + "events": 24771, + "macros": 19693, + "real_component_primitives": 198766, + "prefix_l1": "2765345294379392599/1024", + "coefficient_work_primitive_count": 98333 + }, + "backward": { + "events": 24771, + "macros": 19693, + "real_component_primitives": 198814, + "prefix_l1": "14824960514781440791821/64", + "coefficient_work_primitive_count": 98365 + } + }, + "wrappers": 240 + } + }, + "expected": { + "gain_baseline_kappa": "0.001674622497877364", + "hosted_residuals": 69120, + "rank_mass": 1041408, + "actual_73column_sigmas": 10580, + "cross_replica_helper_roles": 59636, + "idle_remainders": 5279, + "idle_remainder_profile": { + "1": 360, + "24": 1, + "48": 4918 + }, + "global_profile": { + "1": 341928, + "2": 71136, + "3": 59328, + "4": 18720, + "5": 11808, + "8": 1152, + "24": 1, + "48": 4918 + }, + "live": 14336, + "physical": 14826, + "conservative_kappa_decimal": "0.001675121644942436", + "kappa_decimal": "0.001675121647789207", + "complex_lower": "13423459109255787537/8000000000000000000000", + "conservative_complex_lower": "13423459086405125339/8000000000000000000000", + "kappa": "1675121647789207/1000000000000000000", + "assembly_controls_rejected": 69, + "provider_counts": { + "gauge44": 144 + }, + "mutations_rejected": 15 + }, + "pivot_swap": { + "recipe": "construction/leaver/PIVOT-SWAP-k8.json", + "sha256": "3ef7acf0cf67442a532f25b53d5fbeda76d3a84524118df8e003ca69b5cac0bb" + } +} diff --git a/research/crosscall-kernel-demotion/verify.py b/research/crosscall-kernel-demotion/verify.py new file mode 100644 index 0000000000..111639a5d3 --- /dev/null +++ b/research/crosscall-kernel-demotion/verify.py @@ -0,0 +1,80 @@ +"""Fresh finite certificate of a conditional construction. Apache-2.0. +Standard library only; no network, search, WSL, GPU or persistent workers. +""" +import argparse,copy,gzip,hashlib,importlib.util,json,shutil,subprocess,sys,time +from fractions import Fraction as Q +from pathlib import Path +P=Path(__file__).resolve().parent +def need(x,m): + if not x:raise RuntimeError(m) +def read(p): + b=p.read_bytes();return json.loads(gzip.decompress(b) if p.suffix=='.gz' else b) +def sha(p):return hashlib.sha256(p.read_bytes()).hexdigest() +def module(n,p): + s=importlib.util.spec_from_file_location(n,p);m=importlib.util.module_from_spec(s);s.loader.exec_module(m);return m +def write(p,x):p.write_text(json.dumps(x,indent=2)+'\n',encoding='utf-8',newline='\n') +def inventory(): + pins=read(P/'MANIFEST.json');actual={f.relative_to(P).as_posix() for f in P.rglob('*') if f.is_file() and f.name!='MANIFEST.json'} + need(actual==set(pins),'exact source inventory') + for n,h in pins.items():need(sha(P/n)==h,'source sha256 '+n) +def ancestors(): + pins=read(P/'vendor/pr1148/SOURCE-PINS.json') + for name,suffix in { + 'local/data/PARENT-ROUTING.json.gz':'base/split-centres/CANONICAL-WORD.json.gz', + 'inputs/DATA-PHASES.json':'complex-nine-native/DATA-PHASES.json', + 'inputs/ROUND20-PARENT-TEMPLATE.json.gz':'vendor535/inputs/ROUND20-PARENT-TEMPLATE.json.gz', + 'inputs/PRIOR-ALLOWANCE.json':'vendor531/evidence/audit/PREFIX-AND-INVOICE.json', + 'vendor/engines/moment.py':'/moment.py','vendor/engines/base_two_moment.py':'/base_two_moment.py','vendor/engines/outer.py':'/outer.py'}.items(): + hs={h for n,h in pins.items() if n.endswith(suffix)};need(len(hs)==1 and sha(P/name) in hs,'upstream source pin '+name) + claim=read(P/'vendor/pr1148/CLAIM.json');need(Q(claim['kappa'])==Q('0.001675121647789207'),'frozen PR1148 comparison') + +def main(): + need(__debug__,'normal Python required; -O disables vendor checks') + a=argparse.ArgumentParser();a.add_argument('--out',type=Path,required=True);z=a.parse_args();out=z.out.resolve() + need(out!=P and P not in out.parents,'output must be outside the package');need(not out.exists(),'fresh output directory required') + start=time.monotonic();inventory();ancestors();out.mkdir(parents=True) + rows=read(P/'vendor/pr1148/OWNERS.json.gz');edits=read(P/'data/EDITS-FROM-PR1148.json');seen=set();need(len(edits)==1409,'complete literal difference') + for e in edits: + i=e['index'];need(type(i)is int and 0<=i1 and j[0]>1,'two bit moment brackets');bitchecks.append(dict(point=b,accepted=accept,mercator=i,base_two=j)) + H={int(r):n for r,n in audit['profile'].items()};result=pricing.price(H,bit,M,B,A);conservative=pricing.price(H,bit,M,B,A,True) + base=pricing.price({int(r):n for r,n in read(P/'vendor/pr1148/CLAIM.json')['global_profile'].items()},bit,M,B,A) + need(base['kappa']==Q('0.001675121647789207'),'baseline outer compatibility') + need(result['kappa']==Q('0.001675224519162937') and conservative['kappa']==Q('0.001675224516317980'),'exact claimed endpoints');need(result['kappa']>base['kappa'],'strict improvement') + result.update(status='PASS_CROSSCALL_KERNEL_DEMOTION',conservative=conservative,baseline=base['kappa'],gain=result['kappa']-base['kappa'],profile=H,extra_groups=89,bit_moment_checks=bitchecks,local_checks=local,seconds=time.monotonic()-start,source_manifest_sha256=sha(P/'MANIFEST.json'),owner_audit='OWNER-AUDIT.json',finite_invoice='FINITE-INVOICE.json',scope='Finite conditional certificate: fresh changed local programs/phases, full new owner geometry and dispatch, complete profile, invoice and exact outer assembly. Unchanged baseline local and bit circuits, compiler/all-size, hosting/labels, precision/recovery and analytic interfaces remain inherited. No new Lean certificate or unconditional theorem.') + write(out/'RESULT.json',pricing.encode(result));print('PASS_CROSSCALL_KERNEL_DEMOTION kappa='+result['kappa_decimal'],flush=True) +if __name__=='__main__':main()