diff --git a/research/programmable-native-stage/.gitattributes b/research/programmable-native-stage/.gitattributes new file mode 100644 index 0000000000..fa1385d99a --- /dev/null +++ b/research/programmable-native-stage/.gitattributes @@ -0,0 +1 @@ +* -text diff --git a/research/programmable-native-stage/LICENSE b/research/programmable-native-stage/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/programmable-native-stage/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/programmable-native-stage/MANIFEST.json b/research/programmable-native-stage/MANIFEST.json new file mode 100644 index 0000000000..0e6356347a --- /dev/null +++ b/research/programmable-native-stage/MANIFEST.json @@ -0,0 +1,185 @@ +{ + "schema_version": 1, + "files": [ + { + "path": ".gitattributes", + "size": 8, + "sha256": "705fd4d6451a31d36b3df7de96f83f30ac976c9b4a6d1e51671d8e2f33e2d0da" + }, + { + "path": "fusion/FILES.json", + "size": 1779, + "sha256": "2a532ba8565ca2297825b34d6d897baaf4bbe41f81c7ea809d4c461a92174e34" + }, + { + "path": "fusion/inputs/B-MODULE.json", + "size": 968, + "sha256": "03c230cdafc555b557768c7bb4731f31cab5a16457dee89d8005387a67d07168" + }, + { + "path": "fusion/inputs/B-PROGRAM.json.gz", + "size": 910130, + "sha256": "fd30f46e210e4f46302fbeb4055a0e61aa5dce1268a864b53db58406be5a2ed9" + }, + { + "path": "fusion/inputs/BACKWARD-PROOF.md", + "size": 4127, + "sha256": "04ab96921464d5a50a7a6b57b212d8fffe57d3e5f230a66e70782a2510c7f6fb" + }, + { + "path": "fusion/inputs/K-MODULE.json", + "size": 2934, + "sha256": "02cec9cb8ce148c9a2ee97a899338b330b4b3efd1455b4243466987e09b354a0" + }, + { + "path": "fusion/inputs/K-PROGRAM.json.gz", + "size": 1414847, + "sha256": "dd9d0ecae4aebbef05c8134f1772221c97d2bf818e7a2f464501dbfa9c2856c0" + }, + { + "path": "fusion/inputs/PROOF.md", + "size": 14853, + "sha256": "99e5b12bc5f5e67e5c1e49394dbb88746da46ae3d8760598c8b435b9d0baec9c" + }, + { + "path": "fusion/LICENSE", + "size": 11357, + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "path": "fusion/PROOF.txt", + "size": 8778, + "sha256": "46b0d46f9e490ed864ebdf2cda18468aa0cec286c3198913d43df4d703a02b89" + }, + { + "path": "fusion/RESULT.json", + "size": 4326, + "sha256": "0b294617673a03603591387432279135f6e67dd51596843c8be1e87c401c0776" + }, + { + "path": "fusion/SOURCES.json", + "size": 2339, + "sha256": "75d8a6108b6940531dd6e5f4b14b1cc8f859fb74c2c457156ddbf70e983be9c2" + }, + { + "path": "fusion/verify.py", + "size": 6944, + "sha256": "59782c6df370ade16d0cfa080f1e7828381475db7b5410f3df7870fea1e7ac16" + }, + { + "path": "LICENSE", + "size": 11357, + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "path": "native/INTERTWINER-PROOF.txt", + "size": 6172, + "sha256": "14e85d43b61e959d92ff58c285c193b1619c6f4fbdbe50c2eaf10a065134a2c8" + }, + { + "path": "native/programmable_stage.py", + "size": 4374, + "sha256": "9d434dd2e7388be7f83b54819382c0634eccda7bb057e9973eea9edfea0ad0bd" + }, + { + "path": "native/RESULT.json", + "size": 899, + "sha256": "cc01f04a03ff3500b5fc953ffbf11a689cbf70f110b0769ef6aeb56539e43f69" + }, + { + "path": "native/SOURCE-PINS.json", + "size": 846, + "sha256": "eb8d5f23db43798752bba985b08c643a292eea4b7aa9868495688df691288633" + }, + { + "path": "native/vendor/BACKWARD-PROOF.md", + "size": 4127, + "sha256": "04ab96921464d5a50a7a6b57b212d8fffe57d3e5f230a66e70782a2510c7f6fb" + }, + { + "path": "native/vendor/K-MODULE.json", + "size": 2934, + "sha256": "02cec9cb8ce148c9a2ee97a899338b330b4b3efd1455b4243466987e09b354a0" + }, + { + "path": "native/vendor/K-PROGRAM.json.gz", + "size": 1414847, + "sha256": "dd9d0ecae4aebbef05c8134f1772221c97d2bf818e7a2f464501dbfa9c2856c0" + }, + { + "path": "native/vendor/PROOF.md", + "size": 14853, + "sha256": "99e5b12bc5f5e67e5c1e49394dbb88746da46ae3d8760598c8b435b9d0baec9c" + }, + { + "path": "native/verify_intertwiners.py", + "size": 3280, + "sha256": "f2119319355d8f07c6f09dea6792764ccba74baf0de289f103155734fd626c54" + }, + { + "path": "NOTICE.txt", + "size": 383, + "sha256": "b40487b6da5609f2e7dd5c0bab5f0b5bf7afd95a623c41a61c2bfe74d7449177" + }, + { + "path": "precision/COMPOSITION.txt", + "size": 3660, + "sha256": "bad574590518043e3fa293f319889bec7b256460c01fff3016689556fa9d7f39" + }, + { + "path": "precision/PROOF.txt", + "size": 8753, + "sha256": "a07e7d22800eafcdcc91aa78e1eb508fb5eccc7d306c9b981707108822e9300e" + }, + { + "path": "precision/RESULT.json", + "size": 3764, + "sha256": "7de09bcb78ef09f059a5ba4e24ae42e03d46abe45b508420196b71a0b39a383b" + }, + { + "path": "precision/source/B-PROGRAM.json.gz", + "size": 910130, + "sha256": "fd30f46e210e4f46302fbeb4055a0e61aa5dce1268a864b53db58406be5a2ed9" + }, + { + "path": "precision/source/K-PROGRAM.json.gz", + "size": 1414847, + "sha256": "dd9d0ecae4aebbef05c8134f1772221c97d2bf818e7a2f464501dbfa9c2856c0" + }, + { + "path": "precision/SOURCES.json", + "size": 1161, + "sha256": "7b8f9946b7cd5692476bb701e088109cc6e77fee38961fcff98b7883ccfe9f16" + }, + { + "path": "precision/verify.py", + "size": 7774, + "sha256": "c7f99fe2258e7edffbac8a644229676ce3acb3bf43ea2d01e91ce9321c41185c" + }, + { + "path": "README.md", + "size": 4549, + "sha256": "f02370bfbb6a313bca00eb5ce3fee51088e12f0e21dac30a0ec7a6c88be5ad57" + }, + { + "path": "SOURCES.json", + "size": 922, + "sha256": "176e14ff3be208b6cb6ee14c95fcea34a3d9535c73c5c93780b81d98faee0c80" + }, + { + "path": "TASK.json", + "size": 5391, + "sha256": "24ad06dff69e49fd5faecab9df99539b86241b8b81a73eb636a14fb2aae0e252" + }, + { + "path": "VERIFY.json", + "size": 3038, + "sha256": "3c4c96f7b341ac4df2dba6bb2aefb02e5d3e0eb2d98bc087b5d7242e5548e3e8" + }, + { + "path": "verify.py", + "size": 1698, + "sha256": "013462e5fa1cb199d11268ca28741b57a3a976922003f8721cbe536f70caa75b" + } + ] +} diff --git a/research/programmable-native-stage/NOTICE.txt b/research/programmable-native-stage/NOTICE.txt new file mode 100644 index 0000000000..093c4f823c --- /dev/null +++ b/research/programmable-native-stage/NOTICE.txt @@ -0,0 +1,2 @@ +Original additions: Dugongue with substantial OpenAI Codex assistance, one coordinator and three agents; Apache-2.0. +Retained source, geometry, phase, helper and compiler credit is listed in README.md and component proofs/source manifests. No source-specific attribution has been removed. Public content hashes authenticate bytes; no original local path is hashed into this package. diff --git a/research/programmable-native-stage/README.md b/research/programmable-native-stage/README.md new file mode 100644 index 0000000000..b62df85f16 --- /dev/null +++ b/research/programmable-native-stage/README.md @@ -0,0 +1,36 @@ +# Programmable native stages, coded-thin fusion and exact dyadic precision + +This package closes three constructive interfaces from the preceding Word RAM/native work. **It does not establish a superior κ or a complete multiplication caller.** The terminal all-width central-Q gauge remains unresolved, and no ideal invoice is presented as an admitted bound. + +1. [Programmable native stage](native/INTERTWINER-PROOF.txt): an actual event emitter changes the same-frame cross-parity transfer to any rational amplitude while preserving the Gaussian paths and all 1,024 independent input columns. Five amplitudes, including zero, are checked; output files refuse overwrite. +2. [Coded-thin fusion](fusion/PROOF.txt): an additional actual C Q⁻¹ transfer is absorbed into existing native ADD coefficients, with no additional Gaussian child, field or phase path. Both orientations and ten cases are checked. This is not an uncoded I Q⁻¹ request. +3. [Exact precision](precision/PROOF.txt): the actual dyadic forward/backward streams admit fractional storage B = g + ⌈25f/2⌉ + 4, with explicit magnitude and signed-payload bounds. [Composition](precision/COMPOSITION.txt) gives constructive exact-grid propagation for a completely emitted dyadic caller. Arbitrary rational amplitudes require their own rational/rounding implementation; the dyadic theorem does not cover non-dyadic denominators for free. + +## Reproduce + +Python 3.12+, standard library only, without Git, network, Lean or installed native libraries: + +```sh +python -I -B research/programmable-native-stage/verify.py +python -I -O -B research/programmable-native-stage/verify.py +``` + +The launcher authenticates all package bytes and gives each scientific child a fresh non-writing bytecode namespace. Normal and optimized runs check the constructive programs, exact noncommuting matrix identities, all-column frame/invoice replays and precision mutation controls. Native monomial/phase correctness is inherited from the pinned #5464 proof; no independent Lean kernel audit, full caller runtime or new κ is claimed. + +## Exact economic boundary + +Each 512-port local module retains paid profile {8:512, 9:512, 15:512, 16:512}, no helper target bank and no new owned field. Nonzero amplitude uses 38,912 actual scalar ADDs; amplitude zero deletes them. Scaling is paid ordinary work, not a zero-cost arithmetic oracle. + +Ordinary pre/post codes give a paired letter Lᵢ = diag(CᵢDᵢ,DᵢCᵢ), satisfying AᵢQ = QBᵢ. This lets Lᵢ commute with the standard thin shears. However the ordinary closing swap of the one-stage controller produces diag(BᵢQ⁻¹,AᵢQ). The second branch decodes by an ordinary code; the first generally does not. This final placement issue is not removed by a proof-only conjugation or by the one-column expansion of Q. Independent worker checks agree. We do not advertise the earlier ideal p19 arithmetic as a new bound. + +The previous counted kernel is now PR #5466 and its source-bound recoding/decoder interfaces are PR #5467. This contribution adds the actual programmable/fused native interface and all-width exact precision, rather than republishing those packages. #5468's numerical headroom is acknowledged as unchanged-profile work; the selected record remains untouched. Source pins are in component manifests and root SOURCES.json. + +## Open next questions + +1. Build a global caller whose terminal central factors have the correct side, retaining every independent target. First test its exact operator on genuinely noncommuting codes; the existing closing swap fails this requirement. +2. Use the coded-thin fusion to remove a named existing request, with a complete changed paid and target profile. Common-frame C-coded service does not imply uncoded same-port service. +3. Emit that complete caller before applying the precision composition theorem. Then charge actual limb arithmetic, monomial movement, scratch and outer compiler/analytic costs. Exact dyadic storage is not unit-cost arbitrary precision. + +## Attribution + +Credit THU New Media Research Center and #5464 for the actual whole-K programs and inherited all-width phase proofs; Ali Romman #5439 for odd-E8 geometry; Dugongue #4929, #5466 and #5467; Dillon Amburgey, Cao Yifan, Cinna Davis, zxv, Jacob Alan Sussman, Chris R/Clear1nsight, Matarener and the retained native/Clifford/compiler/analytic lineage. Source-specific notices remain unchanged. Original additions prepared for Dugongue with substantial OpenAI Codex assistance by one coordinator and three agents; Apache-2.0. diff --git a/research/programmable-native-stage/SOURCES.json b/research/programmable-native-stage/SOURCES.json new file mode 100644 index 0000000000..5605186fae --- /dev/null +++ b/research/programmable-native-stage/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + } + ], + "frozen_component_sources": [ + "native/SOURCE-PINS.json", + "fusion/SOURCES.json", + "precision/SOURCES.json" + ], + "source_export_contract": "Component-local vendor content is frozen and byte-authenticated by MANIFEST.json and component verifiers. External PR sources are provenance links, not live unpinned checkout inputs." +} diff --git a/research/programmable-native-stage/TASK.json b/research/programmable-native-stage/TASK.json new file mode 100644 index 0000000000..72949f844a --- /dev/null +++ b/research/programmable-native-stage/TASK.json @@ -0,0 +1,77 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "changed", + "scope_change_reason": "The donor assigned closure of the preceding native/Word RAM deliverable. These new sufficient interfaces were established, but the global central-Q placement remains unproved.", + "actual_scope": "Construct programmable actual native stages, coded-thin fusion and sufficient all-width exact dyadic precision; no full caller or improved kappa is established.", + "bottleneck_link": "Actual programmed native endpoints and exact grids are available; the complete caller still needs a correct terminal central-Q placement and complete tariffs.", + "stop_rule": "Stop at the donor requested handoff; do not relabel ideal funding as an admitted multiplication bound.", + "evidence": "Component normal/optimized replays, 1,024 independent columns, ten fusion cases, noncommuting identities and exact parity-dependent precision bounds.", + "author": "Dugongue", + "ai_assistance": "Substantial OpenAI Codex assistance by one coordinator and three agents.", + "outcome": "partial", + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "new_kappa_claimed": false, + "open_questions": [ + { + "question": "Close the global central-Q placement.", + "why_it_matters": "Both independent output banks must be productive before claiming kappa.", + "first_step": "Test an exact closing word on genuinely noncommuting codes.", + "blocked_by": "The current ordinary swap leaves a wrong-side-Q branch." + }, + { + "question": "Remove a real paid query using coded-thin fusion.", + "why_it_matters": "Changing ordinary ADD coefficients alone leaves the recursion invoice unchanged.", + "first_step": "Name a compatible caller request and compare every paid/target entry.", + "blocked_by": "C-coded service does not equal same-port uncoded service." + }, + { + "question": "Apply precision composition to a complete emitted caller.", + "why_it_matters": "A local exact grid does not price a global algorithm.", + "first_step": "Emit all events then propagate dyadic exponents and limb/owned-memory costs.", + "blocked_by": "No full correct caller is emitted here." + } + ] +} diff --git a/research/programmable-native-stage/VERIFY.json b/research/programmable-native-stage/VERIFY.json new file mode 100644 index 0000000000..3c762c87d4 --- /dev/null +++ b/research/programmable-native-stage/VERIFY.json @@ -0,0 +1,69 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "checks": "Source hashes, literal programmable stage, all-column coded-thin fusion and exact dyadic precision; no new kappa.", + "timeout_seconds": 300 + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "checks": "Independent optimized replay of all four scientific checks.", + "timeout_seconds": 300 + } + ], + "package_local_inputs": [ + "research/programmable-native-stage/.gitattributes", + "research/programmable-native-stage/LICENSE", + "research/programmable-native-stage/MANIFEST.json", + "research/programmable-native-stage/NOTICE.txt", + "research/programmable-native-stage/README.md", + "research/programmable-native-stage/SOURCES.json", + "research/programmable-native-stage/TASK.json", + "research/programmable-native-stage/VERIFY.json", + "research/programmable-native-stage/fusion/FILES.json", + "research/programmable-native-stage/fusion/LICENSE", + "research/programmable-native-stage/fusion/PROOF.txt", + "research/programmable-native-stage/fusion/RESULT.json", + "research/programmable-native-stage/fusion/SOURCES.json", + "research/programmable-native-stage/fusion/inputs/B-MODULE.json", + "research/programmable-native-stage/fusion/inputs/B-PROGRAM.json.gz", + "research/programmable-native-stage/fusion/inputs/BACKWARD-PROOF.md", + "research/programmable-native-stage/fusion/inputs/K-MODULE.json", + "research/programmable-native-stage/fusion/inputs/K-PROGRAM.json.gz", + "research/programmable-native-stage/fusion/inputs/PROOF.md", + "research/programmable-native-stage/fusion/verify.py", + "research/programmable-native-stage/native/INTERTWINER-PROOF.txt", + "research/programmable-native-stage/native/RESULT.json", + "research/programmable-native-stage/native/SOURCE-PINS.json", + "research/programmable-native-stage/native/programmable_stage.py", + "research/programmable-native-stage/native/vendor/BACKWARD-PROOF.md", + "research/programmable-native-stage/native/vendor/K-MODULE.json", + "research/programmable-native-stage/native/vendor/K-PROGRAM.json.gz", + "research/programmable-native-stage/native/vendor/PROOF.md", + "research/programmable-native-stage/native/verify_intertwiners.py", + "research/programmable-native-stage/precision/COMPOSITION.txt", + "research/programmable-native-stage/precision/PROOF.txt", + "research/programmable-native-stage/precision/RESULT.json", + "research/programmable-native-stage/precision/SOURCES.json", + "research/programmable-native-stage/precision/source/B-PROGRAM.json.gz", + "research/programmable-native-stage/precision/source/K-PROGRAM.json.gz", + "research/programmable-native-stage/precision/verify.py", + "research/programmable-native-stage/verify.py" + ] +} diff --git a/research/programmable-native-stage/fusion/FILES.json b/research/programmable-native-stage/fusion/FILES.json new file mode 100644 index 0000000000..2d6b2f446d --- /dev/null +++ b/research/programmable-native-stage/fusion/FILES.json @@ -0,0 +1,60 @@ +{ + "files": [ + { + "path": "LICENSE", + "size": 11357, + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "path": "PROOF.txt", + "size": 8778, + "sha256": "46b0d46f9e490ed864ebdf2cda18468aa0cec286c3198913d43df4d703a02b89" + }, + { + "path": "RESULT.json", + "size": 4326, + "sha256": "0b294617673a03603591387432279135f6e67dd51596843c8be1e87c401c0776" + }, + { + "path": "SOURCES.json", + "size": 2339, + "sha256": "75d8a6108b6940531dd6e5f4b14b1cc8f859fb74c2c457156ddbf70e983be9c2" + }, + { + "path": "verify.py", + "size": 6944, + "sha256": "59782c6df370ade16d0cfa080f1e7828381475db7b5410f3df7870fea1e7ac16" + }, + { + "path": "inputs/B-MODULE.json", + "size": 968, + "sha256": "03c230cdafc555b557768c7bb4731f31cab5a16457dee89d8005387a67d07168" + }, + { + "path": "inputs/B-PROGRAM.json.gz", + "size": 910130, + "sha256": "fd30f46e210e4f46302fbeb4055a0e61aa5dce1268a864b53db58406be5a2ed9" + }, + { + "path": "inputs/BACKWARD-PROOF.md", + "size": 4127, + "sha256": "04ab96921464d5a50a7a6b57b212d8fffe57d3e5f230a66e70782a2510c7f6fb" + }, + { + "path": "inputs/K-MODULE.json", + "size": 2934, + "sha256": "02cec9cb8ce148c9a2ee97a899338b330b4b3efd1455b4243466987e09b354a0" + }, + { + "path": "inputs/K-PROGRAM.json.gz", + "size": 1414847, + "sha256": "dd9d0ecae4aebbef05c8134f1772221c97d2bf818e7a2f464501dbfa9c2856c0" + }, + { + "path": "inputs/PROOF.md", + "size": 14853, + "sha256": "99e5b12bc5f5e67e5c1e49394dbb88746da46ae3d8760598c8b435b9d0baec9c" + } + ], + "hash_semantics": "Content SHA-256 only" +} diff --git a/research/programmable-native-stage/fusion/LICENSE b/research/programmable-native-stage/fusion/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/programmable-native-stage/fusion/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/programmable-native-stage/fusion/PROOF.txt b/research/programmable-native-stage/fusion/PROOF.txt new file mode 100644 index 0000000000..327159b30f --- /dev/null +++ b/research/programmable-native-stage/fusion/PROOF.txt @@ -0,0 +1,144 @@ +Literal absorption of coded thin queries in the whole odd-E8 K primitive + +Result +For every fixed dyadic lambda, the pinned whole-K native program has a literal +coefficient variant with exact normalized physical endpoint + F_lambda = diag(D,D) L((1+lambda) C Q^-1) + = F_0 L(lambda C Q^-1). +Its pinned backward companion similarly has endpoint + B_lambda = diag(D,D) U(-(1+lambda) Q C) + = B_0 U(-lambda Q C). +Here C is the actual odd-E8 K owner recoding and C^2=I; [C,Q]=0 is not assumed. +Only existing scalar ADD coefficients change. No paid child, monomial map, owned +field, input, output or phase path is added. For lambda=-1 all scalar ADDs are +omitted and the endpoint is diag(D,D). For lambda=1 one additional actual coded +thin preconditioner is absorbed without another Gaussian call. This is a local +sufficient compiler identity, not a complete multiplication bound or new kappa. + +Actual source +The source is PR 5464 head 3981f9539e63630681f6903e3c6a50b3a0d2f2dd, +research/odd-e8-whole-k-native. SOURCES.json pins six retained files by exact +content hashes; scientific gzip payload hashes are separately recorded. The +phase-complete emitted root cube has 512 ports and 1,024 independent main inputs. +Its complete native construction uses two opposite selector-parity classes. +Each class spans a degenerate nine-space with rank-one restricted pairing and +radical dimension eight; the two classes are orthogonal and meet in that radical. +All original physical inputs x_p,y_p are arbitrary independent ground fields. +No helper or owned temporary is supplied or assumed free. + +Let L_p be the pinned ordinary real normalizer, Q the central one-axis Gaussian, +D the product of the other 24 Gaussian axes. Its geometric coordinates are + u_p=L_p Q^-1 x_p, v_p=L_p y_p. +The source entrance Phi_[q_p] L_p Q^-1 is an emitted ordinary monomial despite +the virtual Q^-1 in the coordinate definition. Thus no incoming Gaussian service +is assumed. The original source's common-window scalar matrix is the actual +K_odd=(K1+K2+K3-K1 K2 K3)/2, where each K_i is an involution and the three owner +factors commute. It is symmetric, squares to I and has exactly 76 entries per +row: 12 entries of magnitude 1/4 and 64 entries of magnitude 1/16. Every nonzero +K_odd[r,s] joins opposite selector parities. + +Exact frame and chronology proof +For a source parity epsilon, all X_s of that parity ascend from their own line +to the same literal Phi_S(epsilon) by an H8 path. Opposite-parity Y_r ascend from +ground to that identical Phi_S(epsilon) by an H9 path. The program executes every +such source and reader path before its cut ADDs, then executes + Y_r += K_odd[r,s] X_s +for every nonzero coefficient. Sources are never overwritten. Every reader +retains its arbitrary old value with coefficient one. Only after all these ADDs +do source H16 and reader H15 exit paths run. The two parity windows use disjoint +source/reader role sets and therefore do not invalidate each other's data. + +Replace every displayed coefficient by (1+lambda) K_odd[r,s]. The exact same +literal source/reader frames still match; all 1,024 independent geometric input +columns give + u'_s=u_s, + v'_r=v_r+(1+lambda) sum_s K_odd[r,s] u_s. +All paths, normalizers and absolute phase opcodes are retained literally. Their +pinned physical identities yield the normalized endpoint claimed above with +C_rs=K_odd[r,s] L_r^-1 L_s. This is genuine delayed execution of a coded input +preconditioner through a Gaussian window, rather than an unexplained frame tag. +For lambda=-1 the zero-coefficient ADDs are deleted as actual instructions. + +The inverse-transpose companion is emitted in the same chronological order from +the source. Each real scalar ADD swaps source/target and negates its coefficient; +every monomial and positive Gaussian child has the pinned literal inverse- +transpose conversion and fixed boundary maps. Since a two-bank shear has square- +zero off-diagonal block, inverse transpose is linear in the scalar multiplier. +Thus scaling its existing ADDs by the same 1+lambda gives the stated B_lambda, +with no commutation of C through Q. Its concrete actual chart names have the +pinned conjugate prefix, and its ADDs still join exactly matching charts. + +Distinction from an uncoded query +For the same external port p, X_p and Y_p enter opposite S9 windows. Their chart +transport has Gaussian rank two, as the pinned source checks; it is not an +ordinary same-frame ADD. Consequently this construction does not absorb an +uncoded y_p+=Q^-1 x_p service. It absorbs the actual C Q^-1 code because every +nonzero coefficient joins the opposite ports that truly meet in one window. +No same-rank or equal-dimension retag is used. + +Reciprocal code identity +Define b=C Q^-1 and a=Q C. C^2=I gives a b=b a=I by adjacent cancellation, +without commuting C and Q. Thus abstract thin shears have the exact relation + L(b) U(-a) L(b) = [[0,-a],[b,0]], +whose square is -I. For two stages i,j the ordered ratios + b_j b_i^-1=C_j C_i, + a_j^-1 a_i=C_j C_i +are ordinary owner recodings. These are sufficient algebraic interfaces for a +future actual coded controller. They do not prove that different stages' codes +commute, that a global controller closes, or that all target gauges unload. +Native F_lambda and B_lambda also perform their D diagonal actions; they must +not be substituted for free thin shears in a word that ignores those actions. + +Complete local operation counts +For the emitted root cube, every variant keeps exactly + 512 H8 + 512 H9 + 512 H15 + 512 H16 +paid children. Forward ordinary monomials remain exactly + 7,680 P + 7,680 D + 3,072 X + 3,072 phase. +Backward ordinary monomials remain exactly + 7,680 P + 7,680 D + 6,656 X + 3,072 phase. +If 1+lambda is nonzero, there are 38,912 scalar ADDs. If it is zero, there are +zero scalar ADDs. There are no helpers, new independent inputs, owned fields, +COPYs or CLEARs in any variant. Coefficients remain fixed dyadic constants; +actual precision and machine-level scalar implementation must still be paid. +For lambda=1 their magnitudes double and denominator exponents decrease by one; +this is not a hidden additional arbitrary-precision division. The per-reader +component-l1 scalar prefix bound is at most 1+7|1+lambda|. All physical maps and +Gaussian children are unitary; complete global rounding propagation remains an +outer caller obligation. No recursive paid histogram is improved by this local +identity alone. + +All-width scope and evidence +The proof uses only linearity at actual common frames, fixed scalar coefficients +and composition of the retained lifted unary operators. At width f, every scalar +coefficient is applied once and each one-copy scalar phase is lifted as i^(f theta). +The proof never tensors an owner matrix sum or expands Q_f into a constant number +of monomials. Its all-width physical scope is inherited from the pinned generic +phase/frame proof, not inferred from the finite checks below. + +Run python3 -B verify.py using Python 3.12+ and the standard library. It checks +all source hashes, all 262,144 entries of the scalar K square over exact integers, +and actual frame/cost/1,024-column replays in both orientations at lambda values +0,1,-1,-2,1/2. Wrong scalar coefficients and wrong physical charts are rejected. +The transformed non-ADD event lists agree literally with the original native +paths, so no phase or child change is hidden. RESULT.json records all ten cases. +This does not rerun every Clifford phase proof, all 2,744 cube instances, a native +machine compiler or any Lean kernel. The source construction and full generic +family proof remain explicit pinned inputs. For the whole family the same +constructor-level coefficient replacement applies to every disjoint cube. + +Credit +Retain PR 5464's THU New Media Research Center contributor attribution, Ali +Romman's PR 5439 odd-E8 geometry, Dugongue/PR 4929, Dillon Amburgey's real +normalizers, Cao Yifan's P112 native lineage, Cinna Davis, zxv, Jacob Alan Sussman, +and the retained native, Clifford, compiler and analytic predecessors. The source +proofs and source-specific notices are included. Ordinary linearity, reciprocal +shear and transvection identities are classical. This source-bound coefficient +compiler, exact modified-column/frame replay and explicit interface accounting +were prepared for Dugongue with substantial OpenAI Codex assistance. Apache-2.0. + +Open next question +Construct a complete chronological controller using these reciprocal coded thin +interfaces and every native D action, with actual ordinary bridges and initial/ +final gauges. Then recompute its independent Gaussian targets, paid moment, +ordinary precision/movement tariff, compiler and outer recovery. No such full +profitable closure or new kappa is established by this package. diff --git a/research/programmable-native-stage/fusion/RESULT.json b/research/programmable-native-stage/fusion/RESULT.json new file mode 100644 index 0000000000..98155beaa0 --- /dev/null +++ b/research/programmable-native-stage/fusion/RESULT.json @@ -0,0 +1,201 @@ +{ + "status": "PASS_LITERAL_CODED_THIN_FUSION", + "new_kappa": false, + "input_columns": 1024, + "exact_K_square_entries": 262144, + "cases": [ + { + "direction": "forward", + "extra_coded_thin": "0", + "total_transfer_multiplier": "1", + "literal_events": 43008, + "paid": { + "8": 512, + "9": 512, + "15": 512, + "16": 512 + }, + "ordinary": { + "ADD": 38912, + "D": 7680, + "P": 7680, + "X": 3072, + "phase": 3072 + } + }, + { + "direction": "backward", + "extra_coded_thin": "0", + "total_transfer_multiplier": "1", + "literal_events": 44544, + "paid": { + "8": 512, + "9": 512, + "15": 512, + "16": 512 + }, + "ordinary": { + "ADD": 38912, + "D": 7680, + "P": 7680, + "X": 6656, + "phase": 3072 + } + }, + { + "direction": "forward", + "extra_coded_thin": "1", + "total_transfer_multiplier": "2", + "literal_events": 43008, + "paid": { + "8": 512, + "9": 512, + "15": 512, + "16": 512 + }, + "ordinary": { + "ADD": 38912, + "D": 7680, + "P": 7680, + "X": 3072, + "phase": 3072 + } + }, + { + "direction": "backward", + "extra_coded_thin": "1", + "total_transfer_multiplier": "2", + "literal_events": 44544, + "paid": { + "8": 512, + "9": 512, + "15": 512, + "16": 512 + }, + "ordinary": { + "ADD": 38912, + "D": 7680, + "P": 7680, + "X": 6656, + "phase": 3072 + } + }, + { + "direction": "forward", + "extra_coded_thin": "-1", + "total_transfer_multiplier": "0", + "literal_events": 4096, + "paid": { + "8": 512, + "9": 512, + "15": 512, + "16": 512 + }, + "ordinary": { + "D": 7680, + "P": 7680, + "X": 3072, + "phase": 3072 + } + }, + { + "direction": "backward", + "extra_coded_thin": "-1", + "total_transfer_multiplier": "0", + "literal_events": 5632, + "paid": { + "8": 512, + "9": 512, + "15": 512, + "16": 512 + }, + "ordinary": { + "D": 7680, + "P": 7680, + "X": 6656, + "phase": 3072 + } + }, + { + "direction": "forward", + "extra_coded_thin": "-2", + "total_transfer_multiplier": "-1", + "literal_events": 43008, + "paid": { + "8": 512, + "9": 512, + "15": 512, + "16": 512 + }, + "ordinary": { + "ADD": 38912, + "D": 7680, + "P": 7680, + "X": 3072, + "phase": 3072 + } + }, + { + "direction": "backward", + "extra_coded_thin": "-2", + "total_transfer_multiplier": "-1", + "literal_events": 44544, + "paid": { + "8": 512, + "9": 512, + "15": 512, + "16": 512 + }, + "ordinary": { + "ADD": 38912, + "D": 7680, + "P": 7680, + "X": 6656, + "phase": 3072 + } + }, + { + "direction": "forward", + "extra_coded_thin": "1/2", + "total_transfer_multiplier": "3/2", + "literal_events": 43008, + "paid": { + "8": 512, + "9": 512, + "15": 512, + "16": 512 + }, + "ordinary": { + "ADD": 38912, + "D": 7680, + "P": 7680, + "X": 3072, + "phase": 3072 + } + }, + { + "direction": "backward", + "extra_coded_thin": "1/2", + "total_transfer_multiplier": "3/2", + "literal_events": 44544, + "paid": { + "8": 512, + "9": 512, + "15": 512, + "16": 512 + }, + "ordinary": { + "ADD": 38912, + "D": 7680, + "P": 7680, + "X": 6656, + "phase": 3072 + } + } + ], + "rejected_controls": [ + "wrong_cut_coefficient", + "wrong_physical_chart" + ], + "scope": "Exact all-column scalar/frame replay; all original monomial/paid/phase paths retained literally. Native physical correctness and all-width phase proof inherited from pinned upstream." +} diff --git a/research/programmable-native-stage/fusion/SOURCES.json b/research/programmable-native-stage/fusion/SOURCES.json new file mode 100644 index 0000000000..8549b69058 --- /dev/null +++ b/research/programmable-native-stage/fusion/SOURCES.json @@ -0,0 +1,55 @@ +{ + "sources": [ + { + "file": "K-PROGRAM.json.gz", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "3981f9539e63630681f6903e3c6a50b3a0d2f2dd", + "upstream_path": "research/odd-e8-whole-k-native/K-PROGRAM.json.gz", + "sha256": "dd9d0ecae4aebbef05c8134f1772221c97d2bf818e7a2f464501dbfa9c2856c0", + "bytes": 1414847, + "payload_sha256": "98941b295d428462b82dae52a369de97dcbf5be1dd7a369f6c495cda5fc6ac8a" + }, + { + "file": "B-PROGRAM.json.gz", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "3981f9539e63630681f6903e3c6a50b3a0d2f2dd", + "upstream_path": "research/odd-e8-whole-k-native/B-PROGRAM.json.gz", + "sha256": "fd30f46e210e4f46302fbeb4055a0e61aa5dce1268a864b53db58406be5a2ed9", + "bytes": 910130, + "payload_sha256": "f6b26f28f2a8f2dcfbf81f98c7ca18f967384b7b61518766494f8e821d5bf56f" + }, + { + "file": "K-MODULE.json", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "3981f9539e63630681f6903e3c6a50b3a0d2f2dd", + "upstream_path": "research/odd-e8-whole-k-native/K-MODULE.json", + "sha256": "02cec9cb8ce148c9a2ee97a899338b330b4b3efd1455b4243466987e09b354a0", + "bytes": 2934 + }, + { + "file": "B-MODULE.json", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "3981f9539e63630681f6903e3c6a50b3a0d2f2dd", + "upstream_path": "research/odd-e8-whole-k-native/B-MODULE.json", + "sha256": "03c230cdafc555b557768c7bb4731f31cab5a16457dee89d8005387a67d07168", + "bytes": 968 + }, + { + "file": "PROOF.md", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "3981f9539e63630681f6903e3c6a50b3a0d2f2dd", + "upstream_path": "research/odd-e8-whole-k-native/PROOF.md", + "sha256": "99e5b12bc5f5e67e5c1e49394dbb88746da46ae3d8760598c8b435b9d0baec9c", + "bytes": 14853 + }, + { + "file": "BACKWARD-PROOF.md", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "3981f9539e63630681f6903e3c6a50b3a0d2f2dd", + "upstream_path": "research/odd-e8-whole-k-native/BACKWARD-PROOF.md", + "sha256": "04ab96921464d5a50a7a6b57b212d8fffe57d3e5f230a66e70782a2510c7f6fb", + "bytes": 4127 + } + ], + "evidence": "Pinned native word and source proofs; no new Lean audit" +} diff --git a/research/programmable-native-stage/fusion/inputs/B-MODULE.json b/research/programmable-native-stage/fusion/inputs/B-MODULE.json new file mode 100644 index 0000000000..6efe1d2975 --- /dev/null +++ b/research/programmable-native-stage/fusion/inputs/B-MODULE.json @@ -0,0 +1,30 @@ +{ + "CLEAR": 0, + "COPY": 0, + "actual_rank8_word_absolute_phase_checked": true, + "all_independent_scalar_columns": 1024, + "backward_scientific_payload_sha256": "f6b26f28f2a8f2dcfbf81f98c7ca18f967384b7b61518766494f8e821d5bf56f", + "distinct_conjugated_paid_paths": 1028, + "forward_scientific_payload_sha256": "98941b295d428462b82dae52a369de97dcbf5be1dd7a369f6c495cda5fc6ac8a", + "helpers": 0, + "new_kappa": false, + "normalized_endpoint": "B_K=diag(D,D) U(-Q C_K), without requiring [C_K,Q]=0", + "ordinary_literal_profile": { + "ADD": 38912, + "D": 7680, + "P": 7680, + "X": 6656, + "phase": 3072 + }, + "owned_fields": 0, + "paid_profile": { + "8": 512, + "9": 512, + "15": 512, + "16": 512 + }, + "schema": "odd-E8-whole-K-backward-native/v1", + "scope": "Literal backward native K companion, including ordinary boundaries. It does not supply H or close/admit an outer caller.", + "small_dense_child_inversion_cases": 26, + "status": "PASS" +} diff --git a/research/programmable-native-stage/fusion/inputs/B-PROGRAM.json.gz b/research/programmable-native-stage/fusion/inputs/B-PROGRAM.json.gz new file mode 100644 index 0000000000..6651986b9f Binary files /dev/null and b/research/programmable-native-stage/fusion/inputs/B-PROGRAM.json.gz differ diff --git a/research/programmable-native-stage/fusion/inputs/BACKWARD-PROOF.md b/research/programmable-native-stage/fusion/inputs/BACKWARD-PROOF.md new file mode 100644 index 0000000000..0777adf3d8 --- /dev/null +++ b/research/programmable-native-stage/fusion/inputs/BACKWARD-PROOF.md @@ -0,0 +1,77 @@ +# Literal backward native K + +Let `A=diag(D,D)` and `C=C_K`. The proved forward word is +`F=A L(C Q^-1)`. Since C is real symmetric and Q is symmetric, + +``` +F^-T = A^-1 U(-Q^-1 C). +``` + +Every emitted gate is invertible. There is no CLEAR, COPY, allocation or +owned zero field. If the chronological gates are `E_1,...,E_m`, the matrix +is `F=E_m ... E_1`, and `F^-T=E_m^-T ... E_1^-T`. Thus the same chronological +gate order, with each gate replaced by its inverse transpose, is exact. +This statement does not reverse chronological order. + +For a real scalar ADD `destination += c source`, inverse transpose is +`source += -c destination`. For an ordinary unitary monomial M, inverse +transpose is its complex conjugate. The literal P and X factors remain +unchanged; each D factor retains its quadratic coefficient 2 modulo 4 and +negates its Z4 linear coefficients; each scalar phase is negated modulo 4. +The entire chronological monomial factor order remains unchanged. + +Each paid child is a product of commuting positive coordinate Gaussians. +On one coordinate `C_plus^2=X` and `C_plus^4=I`, including their scalar +phases. Therefore `C_minus=C_plus X`. A rank-r inverse child is emitted +as the same positive rank-r child followed by the single ordinary X whose +mask is the sum of the r child coordinate vectors. This is a literal +phase identity on all address columns, not only an equality of tableaux. +`backward.py` checks it densely on all columns and all nonempty coordinate +subsets for dimensions 1 through 4, and checks the first physical rank-8 +path with fresh sparse Gaussian-integer arithmetic. Every translated +physical path also has its conjugated signed tableau and rank checked. +The all-dimensional result follows directly from the one-coordinate +identity and commuting tensor factors. + +Now put `J=diag(Q^2,I)`. Emit input X `Q^-2`, both output-bank `D^2`, and +output X `Q^2`. D and Q act on disjoint address coordinates. The result is + +``` +J A^2 F^-T J^-1 = A U(-Q C) = B_K. +``` + +The first diagonal block is `Q^2 D Q^-2=D`; the second is D; the upper +off-diagonal block is `-Q^2 D Q^-1 C=-D Q C`. C is never commuted across Q. +The implementation performs these exact word reductions independently. +Since `Q^2=Q^-2=X_0` and `D^2=X_[1,25)`, every boundary is ordinary. The +consecutive X-bank output masks are literally composed to `X_[0,25)`. + +The resulting program retains all 1,024 original fields. The transformed +scalar word acts on independent coordinates obtained by its explicitly +conjugated incoming wrappers and input boundary. Replaying every ADD gives +unchanged Y coordinates and X coordinate `u-K_odd^T v`. The gatewise +inverse-transpose identity, including its ordinary boundary factors, +identifies this logical replay with the stated physical B_K endpoint on +arbitrary independent original ground-chart inputs. No coupled X endpoint +is credited as a separate autonomous Gaussian output. + +The paid profile remains 512 children of each width 8,9,15,16 per cube. +There is one new X per child and three boundary X factors per owner port. +The complete per-port ordinary invoice is therefore 76 ADD,15 P,15 D, +13 X,6 phase. The implementation verifies these counts from the literal +stream, including identity opcodes; it performs no COPY or CLEAR. + +The transformed X rows have intermediate coefficient l1 at most 8 and +denominator exponent at most 4, while Y rows remain unchanged. All address +factors and boundaries are unitary, so the same factor 8 bounds each field +norm relative to the largest independent original input norm. This remains +a local growth constant rather than a complete caller precision analysis. + +At positive field width f, the address maps tensor-lift and a literal +scalar phase theta becomes `i^(f theta)`. The real owner ADD coefficients +are negated and transposed once. The owner K matrix is never raised to a +tensor power. The same generic transformation applies independently to +every cube in the structured all-family forward constructor. + +This is a backward K component. It neither produces H nor closes a whole +caller, and gives no precision/storage admission or kappa improvement. diff --git a/research/programmable-native-stage/fusion/inputs/K-MODULE.json b/research/programmable-native-stage/fusion/inputs/K-MODULE.json new file mode 100644 index 0000000000..2486521a39 --- /dev/null +++ b/research/programmable-native-stage/fusion/inputs/K-MODULE.json @@ -0,0 +1,72 @@ +{ + "CLEAR": 0, + "COPY": 0, + "all_original_scalar_columns_checked": 1024, + "axis_dimension": 25, + "code_contract": { + "C_K_commutes_full_R": true, + "C_K_squared_identity": true, + "C_K_symmetric": true, + "proof": "K_odd symmetric involution and real orthogonal direct-owner normalizer similarity; each L_i commutes R exactly" + }, + "cube_tuple": [ + 0, + 0, + 0 + ], + "environment_metadata": { + "program_container_bytes": 1414847, + "program_container_sha256": "dd9d0ecae4aebbef05c8134f1772221c97d2bf818e7a2f464501dbfa9c2856c0" + }, + "helpers": 0, + "logical_growth": { + "max_scalar_denominator_exponent": 4, + "proof": "Each reader retains its own v plus76 distinct independent u terms:12 magnitudes1/4 and64 magnitudes1/16. Sources unchanged; all physical charts/wrappers unitary.", + "reader_max_row_l1": "8", + "source_max_row_l1": "1" + }, + "mutation_controls": { + "missing_actual_ADD_changes_independent_endpoint": true, + "same_tableau_phase_i_rejected": true, + "wrong_parity_common_chart_transport_rank": 2 + }, + "new_kappa": false, + "normalized_endpoint": "F_K=diag(D,D) L(C_K Q^-1), C_K=diag(L_i^-1) K_odd diag(L_i), D=C_[1,25), Q=C_0", + "normalized_entry": "All original x_i,y_i arbitrary independent at physical ground; all virtual-Q source-line entry wrappers are emitted ordinary monomials.", + "ordinary_literal_profile": { + "ADD": 38912, + "D": 7680, + "P": 7680, + "X": 3072, + "phase": 3072 + }, + "original_main_inputs": 1024, + "owned_fields": 0, + "paid_path_applications": 2048, + "paid_profile": { + "15": 512, + "16": 512, + "8": 512, + "9": 512 + }, + "phase_compilation": { + "all_positive_widths": "literal one-copy phases tensor lift; phase opcode theta becomes i^(f theta); owner scalar coefficients applied once", + "all_wrappers_monomial": true, + "low_rank_sparse_peak_support": 512, + "native_full_conjugate_analytic_anchors": 514, + "reader_output_wrappers": 512, + "source_input_wrappers": 512 + }, + "reader_endpoint": "D(y_i+sum_j K_odd[i,j] L_i^-1 L_j Q^-1 x_j)", + "reader_fields": 512, + "schema": "odd-E8-K-normalized-native-rootcase/v1", + "scientific_program_payload_sha256": "98941b295d428462b82dae52a369de97dcbf5be1dd7a369f6c495cda5fc6ac8a", + "scope": "Whole local block-diagonal K native constructor, with phase-complete emitted cube instance and generic forall2744 proof plus independent all-family geometry. It does not implement H, install F3, close any outer caller, admit precision/work/storage, or improve kappa.", + "source_endpoint": "D x_i on every independent original source x_i", + "source_fields": 512, + "source_pins": { + "NORMALIZERS.json": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da", + "clifford_exact.py": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + }, + "status": "PASS_PHASE_COMPLETE_K_NATIVE_ROOTCASE_AND_GENERIC_FAMILY_TEMPLATE" +} diff --git a/research/programmable-native-stage/fusion/inputs/K-PROGRAM.json.gz b/research/programmable-native-stage/fusion/inputs/K-PROGRAM.json.gz new file mode 100644 index 0000000000..86a14df78e Binary files /dev/null and b/research/programmable-native-stage/fusion/inputs/K-PROGRAM.json.gz differ diff --git a/research/programmable-native-stage/fusion/inputs/PROOF.md b/research/programmable-native-stage/fusion/inputs/PROOF.md new file mode 100644 index 0000000000..70d56ae3ff --- /dev/null +++ b/research/programmable-native-stage/fusion/inputs/PROOF.md @@ -0,0 +1,326 @@ +# A complete native K primitive for every odd-E8 product cube + +This constructs the whole block-diagonal three-factor K service, including +the ordinary wrappers that normalize its actual supplied-line interface to +arbitrary ground-chart inputs. It does not produce the cross-cube H service, +install the low-rank F3 decoder, complete an outer caller or claim a kappa. + +The construction is a fixed finite structured word for all 14^3 cubes. +`core.calculate((a,b,c))` emits its exact literal instance for any cube. +The default finite phase replay fully emits cube(0,0,0); it does not pretend +to have expanded all 106,774,528 scalar ADDs or executed every phase instance. +The all-family result follows from the generic frame/phase proof below and +the independent all-2,744-cube geometry checks in `family_geometry.py`. + +Credits remain with Ali Romman's #5439 odd-E8 geometry, the P112/E8 data, +the PR5464 polarized native phase tools, the original native/Clifford +compiler lineage, and the coded-native-caller real centralizing normalizers. +This assembly and its explicit whole-K contract used substantial OpenAI +Codex assistance. New material is Apache-2.0. No independent human or +proof-kernel acceptance is asserted. + +## 1. Actual fields, scalar coefficients and global coordinates + +The pinned NORMALIZERS data supply 112 distinct binary q labels and their +root columns. The roots split into fourteen eight-root sign cubes. For a +cube b, put B_b=M_b M_b^T/4 and K_b=I-B_b. Exact rational checks give +K_b^2=I; each row has four entries +-1/2, all joining opposite selector +parities. The two four-port classes each span a three-space with pairing +rank one, and the two three-spaces are orthogonal. + +A product cube has 512 owners. Define + + K_odd=(K1+K2+K3-K1 K2 K3)/2. + +The three factor matrices commute and square to I. Expanding the square +of their displayed majority polynomial gives I. The scalar K_odd is also +symmetric. Every row has twelve distinct one-factor entries of magnitude +1/4 and sixty-four distinct three-factor entries of magnitude 1/16. +The two support sets are disjoint since each K_b has zero diagonal. +Every nonzero entry reverses total selector parity. Thus each row has +exactly 76 nonzero coefficients and their absolute sum is seven. + +The actual product labels are concatenated triples in F2^27. Their global +span U is the 25-space of equal three-block parities. The code records an +explicit orthonormal basis of U, and takes physical coordinates by dotting +against it. This is one global I25 realization, shared by all cubes; no +local-20-to-global-25 free adapter is introduced. Every port has norm one +and differs from the characteristic vector of U. The latter is the raw +all-ones27 vector, whereas each base label has weight three or seven. + +For every product cube the two 256-port parity classes span S0,S1 with + + dim S0=dim S1=9, S0 perpendicular S1, + rank(B|S0)=rank(B|S1)=1, dim rad(S0)=dim rad(S1)=8. + +Their joint span has dimension ten. `family_geometry.py` checks all +1,404,928 actual norm-one noncharacteristic labels, all 5,488 nine-space +classes and all opposite-reader/source-basis incidences. The restricted +characteristic issue is explicit: every odd q represents the characteristic +functional within S9. The construction never requires a noncharacteristic +vector inside S9, and never tries to orthonormalize this degenerate S9. + +Use two independent fields X_p,Y_p per port p. There are no other independent +fields, no owned full-field scratch, no COPY and no CLEAR. Across the family +the product cubes partition the actual owner indices, so no independent +input is duplicated or identified between cube instances. + +## 2. Canonical frames for arbitrary degenerate subspaces + +All operator products below act rightmost first. The primitive convention is + + C_q=((1+i)I+(1-i)X_q)/2. + +Write R=C_[0,25), Q=C_0 and D=C_[1,25), so R=DQ. If the columns of G are +any full binary basis and A=G^-1, put + + K_G=D_J P_G, J=I+A^T A. + +Here the diagonal uses the retained compiler's Z4 quadratic convention. +For the first r columns spanning S, the actual native frame is + + Phi_(G,r)=K_G C_[0,r) K_G^-1. + +It is not necessary for the restricted form on S to be nondegenerate. +Its binary symplectic action sends the Z Lagrangian to + + L_S={(x,z): x in S and z+x in S-perp}. + +To check this directly, let B=G P_r G^T. On a Z input z the output X part +is x=Bz, and its Z part is z+JBz. Since J=I+G^-T G^-1, the vector formed +by adding x to that output Z part is z+G^-T G^-1 x. Its dot product with +every first-r basis column vanishes. Dimensions give exactly L_S. +The symplectic action of C, and therefore of Phi, is an involution; +the inverse frame has the same Lagrangian image. + +Consequently two constructions of the same S differ by a monomial map. +If S is contained in T, their transition has Gaussian rank + + 25-dim(L_S intersect L_T)=dim T-dim S. + +Indeed their intersection has x in S and z+x in T-perp, hence dimension +dim S+25-dim T. This proves all required rank and zero-rank statements +for every actual cube, not only for the root instance's tableaux. + +## 3. Literal source and reader paths + +Fix a source parity class S9. All sources in it and all opposite readers +will meet at one and the same literal canonical Phi_S9 word. Each source +q belongs to S9. Its line-to-S9 path costs H8. To emit this path, choose +a full flag whose first vector is q and first nine vectors span S9. +Monomial gauges connect its one- and nine-dimensional frames to the +declared canonical frames, and the only Gaussian child is C_[1,9). + +A reader q is orthogonal to S9 and has norm one. Therefore it is outside +S9 and its q-perp24 contains S9. The reader starts at ground, reaches +Phi_S9 by one H9, and leaves it by one H15 to a full flag beginning with +the identical ordered S9 basis and spanning that actual q-perp24. +The emitted word supplies every reader's actual endpoint flag. + +The source leaves S9 for canonical full R by one H16. Let + + T_G=R K_G R^-1. + +The source-exit word executes K_G^-1, then C_[9,25), then T_G, since + + R Phi_S9^-1=T_G C_[9,25) K_G^-1. + +No extra Gaussian is hidden in T_G; its exact monomial phase is given +in section 4. All other gauges are compiled as P/D/X/phase-only words. + +At the common cut, directly execute Y_r += K_odd[r,s] X_s for every +nonzero scalar coefficient. The two main banks are independent. X is +never modified by these ADDs, so every source read uses its original +geometric logical value. Every reader retains its arbitrary old value +with coefficient one. There is no need for a rank-one cache or any +owned helper, even though the scalar matrix between the classes is full +rank. The two parity directions use disjoint source/reader field sets +and are executed separately. Every ADD is at an actually identical frame, +not merely between containing or cross-orthogonal subspaces. + +The geometric endpoint is exactly + + X_s: Phi_[q_s] u_s -> R u_s, + Y_r: v_r -> Phi_(q_r-perp)(v_r+sum_s K_odd[r,s]u_s). + +Every 512-port cube thus uses 512 children of each of widths 8,9,15,16, +and 38,912 ordinary scalar ADDs, with no helper or owned field. + +## 4. Absolute phases without exponential dense columns + +The retained signed tableau fixes a Clifford operator up to scalar. +Every low-rank monomial gauge is checked with an exact sparse +Gaussian-integer zero-column evaluation that fixes this scalar as well. +For same-S9 gauges the sparse support remains at most 512: after changing +coordinates, both rank-nine Gaussian portions act inside the same prefix. +The normalization gauges below need at most two one-axis Gaussians. + +For any native full basis G, let a_j=G^-1 e_j and set + + d_j=floor(wt(a_j)/2) mod 2. + +If q_J is the diagonal's actual Z4 phase, XOR Hamming-weight expansion +modulo four gives + + q_J(y)+wt(G^-1 y)=wt(y)+2d.y mod4. + +The quadratic cross terms cancel. For each j, its remaining linear +coefficient is alpha_j+wt(a_j), with alpha_j=(1+wt(a_j)) mod2 in {0,1}; +this equals 1+2d_j modulo four. With a=(1-i)/2, + + R^-1|0>=a^25 sum_x i^wt(x)|x>, + K_G R^-1|0>=Z_d R^-1|0>, + T_G|0>=(-i)^wt(d)|d>. + +Furthermore T_G is monomial: R^-1 takes Z Paulis to the diagonal +Lagrangian {(z,z)}, K_G takes it to {(Gz,Gz)}, and R takes it back to +Z Paulis. Its exact signed tableau plus this absolutely normalized +column determines the emitted P/D/X/phase word universally. No 2^25 +state is allocated. `frame_tools.py` retains this analytic anchor. + +These generic arguments prove the compiler construction for every cube +and every flag satisfying the verified geometry. Default execution fully +corroborates all actual root-case gauges, including 512 reader-output +full-basis anchors, rather than sampling a few field pairs. + +## 5. Real normalizers and virtual-Q entry + +The geometric input line service above is not silently assumed free in +the normalized native F_K. We explicitly wrap arbitrary ground inputs. +For each physical q, construct an orthogonal binary G_i taking e0 to q. +If q_0=0 use the even transvection T_(e0+q). Otherwise choose j>0 with +q_j=0 and use T_(ej+q) T_(e0+ej). Such j exists because q is not the +ambient characteristic vector. + +For row j of G_i put z_j=(wt(row_j)-1)/2 modulo two and define + + L_i=Z_z P_Gi. + +This is a real signed orthogonal monomial. Orthogonality cancels every +quadratic cross coefficient in the weight identity + + wt(G_i^-1 x)-wt(x)=2z.x mod4. + +It follows that L_i R L_i^-1=R exactly, including absolute phase. +Checking orthogonality and the 25 linear coefficients proves the weight +identity for all 2^25 addresses; no address sampling is used. + +The actual ordinary normalized wrappers are + + input X: Phi_[q_i] L_i Q^-1, + input Y: L_i, + output X: L_i^-1, + output Y: D L_i^-1 Phi_(q_i-perp)^-1. + +Their monomiality follows from the corresponding line/hyperplane +Lagrangian incidences. Input X's literal defining word has two one-axis +Gaussian factors and is compiled with exact sparse absolute phase. +It is emitted and executed as an ordinary monomial; Q^-1 is virtual +inside this identity, not an additional unpriced Gaussian instruction. + +For the potentially high-rank reader-output wrapper let its endpoint +flag be Phi_V=K_v C_[0,24) K_v^-1. The exact low-rank expression is + + D L_i^-1 Phi_V^-1 + =Q^-1 L_i^-1 T_v C_24 K_v^-1, + T_v=R K_v R^-1. + +This follows by C_[0,24)^-1=R^-1 C_24 and [L_i,R]=0. The right side +has only two one-axis Gaussian factors plus phase-complete monomials. +Its signed tableau is checked against the defining left side, and its +absolute phase is compiled from the low-rank expression. Thus no +rank-24 dense zero column is needed and no projective phase is discarded. + +## 6. Normalized arbitrary-input endpoint + +Let x_i,y_i be the actual independent ground inputs. After input wrappers +the geometric logical values are exactly + + u_i=L_i Q^-1 x_i, v_i=L_i y_i. + +These are invertible functions of the original independent inputs; they +are not being renamed originals or assumed zero. The actual emitted +input-X monomial already puts its physical field at Phi_[q_i]u_i. + +Source output followed by its wrapper is + + L_i^-1 R L_i Q^-1 x_i = D x_i. + +Reader output followed by its wrapper is + + D y_i + sum_j K_odd[i,j] D L_i^-1 L_j Q^-1 x_j. + +Define, at actual field width f, + + (C_K,f)_ij=K_odd[i,j] L_i,f^-1 L_j,f. + +The complete normalized operator is therefore + + F_K=diag(D,D) L(C_K Q^-1). + +K_odd is a real symmetric involution and the L_i are real orthogonal. +Thus C_K^T=C_K, C_K^2=I and [C_K,R]=0. These facts follow by actual +operator similarity. They do not tensor the whole owner matrix: +scalar K_odd coefficients are applied once, and cancellation of adjacent +L_j,f L_j,f^-1 proves the square identity at every positive width. + +All 1,024 geometric original columns are explicitly interpreted in the +root-case word; the incoming-column and outgoing-row factor identities +above imply all 38,912 nonzero normalized operator blocks at once. No +sampling of cross-owner physical operators is used. + +The normalized source outputs are autonomous rank-24 D transforms of +their original inputs. Reader outputs remain the specified triangular +coupled transforms. The service is invertible and retains every original +input; a complete outer Gaussian caller and its larger productive jobs +must still be supplied before using any whole-caller target profile. + +## 7. All positive widths and complete local accounting + +Every single-copy identity includes its absolute phase. Tensor it +columnwise to f positive address columns. P and X lift as binary block +maps, D sums its Z4 phase over the columns, and a single-copy phase theta +becomes i^(f theta). Scalar owner coefficients are applied once per field. +No width-one sum relation has been extrapolated by taking a tensor power +of a sum. This proves the actual physical word and F_K endpoint for every f. + +The normalized root case has 512 fields of each X/Y role and profile + + paid {8:512,9:512,15:512,16:512}, + ordinary {ADD:38912,P:7680,D:7680,X:3072,phase:3072}. + +There are 42 literal monomial primitives and 76 scalar ADDs per owner, +in addition to its four correctly charged Gaussian paths. These are +nonrecursive work, not zero-work operations. Their address movement, +storage, precision and tape price remain eventual caller obligations. +No helper input, helper target, owned field, COPY or CLEAR is introduced. + +For v=112^3=1,404,928, concatenate the cube words in lexicographic order. +The whole-family profiles are + + paid {8:v,9:v,15:v,16:v}, + ordinary {ADD:76v,P:15v,D:15v,X:6v,phase:6v}. + +The number of actual main inputs is 2v=2,809,856. The Gaussian rank mass +is 48v. No smaller pairing rank is substituted for any physical child. + +At geometric logical opcode boundaries each source row has l1 one and +each reader has its old value plus distinct source coefficients of total +l1 seven. Hence all prefix row l1 values are at most eight, and scalar +denominator exponent is at most four. Physical charts and wrappers are +unitary, so independent input norm at most M gives field norms at most +M for sources and 8M for readers. This is a finite local growth constant, +not a complete recursive rounding-error, precision or outer-admission bill. + +Actual mutation controls detect a global phase i despite an identical +signed tableau, a wrong parity S9 frame (requiring rank-two transport), +and omission of a literal K ADD (changing an independent input column). + +## 8. Remaining scope + +This fills the local K-native construction gate. It does not provide H, +remove H by a global basis change, make the F3 factor totals freely +available, prove a decoder/reader chronology, or close the mixed-Q +E=I-H interface. No whole-caller profit or kappa improvement is claimed. +The earlier planning profile and separated-helper obstruction cannot +be reused as a completed budget for this changed primitive. diff --git a/research/programmable-native-stage/fusion/verify.py b/research/programmable-native-stage/fusion/verify.py new file mode 100644 index 0000000000..c7dfa6f62c --- /dev/null +++ b/research/programmable-native-stage/fusion/verify.py @@ -0,0 +1,128 @@ +"""Literal whole-K coded-thin fusion; only scalar ADD coefficients change. +Apache-2.0; substantial OpenAI Codex assistance. No new kappa is claimed. +""" +from collections import Counter +from fractions import Fraction as F +from pathlib import Path +import gzip,hashlib,json,sys +ROOT=Path(__file__).resolve().parent + +def need(condition,message): + if not condition:raise ValueError(message) + +def inputs(): + pins=json.loads((ROOT/'SOURCES.json').read_text(encoding='utf-8'))['sources'] + out={} + for record in pins: + data=(ROOT/'inputs'/record['file']).read_bytes() + need(hashlib.sha256(data).hexdigest()==record['sha256'],'Changed pinned source: '+record['file']) + if record['file'].endswith('.gz'): + data=gzip.decompress(data) + need(hashlib.sha256(data).hexdigest()==record['payload_sha256'],'Changed scientific payload') + if record['file'].endswith(('.json','.json.gz')):out[record['file']]=json.loads(data) + return out + +def fuse(word,extra): + """Return the actual modified instruction stream for one added coded thin. + `extra` is lambda; mu=1+lambda scales every existing cut ADD. No new + oracle, monomial, paid path, memory field or chart change is introduced. + """ + mu=1+F(extra);den=mu.denominator + need(den&(den-1)==0,'The fixed caller coefficient must be dyadic') + stream=[] + for event in word['program']: + if event[0]!='ADD':stream.append(event);continue + if not mu:continue + changed=list(event);coefficient=mu*F(event[5],event[6]) + changed[5],changed[6]=coefficient.numerator,coefficient.denominator + stream.append(changed) + return stream + +def replay(word,stream,inverse=False): + ports=word['port_order'];prefix='conjugate:'if inverse else'' + rows={(r,p):{(r,p):F(1)}for r in ['X','Y']for p in ports} + charts={(r,p):prefix+('line:'+str(p)if r=='X'else'ground')for r,p in rows} + paid,ordinary=Counter(),Counter() + def monomial(key): + literal=word['definitions'][key] + need(all(op[0]in('P','D','X','phase')for op in literal),'Hidden Gaussian in ordinary map') + ordinary.update(op[0]for op in literal) + for index,event in enumerate(stream): + kind=event[0] + if kind in('MONOMIAL','BOUNDARY_MONOMIAL'): + monomial(event[3]) + elif kind=='PAID_PATH': + _,role,port,old,new,path=event + need(charts[role,port]==old,'Paid path enters wrong actual chart') + need(path['rank']==len(path['child_axes']),'Changed paid-child rank') + charts[role,port]=new;paid[path['rank']]+=1 + monomial(path['before_monomial']);monomial(path['after_monomial']) + else: + need(kind=='ADD','Unknown literal event') + _,dr,dp,sr,sp,a,b,chart=event + need(charts[dr,dp]==charts[sr,sp]==chart,'ADD crosses different actual S9 charts') + need((dr,dp)!=(sr,sp),'Overwriting a source during cut accumulation') + for variable,value in rows[sr,sp].items(): + v=rows[dr,dp].get(variable,F(0))+F(a,b)*value + if v:rows[dr,dp][variable]=v + else:rows[dr,dp].pop(variable,None) + ordinary['ADD']+=1 + return rows,charts,dict(sorted(paid.items())),dict(sorted(ordinary.items())) + +def expected(word,mu,inverse=False): + rows={(r,p):{(r,p):F(1)}for r in ['X','Y']for p in word['port_order']} + for reader,row in word['literal_scalar_K_rows'].items(): + for source,a,b in row: + target,variable=(('X',source),('Y',int(reader)))if inverse else(('Y',int(reader)),('X',source)) + value=F(a,b)*mu*(-1 if inverse else 1) + if value:rows[target][variable]=value + return rows + +def involution(word): + # K has denominator16. Check the exact integer matrix square, no float. + matrix={int(r):{s:int(F(a,b)*16)for s,a,b in row}for r,row in word['literal_scalar_K_rows'].items()} + checks=0 + for r,row in matrix.items(): + out={} + for k,a in row.items(): + for s,b in matrix[k].items():out[s]=out.get(s,0)+a*b + out={s:v for s,v in out.items()if v} + need(out=={r:256},'Literal scalar K is not an involution');checks+=len(matrix) + return checks + +def check(): + source=inputs();forward=source['K-PROGRAM.json.gz'];backward=source['B-PROGRAM.json.gz'] + result={'status':'PASS_LITERAL_CODED_THIN_FUSION','new_kappa':False, + 'input_columns':2*len(forward['port_order']),'exact_K_square_entries':involution(forward),'cases':[]} + for extra in [0,1,-1,-2,F(1,2)]: + mu=1+extra + for inverse,word,name in [(False,forward,'forward'),(True,backward,'backward')]: + program=fuse(word,extra) + rows,charts,paid,ordinary=replay(word,program,inverse) + need(rows==expected(forward,mu,inverse),'Changed coefficient family endpoint') + need(paid=={8:512,9:512,15:512,16:512},'A new paid child was introduced') + need(ordinary.get('ADD',0)==(38912 if mu else 0),'Unpaid or missing ordinary ADD') + need(all(charts['X',p]==('conjugate:'if inverse else'')+'full25'for p in word['port_order']),'Source final charts') + need(all(charts['Y',p]==('conjugate:'if inverse else'')+'qperp24:'+str(p)for p in word['port_order']),'Reader final charts') + result['cases'].append({'direction':name,'extra_coded_thin':str(extra),'total_transfer_multiplier':str(mu), + 'literal_events':len(program),'paid':paid,'ordinary':ordinary}) + controls=[] + base=fuse(forward,1);index=next(i for i,e in enumerate(base)if e[0]=='ADD') + bad=base.copy();bad[index]=list(bad[index]);bad[index][5]+=1 + rows,*_=replay(forward,bad) + need(rows!=expected(forward,2),'Coefficient mutation accepted');controls.append('wrong_cut_coefficient') + bad=base.copy();bad[index]=list(bad[index]);bad[index][7]='S9:wrong' + try:replay(forward,bad) + except ValueError as exc:need(str(exc)=='ADD crosses different actual S9 charts','Wrong frame rejection') + else:raise ValueError('Wrong-chart mutation accepted') + controls.append('wrong_physical_chart') + need([e for e in base if e[0]!='ADD']==[e for e in forward['program']if e[0]!='ADD'],'A literal native/phase path changed') + result['rejected_controls']=controls + result['scope']='Exact all-column scalar/frame replay; all original monomial/paid/phase paths retained literally. Native physical correctness and all-width phase proof inherited from pinned upstream.' + return json.loads(json.dumps(result)) + +if __name__=='__main__': + report=check();path=ROOT/'RESULT.json' + if '--emit'in sys.argv:path.write_text(json.dumps(report,indent=2)+'\n',encoding='utf-8') + else:need(report==json.loads(path.read_text(encoding='utf-8')),'Frozen mathematical receipt differs') + print(report['status'],'columns='+str(report['input_columns']),'cases='+str(len(report['cases']))) diff --git a/research/programmable-native-stage/native/INTERTWINER-PROOF.txt b/research/programmable-native-stage/native/INTERTWINER-PROOF.txt new file mode 100644 index 0000000000..9f1dda8bce --- /dev/null +++ b/research/programmable-native-stage/native/INTERTWINER-PROOF.txt @@ -0,0 +1,109 @@ +Programmable native stages and exact intertwiners + +Scope. This is a sufficient all-width application theorem for the actual +whole-K native constructor in PR #5464, head +3981f9539e63630681f6903e3c6a50b3a0d2f2dd. It supplies an adjustable native +macro and exact algebra for composing its stages. It is not a completed outer +caller, a precision admission, or a new kappa claim. The native phase and +all-family geometry proofs are inherited explicitly from that PR. + +Theorem 1 (programmable common-cut transfer). +Fix any of the 2,744 product cubes. Keep the exact source and reader paths, +ordinary normalization wrappers and their order in core.calculate. At its +common-cut ADD instructions replace K[r,s] by any rational matrix M[r,s] +whose nonzero entries join opposite selector parities. Emit one ADD for each +nonzero entry, preserving the same two parity directions. Then the normalized +physical endpoint, on independent arbitrary original ground inputs, is + + X -> D X, + Y -> D (Y + C_M Q^-1 X), + C_M = diag(L_r^-1) M diag(L_s). + +The exact paid profile per owner remains {8:1,9:1,15:1,16:1}. There are no +helpers, owned fields, COPY or CLEAR. The scalar ADD count is nnz(M), not the +original fixed count unless M has the same support. The existing ordinary +monomial wrappers remain unchanged. Scalar arithmetic uses the chosen exact +rational coefficients; numerical precision must be admitted separately. + +Proof. In each parity direction all sources and opposite readers are in the +same literal canonical Phi_S9 frame before any ADD. Every source retains its +original value and every reader retains its independent old value with +coefficient one. Thus the common-cut row is v_r + sum_s M[r,s]u_s, for every +independent column, without requiring symmetry, invertibility or low rank of M. +The source and reader exits are linear operators independent of M. Applying +the published ordinary entry and exit identities gives exactly the endpoint +above. The source paths are H8 then H16 and reader paths H9 then H15, so changing +only ADD coefficients cannot change any Gaussian child or introduce a field. +The argument holds for each positive address width f: scalar coefficients are +applied once to entire fields; all frame operators are the published tensor +lifts. It takes no tensor power of M. This proves the assertion uniformly. + +Corollary 1. For arbitrary rational lambda, M=lambda K gives + F_lambda = diag(D,D) L(lambda C Q^-1), +with the same paid profile. At lambda=0 the ADDs may be omitted. Applying the +published backward-word construction likewise supplies + B_lambda = diag(D,D) U(-lambda Q C). +These statements concern actual physical normalized endpoints, not role labels. + +Corollary 2 (local norm and coefficient bounds). +For M=lambda K each source has logical row norm one and each partial reader +row has l1 norm at most 1+7|lambda|. Hence the norm of every physical field +at every prefix is at most (1+7|lambda|) times the largest norm of an original +input, provided the initial inputs are measured in the same Hilbert norm. +Proof: each source is unchanged; each reader receives each distinct source at +most once, and its total coefficient absolute sum is at most 7|lambda|. +All physical path prefixes and normalization wrappers are unitary. Apply the +triangle inequality at each ADD. No arbitrary-precision or storage admission +follows merely from this local growth estimate. + +Theorem 2 (ordinary normalized stage). +Let C be any ordinary invertible bank recoding satisfying C^2=I and +[C,DQ]=0, where D and Q commute. Define A=CD, B=DC and L=diag(A,B). +For ordinary pre-recoding T=diag(I,C) and post-recoding S=diag(C,I), + + S F_lambda T = L L_lower(lambda Q^-1), + S B_lambda T = L U_upper(-lambda Q), + A Q = Q B. + +Consequently L commutes with both displayed weighted shears, for every scalar +lambda. Proof: diagonal blocks become CD and DC. For the lower-left block, +directly S F_lambda T has lower-left D lambda C Q^-1, +while L L_lower has lower-left D C lambda Q^-1. They coincide. For the +upper-right block S B_lambda T has -lambda C D Q C^2 = -lambda C D Q, +which equals the required -lambda A Q. Finally C D Q = D Q C = Q D C +proves A Q = Q B, and multiplying by Q^-1 gives the lower shear identity. +All operations are finite bank recodings or the already supplied native macro. + +Theorem 3 (ordered products on fresh axes). +Suppose D_i commute with Q and each other, C_i^2=I, +[C_i,D_i Q]=0, and [C_i,D_j]=0 for i != j. Define A_i=C_i D_i, +B_i=D_i C_i. For any ordered distinct stage list i_m,...,i_1, let +P=C_i_m ... C_i_1 and D_all=D_i_m ... D_i_1. Then + + A_i_m ... A_i_1 = P D_all, + B_i_m ... B_i_1 = D_all P, + (P D_all)Q = Q(D_all P) = P(D_all Q), + [P,D_all Q]=0. + +Proof. Move each D_i only past C_j with j != i to obtain the first two +identities; no two C factors are exchanged. Each C_i commutes with D_all Q, +since it commutes with D_i Q and all other D_j. This proves the last identity, +and the middle one follows by the stage intertwining identity or direct +multiplication. This theorem does not assume C_i commute with one another. +It is valid for the actual fresh-axis embeddings whenever the stated support +conditions are checked by the caller. + +Boundary obligation. An ordinary signed SWAP is not a free weighted swap. +For one letter L=diag(A,B), the weighted three-shear word satisfies + J L_lower(Q^-1) L U_upper(-Q) L_lower(Q^-1) + = diag(B Q^-1, A Q), +where J=[[0,I],[-I,0]]. The second output has the good Gaussian-plus-ordinary +form C(DQ); the first does not follow from the preceding theorems to have the +same form. No complete caller or kappa is inferred by omitting this boundary. + +Credit. The actual whole-K paid paths, phases, source geometry and ordinary +entry/exit compiler come from PR #5464 and its cited Ali Romman #5439 odd-E8, +P112/E8, original native/Clifford compiler and coded-normalizer predecessors. +The programmable transfer and explicit noncommutative intertwiner application +here were developed with substantial OpenAI Codex assistance. No independent +human or Lean-kernel review is asserted. diff --git a/research/programmable-native-stage/native/RESULT.json b/research/programmable-native-stage/native/RESULT.json new file mode 100644 index 0000000000..13764f4f50 --- /dev/null +++ b/research/programmable-native-stage/native/RESULT.json @@ -0,0 +1,28 @@ +{ + "exact_intertwiner_controls": 102, + "native_amplitudes": [ + "0", + "1", + "-1", + "2", + "1/2" + ], + "native_independent_columns_per_instance": 1024, + "native_paid_profile_per_cube": { + "15": 512, + "16": 512, + "8": 512, + "9": 512 + }, + "new_kappa": false, + "normal_and_optimized_python": true, + "phase_checks": "inherited pinned PR5464 proofs, not regenerated here", + "sha256": { + "INTERTWINER-PROOF.txt": "14e85d43b61e959d92ff58c285c193b1619c6f4fbdbe50c2eaf10a065134a2c8", + "SOURCE-PINS.json": "eb8d5f23db43798752bba985b08c643a292eea4b7aa9868495688df691288633", + "programmable_stage.py": "9d434dd2e7388be7f83b54819382c0634eccda7bb057e9973eea9edfea0ad0bd", + "verify_intertwiners.py": "f2119319355d8f07c6f09dea6792764ccba74baf0de289f103155734fd626c54" + }, + "status": "PASS", + "universal_theorem": "INTERTWINER-PROOF.txt" +} diff --git a/research/programmable-native-stage/native/SOURCE-PINS.json b/research/programmable-native-stage/native/SOURCE-PINS.json new file mode 100644 index 0000000000..9942e9c60f --- /dev/null +++ b/research/programmable-native-stage/native/SOURCE-PINS.json @@ -0,0 +1,14 @@ +{ + "commit": "3981f9539e63630681f6903e3c6a50b3a0d2f2dd", + "credits": "Ali Romman PR5439 odd-E8 geometry; P112/E8; original native/Clifford compiler; coded-native-caller normalizers; PR5464 complete native K supplier; substantial OpenAI Codex assistance.", + "files": { + "BACKWARD-PROOF.md": "04ab96921464d5a50a7a6b57b212d8fffe57d3e5f230a66e70782a2510c7f6fb", + "K-MODULE.json": "02cec9cb8ce148c9a2ee97a899338b330b4b3efd1455b4243466987e09b354a0", + "K-PROGRAM.json.gz": "dd9d0ecae4aebbef05c8134f1772221c97d2bf818e7a2f464501dbfa9c2856c0", + "PROOF.md": "99e5b12bc5f5e67e5c1e49394dbb88746da46ae3d8760598c8b435b9d0baec9c" + }, + "license": "Apache-2.0, inherited source notices retained", + "pull_request": 5464, + "source_directory": "research/odd-e8-whole-k-native", + "source_repository": "thu-nmrc/integer-mult-bounds" +} diff --git a/research/programmable-native-stage/native/programmable_stage.py b/research/programmable-native-stage/native/programmable_stage.py new file mode 100644 index 0000000000..d00aff4300 --- /dev/null +++ b/research/programmable-native-stage/native/programmable_stage.py @@ -0,0 +1,81 @@ +#!/usr/bin/env python3 +"""Literal rational-amplitude specialization of pinned whole-K native cube.""" +from collections import Counter +from fractions import Fraction as F +from hashlib import sha256 +from pathlib import Path +import argparse,gzip,json +HERE=Path(__file__).resolve().parent + +def need(ok,msg): + if not ok:raise ValueError(msg) +def source(): + pins=json.loads((HERE/'SOURCE-PINS.json').read_bytes()) + for name,digest in pins['files'].items(): + need(sha256((HERE/'vendor'/name).read_bytes()).hexdigest()==digest,'source pin '+name) + return json.loads(gzip.decompress((HERE/'vendor/K-PROGRAM.json.gz').read_bytes())) +def specialize(payload,lam): + result=json.loads(json.dumps(payload));out=[] + for event in result['program']: + if event[0]=='ADD': + q=lam*F(event[5],event[6]) + if not q:continue + event[5:7]=[q.numerator,q.denominator] + out.append(event) + result['program']=out + result['schema']='programmable-whole-K-rational-amplitude/v1' + result['amplitude']=[lam.numerator,lam.denominator] + # Upstream endpoint_rows describe lambda=1; never retain stale metadata. + for row in result['logical_endpoint_rows']['reader_rows'].values(): + for term in row: + if term[0]=='X': + q=lam*F(term[2],term[3]);term[2:4]=[q.numerator,q.denominator] + result['literal_scalar_K_rows']={r:[[s,(lam*F(a,b)).numerator,(lam*F(a,b)).denominator]for s,a,b in row]for r,row in result['literal_scalar_K_rows'].items()} + return result + +def verify(payload,lam): + ports=payload['port_order'];charts={('X',p):'line:'+str(p)for p in ports} + charts.update({('Y',p):'ground'for p in ports}) + rows={('X',p):{('X',p):F(1)}for p in ports};rows.update({('Y',p):{('Y',p):F(1)}for p in ports}) + paid=Counter();adds=0 + for e in payload['program']: + if e[0]=='MONOMIAL':continue # Exact inherited monomial wrappers change physical frames, not the geometric u,v columns. + if e[0]=='PAID_PATH': + _,role,p,old,target,record=e + need(charts[role,p]==old,'actual path chronology') + charts[role,p]=target;paid[record['rank']]+=1 + elif e[0]=='ADD': + _,dr,d,sr,s,a,b,chart=e + need(dr=='Y'and sr=='X','source bank never modified') + need(charts[dr,d]==charts[sr,s]==chart,'literal equal-frame ADD') + q=F(a,b) + for key,v in rows[sr,s].items(): + value=rows[dr,d].get(key,F(0))+q*v + if value:rows[dr,d][key]=value + else:rows[dr,d].pop(key,None) + adds+=1 + else:raise ValueError('unknown opcode') + need(paid=={8:512,9:512,15:512,16:512},'complete unchanged paid histogram') + for p in ports: + need(rows['X',p]=={('X',p):F(1)},'every independent source retained') + expected={('Y',p):F(1)} + for s,a,b in payload['literal_scalar_K_rows'][str(p)]: + if a:expected['X',s]=F(a,b) + need(rows['Y',p]==expected,'every original independent column') + declared={(role,s):F(a,b)for role,s,a,b in payload['logical_endpoint_rows']['reader_rows'][str(p)]if a} + need(declared==expected,'serialized endpoints match actual ADD rows') + need(adds==(38912 if lam else 0),'actual amplitude ADD count') + return {'amplitude':[lam.numerator,lam.denominator],'paid':dict(sorted(paid.items())),'ADD':adds,'independent_columns':1024} +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--amplitude');ap.add_argument('--output');a=ap.parse_args() + original=source();amplitudes=[F(a.amplitude)]if a.amplitude is not None else [F(0),F(1),F(-1),F(2),F(1,2)] + records=[] + for lam in amplitudes: + payload=specialize(original,lam);records.append(verify(payload,lam)) + if a.output: + need(len(amplitudes)==1,'output requires explicit amplitude') + target=Path(a.output);need(not target.exists(),'refuse overwrite output') + encoded=(json.dumps(payload,sort_keys=True,separators=(',',':'))+'\n').encode() + target.write_bytes(gzip.compress(encoded,mtime=0)) + print(json.dumps({'status':'PASS','native_instances':records,'inherited_phase_scope':'vendor/PROOF.md','new_kappa':False},sort_keys=True)) +if __name__=='__main__':main() diff --git a/research/programmable-native-stage/native/vendor/BACKWARD-PROOF.md b/research/programmable-native-stage/native/vendor/BACKWARD-PROOF.md new file mode 100644 index 0000000000..0777adf3d8 --- /dev/null +++ b/research/programmable-native-stage/native/vendor/BACKWARD-PROOF.md @@ -0,0 +1,77 @@ +# Literal backward native K + +Let `A=diag(D,D)` and `C=C_K`. The proved forward word is +`F=A L(C Q^-1)`. Since C is real symmetric and Q is symmetric, + +``` +F^-T = A^-1 U(-Q^-1 C). +``` + +Every emitted gate is invertible. There is no CLEAR, COPY, allocation or +owned zero field. If the chronological gates are `E_1,...,E_m`, the matrix +is `F=E_m ... E_1`, and `F^-T=E_m^-T ... E_1^-T`. Thus the same chronological +gate order, with each gate replaced by its inverse transpose, is exact. +This statement does not reverse chronological order. + +For a real scalar ADD `destination += c source`, inverse transpose is +`source += -c destination`. For an ordinary unitary monomial M, inverse +transpose is its complex conjugate. The literal P and X factors remain +unchanged; each D factor retains its quadratic coefficient 2 modulo 4 and +negates its Z4 linear coefficients; each scalar phase is negated modulo 4. +The entire chronological monomial factor order remains unchanged. + +Each paid child is a product of commuting positive coordinate Gaussians. +On one coordinate `C_plus^2=X` and `C_plus^4=I`, including their scalar +phases. Therefore `C_minus=C_plus X`. A rank-r inverse child is emitted +as the same positive rank-r child followed by the single ordinary X whose +mask is the sum of the r child coordinate vectors. This is a literal +phase identity on all address columns, not only an equality of tableaux. +`backward.py` checks it densely on all columns and all nonempty coordinate +subsets for dimensions 1 through 4, and checks the first physical rank-8 +path with fresh sparse Gaussian-integer arithmetic. Every translated +physical path also has its conjugated signed tableau and rank checked. +The all-dimensional result follows directly from the one-coordinate +identity and commuting tensor factors. + +Now put `J=diag(Q^2,I)`. Emit input X `Q^-2`, both output-bank `D^2`, and +output X `Q^2`. D and Q act on disjoint address coordinates. The result is + +``` +J A^2 F^-T J^-1 = A U(-Q C) = B_K. +``` + +The first diagonal block is `Q^2 D Q^-2=D`; the second is D; the upper +off-diagonal block is `-Q^2 D Q^-1 C=-D Q C`. C is never commuted across Q. +The implementation performs these exact word reductions independently. +Since `Q^2=Q^-2=X_0` and `D^2=X_[1,25)`, every boundary is ordinary. The +consecutive X-bank output masks are literally composed to `X_[0,25)`. + +The resulting program retains all 1,024 original fields. The transformed +scalar word acts on independent coordinates obtained by its explicitly +conjugated incoming wrappers and input boundary. Replaying every ADD gives +unchanged Y coordinates and X coordinate `u-K_odd^T v`. The gatewise +inverse-transpose identity, including its ordinary boundary factors, +identifies this logical replay with the stated physical B_K endpoint on +arbitrary independent original ground-chart inputs. No coupled X endpoint +is credited as a separate autonomous Gaussian output. + +The paid profile remains 512 children of each width 8,9,15,16 per cube. +There is one new X per child and three boundary X factors per owner port. +The complete per-port ordinary invoice is therefore 76 ADD,15 P,15 D, +13 X,6 phase. The implementation verifies these counts from the literal +stream, including identity opcodes; it performs no COPY or CLEAR. + +The transformed X rows have intermediate coefficient l1 at most 8 and +denominator exponent at most 4, while Y rows remain unchanged. All address +factors and boundaries are unitary, so the same factor 8 bounds each field +norm relative to the largest independent original input norm. This remains +a local growth constant rather than a complete caller precision analysis. + +At positive field width f, the address maps tensor-lift and a literal +scalar phase theta becomes `i^(f theta)`. The real owner ADD coefficients +are negated and transposed once. The owner K matrix is never raised to a +tensor power. The same generic transformation applies independently to +every cube in the structured all-family forward constructor. + +This is a backward K component. It neither produces H nor closes a whole +caller, and gives no precision/storage admission or kappa improvement. diff --git a/research/programmable-native-stage/native/vendor/K-MODULE.json b/research/programmable-native-stage/native/vendor/K-MODULE.json new file mode 100644 index 0000000000..2486521a39 --- /dev/null +++ b/research/programmable-native-stage/native/vendor/K-MODULE.json @@ -0,0 +1,72 @@ +{ + "CLEAR": 0, + "COPY": 0, + "all_original_scalar_columns_checked": 1024, + "axis_dimension": 25, + "code_contract": { + "C_K_commutes_full_R": true, + "C_K_squared_identity": true, + "C_K_symmetric": true, + "proof": "K_odd symmetric involution and real orthogonal direct-owner normalizer similarity; each L_i commutes R exactly" + }, + "cube_tuple": [ + 0, + 0, + 0 + ], + "environment_metadata": { + "program_container_bytes": 1414847, + "program_container_sha256": "dd9d0ecae4aebbef05c8134f1772221c97d2bf818e7a2f464501dbfa9c2856c0" + }, + "helpers": 0, + "logical_growth": { + "max_scalar_denominator_exponent": 4, + "proof": "Each reader retains its own v plus76 distinct independent u terms:12 magnitudes1/4 and64 magnitudes1/16. Sources unchanged; all physical charts/wrappers unitary.", + "reader_max_row_l1": "8", + "source_max_row_l1": "1" + }, + "mutation_controls": { + "missing_actual_ADD_changes_independent_endpoint": true, + "same_tableau_phase_i_rejected": true, + "wrong_parity_common_chart_transport_rank": 2 + }, + "new_kappa": false, + "normalized_endpoint": "F_K=diag(D,D) L(C_K Q^-1), C_K=diag(L_i^-1) K_odd diag(L_i), D=C_[1,25), Q=C_0", + "normalized_entry": "All original x_i,y_i arbitrary independent at physical ground; all virtual-Q source-line entry wrappers are emitted ordinary monomials.", + "ordinary_literal_profile": { + "ADD": 38912, + "D": 7680, + "P": 7680, + "X": 3072, + "phase": 3072 + }, + "original_main_inputs": 1024, + "owned_fields": 0, + "paid_path_applications": 2048, + "paid_profile": { + "15": 512, + "16": 512, + "8": 512, + "9": 512 + }, + "phase_compilation": { + "all_positive_widths": "literal one-copy phases tensor lift; phase opcode theta becomes i^(f theta); owner scalar coefficients applied once", + "all_wrappers_monomial": true, + "low_rank_sparse_peak_support": 512, + "native_full_conjugate_analytic_anchors": 514, + "reader_output_wrappers": 512, + "source_input_wrappers": 512 + }, + "reader_endpoint": "D(y_i+sum_j K_odd[i,j] L_i^-1 L_j Q^-1 x_j)", + "reader_fields": 512, + "schema": "odd-E8-K-normalized-native-rootcase/v1", + "scientific_program_payload_sha256": "98941b295d428462b82dae52a369de97dcbf5be1dd7a369f6c495cda5fc6ac8a", + "scope": "Whole local block-diagonal K native constructor, with phase-complete emitted cube instance and generic forall2744 proof plus independent all-family geometry. It does not implement H, install F3, close any outer caller, admit precision/work/storage, or improve kappa.", + "source_endpoint": "D x_i on every independent original source x_i", + "source_fields": 512, + "source_pins": { + "NORMALIZERS.json": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da", + "clifford_exact.py": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + }, + "status": "PASS_PHASE_COMPLETE_K_NATIVE_ROOTCASE_AND_GENERIC_FAMILY_TEMPLATE" +} diff --git a/research/programmable-native-stage/native/vendor/K-PROGRAM.json.gz b/research/programmable-native-stage/native/vendor/K-PROGRAM.json.gz new file mode 100644 index 0000000000..86a14df78e Binary files /dev/null and b/research/programmable-native-stage/native/vendor/K-PROGRAM.json.gz differ diff --git a/research/programmable-native-stage/native/vendor/PROOF.md b/research/programmable-native-stage/native/vendor/PROOF.md new file mode 100644 index 0000000000..70d56ae3ff --- /dev/null +++ b/research/programmable-native-stage/native/vendor/PROOF.md @@ -0,0 +1,326 @@ +# A complete native K primitive for every odd-E8 product cube + +This constructs the whole block-diagonal three-factor K service, including +the ordinary wrappers that normalize its actual supplied-line interface to +arbitrary ground-chart inputs. It does not produce the cross-cube H service, +install the low-rank F3 decoder, complete an outer caller or claim a kappa. + +The construction is a fixed finite structured word for all 14^3 cubes. +`core.calculate((a,b,c))` emits its exact literal instance for any cube. +The default finite phase replay fully emits cube(0,0,0); it does not pretend +to have expanded all 106,774,528 scalar ADDs or executed every phase instance. +The all-family result follows from the generic frame/phase proof below and +the independent all-2,744-cube geometry checks in `family_geometry.py`. + +Credits remain with Ali Romman's #5439 odd-E8 geometry, the P112/E8 data, +the PR5464 polarized native phase tools, the original native/Clifford +compiler lineage, and the coded-native-caller real centralizing normalizers. +This assembly and its explicit whole-K contract used substantial OpenAI +Codex assistance. New material is Apache-2.0. No independent human or +proof-kernel acceptance is asserted. + +## 1. Actual fields, scalar coefficients and global coordinates + +The pinned NORMALIZERS data supply 112 distinct binary q labels and their +root columns. The roots split into fourteen eight-root sign cubes. For a +cube b, put B_b=M_b M_b^T/4 and K_b=I-B_b. Exact rational checks give +K_b^2=I; each row has four entries +-1/2, all joining opposite selector +parities. The two four-port classes each span a three-space with pairing +rank one, and the two three-spaces are orthogonal. + +A product cube has 512 owners. Define + + K_odd=(K1+K2+K3-K1 K2 K3)/2. + +The three factor matrices commute and square to I. Expanding the square +of their displayed majority polynomial gives I. The scalar K_odd is also +symmetric. Every row has twelve distinct one-factor entries of magnitude +1/4 and sixty-four distinct three-factor entries of magnitude 1/16. +The two support sets are disjoint since each K_b has zero diagonal. +Every nonzero entry reverses total selector parity. Thus each row has +exactly 76 nonzero coefficients and their absolute sum is seven. + +The actual product labels are concatenated triples in F2^27. Their global +span U is the 25-space of equal three-block parities. The code records an +explicit orthonormal basis of U, and takes physical coordinates by dotting +against it. This is one global I25 realization, shared by all cubes; no +local-20-to-global-25 free adapter is introduced. Every port has norm one +and differs from the characteristic vector of U. The latter is the raw +all-ones27 vector, whereas each base label has weight three or seven. + +For every product cube the two 256-port parity classes span S0,S1 with + + dim S0=dim S1=9, S0 perpendicular S1, + rank(B|S0)=rank(B|S1)=1, dim rad(S0)=dim rad(S1)=8. + +Their joint span has dimension ten. `family_geometry.py` checks all +1,404,928 actual norm-one noncharacteristic labels, all 5,488 nine-space +classes and all opposite-reader/source-basis incidences. The restricted +characteristic issue is explicit: every odd q represents the characteristic +functional within S9. The construction never requires a noncharacteristic +vector inside S9, and never tries to orthonormalize this degenerate S9. + +Use two independent fields X_p,Y_p per port p. There are no other independent +fields, no owned full-field scratch, no COPY and no CLEAR. Across the family +the product cubes partition the actual owner indices, so no independent +input is duplicated or identified between cube instances. + +## 2. Canonical frames for arbitrary degenerate subspaces + +All operator products below act rightmost first. The primitive convention is + + C_q=((1+i)I+(1-i)X_q)/2. + +Write R=C_[0,25), Q=C_0 and D=C_[1,25), so R=DQ. If the columns of G are +any full binary basis and A=G^-1, put + + K_G=D_J P_G, J=I+A^T A. + +Here the diagonal uses the retained compiler's Z4 quadratic convention. +For the first r columns spanning S, the actual native frame is + + Phi_(G,r)=K_G C_[0,r) K_G^-1. + +It is not necessary for the restricted form on S to be nondegenerate. +Its binary symplectic action sends the Z Lagrangian to + + L_S={(x,z): x in S and z+x in S-perp}. + +To check this directly, let B=G P_r G^T. On a Z input z the output X part +is x=Bz, and its Z part is z+JBz. Since J=I+G^-T G^-1, the vector formed +by adding x to that output Z part is z+G^-T G^-1 x. Its dot product with +every first-r basis column vanishes. Dimensions give exactly L_S. +The symplectic action of C, and therefore of Phi, is an involution; +the inverse frame has the same Lagrangian image. + +Consequently two constructions of the same S differ by a monomial map. +If S is contained in T, their transition has Gaussian rank + + 25-dim(L_S intersect L_T)=dim T-dim S. + +Indeed their intersection has x in S and z+x in T-perp, hence dimension +dim S+25-dim T. This proves all required rank and zero-rank statements +for every actual cube, not only for the root instance's tableaux. + +## 3. Literal source and reader paths + +Fix a source parity class S9. All sources in it and all opposite readers +will meet at one and the same literal canonical Phi_S9 word. Each source +q belongs to S9. Its line-to-S9 path costs H8. To emit this path, choose +a full flag whose first vector is q and first nine vectors span S9. +Monomial gauges connect its one- and nine-dimensional frames to the +declared canonical frames, and the only Gaussian child is C_[1,9). + +A reader q is orthogonal to S9 and has norm one. Therefore it is outside +S9 and its q-perp24 contains S9. The reader starts at ground, reaches +Phi_S9 by one H9, and leaves it by one H15 to a full flag beginning with +the identical ordered S9 basis and spanning that actual q-perp24. +The emitted word supplies every reader's actual endpoint flag. + +The source leaves S9 for canonical full R by one H16. Let + + T_G=R K_G R^-1. + +The source-exit word executes K_G^-1, then C_[9,25), then T_G, since + + R Phi_S9^-1=T_G C_[9,25) K_G^-1. + +No extra Gaussian is hidden in T_G; its exact monomial phase is given +in section 4. All other gauges are compiled as P/D/X/phase-only words. + +At the common cut, directly execute Y_r += K_odd[r,s] X_s for every +nonzero scalar coefficient. The two main banks are independent. X is +never modified by these ADDs, so every source read uses its original +geometric logical value. Every reader retains its arbitrary old value +with coefficient one. There is no need for a rank-one cache or any +owned helper, even though the scalar matrix between the classes is full +rank. The two parity directions use disjoint source/reader field sets +and are executed separately. Every ADD is at an actually identical frame, +not merely between containing or cross-orthogonal subspaces. + +The geometric endpoint is exactly + + X_s: Phi_[q_s] u_s -> R u_s, + Y_r: v_r -> Phi_(q_r-perp)(v_r+sum_s K_odd[r,s]u_s). + +Every 512-port cube thus uses 512 children of each of widths 8,9,15,16, +and 38,912 ordinary scalar ADDs, with no helper or owned field. + +## 4. Absolute phases without exponential dense columns + +The retained signed tableau fixes a Clifford operator up to scalar. +Every low-rank monomial gauge is checked with an exact sparse +Gaussian-integer zero-column evaluation that fixes this scalar as well. +For same-S9 gauges the sparse support remains at most 512: after changing +coordinates, both rank-nine Gaussian portions act inside the same prefix. +The normalization gauges below need at most two one-axis Gaussians. + +For any native full basis G, let a_j=G^-1 e_j and set + + d_j=floor(wt(a_j)/2) mod 2. + +If q_J is the diagonal's actual Z4 phase, XOR Hamming-weight expansion +modulo four gives + + q_J(y)+wt(G^-1 y)=wt(y)+2d.y mod4. + +The quadratic cross terms cancel. For each j, its remaining linear +coefficient is alpha_j+wt(a_j), with alpha_j=(1+wt(a_j)) mod2 in {0,1}; +this equals 1+2d_j modulo four. With a=(1-i)/2, + + R^-1|0>=a^25 sum_x i^wt(x)|x>, + K_G R^-1|0>=Z_d R^-1|0>, + T_G|0>=(-i)^wt(d)|d>. + +Furthermore T_G is monomial: R^-1 takes Z Paulis to the diagonal +Lagrangian {(z,z)}, K_G takes it to {(Gz,Gz)}, and R takes it back to +Z Paulis. Its exact signed tableau plus this absolutely normalized +column determines the emitted P/D/X/phase word universally. No 2^25 +state is allocated. `frame_tools.py` retains this analytic anchor. + +These generic arguments prove the compiler construction for every cube +and every flag satisfying the verified geometry. Default execution fully +corroborates all actual root-case gauges, including 512 reader-output +full-basis anchors, rather than sampling a few field pairs. + +## 5. Real normalizers and virtual-Q entry + +The geometric input line service above is not silently assumed free in +the normalized native F_K. We explicitly wrap arbitrary ground inputs. +For each physical q, construct an orthogonal binary G_i taking e0 to q. +If q_0=0 use the even transvection T_(e0+q). Otherwise choose j>0 with +q_j=0 and use T_(ej+q) T_(e0+ej). Such j exists because q is not the +ambient characteristic vector. + +For row j of G_i put z_j=(wt(row_j)-1)/2 modulo two and define + + L_i=Z_z P_Gi. + +This is a real signed orthogonal monomial. Orthogonality cancels every +quadratic cross coefficient in the weight identity + + wt(G_i^-1 x)-wt(x)=2z.x mod4. + +It follows that L_i R L_i^-1=R exactly, including absolute phase. +Checking orthogonality and the 25 linear coefficients proves the weight +identity for all 2^25 addresses; no address sampling is used. + +The actual ordinary normalized wrappers are + + input X: Phi_[q_i] L_i Q^-1, + input Y: L_i, + output X: L_i^-1, + output Y: D L_i^-1 Phi_(q_i-perp)^-1. + +Their monomiality follows from the corresponding line/hyperplane +Lagrangian incidences. Input X's literal defining word has two one-axis +Gaussian factors and is compiled with exact sparse absolute phase. +It is emitted and executed as an ordinary monomial; Q^-1 is virtual +inside this identity, not an additional unpriced Gaussian instruction. + +For the potentially high-rank reader-output wrapper let its endpoint +flag be Phi_V=K_v C_[0,24) K_v^-1. The exact low-rank expression is + + D L_i^-1 Phi_V^-1 + =Q^-1 L_i^-1 T_v C_24 K_v^-1, + T_v=R K_v R^-1. + +This follows by C_[0,24)^-1=R^-1 C_24 and [L_i,R]=0. The right side +has only two one-axis Gaussian factors plus phase-complete monomials. +Its signed tableau is checked against the defining left side, and its +absolute phase is compiled from the low-rank expression. Thus no +rank-24 dense zero column is needed and no projective phase is discarded. + +## 6. Normalized arbitrary-input endpoint + +Let x_i,y_i be the actual independent ground inputs. After input wrappers +the geometric logical values are exactly + + u_i=L_i Q^-1 x_i, v_i=L_i y_i. + +These are invertible functions of the original independent inputs; they +are not being renamed originals or assumed zero. The actual emitted +input-X monomial already puts its physical field at Phi_[q_i]u_i. + +Source output followed by its wrapper is + + L_i^-1 R L_i Q^-1 x_i = D x_i. + +Reader output followed by its wrapper is + + D y_i + sum_j K_odd[i,j] D L_i^-1 L_j Q^-1 x_j. + +Define, at actual field width f, + + (C_K,f)_ij=K_odd[i,j] L_i,f^-1 L_j,f. + +The complete normalized operator is therefore + + F_K=diag(D,D) L(C_K Q^-1). + +K_odd is a real symmetric involution and the L_i are real orthogonal. +Thus C_K^T=C_K, C_K^2=I and [C_K,R]=0. These facts follow by actual +operator similarity. They do not tensor the whole owner matrix: +scalar K_odd coefficients are applied once, and cancellation of adjacent +L_j,f L_j,f^-1 proves the square identity at every positive width. + +All 1,024 geometric original columns are explicitly interpreted in the +root-case word; the incoming-column and outgoing-row factor identities +above imply all 38,912 nonzero normalized operator blocks at once. No +sampling of cross-owner physical operators is used. + +The normalized source outputs are autonomous rank-24 D transforms of +their original inputs. Reader outputs remain the specified triangular +coupled transforms. The service is invertible and retains every original +input; a complete outer Gaussian caller and its larger productive jobs +must still be supplied before using any whole-caller target profile. + +## 7. All positive widths and complete local accounting + +Every single-copy identity includes its absolute phase. Tensor it +columnwise to f positive address columns. P and X lift as binary block +maps, D sums its Z4 phase over the columns, and a single-copy phase theta +becomes i^(f theta). Scalar owner coefficients are applied once per field. +No width-one sum relation has been extrapolated by taking a tensor power +of a sum. This proves the actual physical word and F_K endpoint for every f. + +The normalized root case has 512 fields of each X/Y role and profile + + paid {8:512,9:512,15:512,16:512}, + ordinary {ADD:38912,P:7680,D:7680,X:3072,phase:3072}. + +There are 42 literal monomial primitives and 76 scalar ADDs per owner, +in addition to its four correctly charged Gaussian paths. These are +nonrecursive work, not zero-work operations. Their address movement, +storage, precision and tape price remain eventual caller obligations. +No helper input, helper target, owned field, COPY or CLEAR is introduced. + +For v=112^3=1,404,928, concatenate the cube words in lexicographic order. +The whole-family profiles are + + paid {8:v,9:v,15:v,16:v}, + ordinary {ADD:76v,P:15v,D:15v,X:6v,phase:6v}. + +The number of actual main inputs is 2v=2,809,856. The Gaussian rank mass +is 48v. No smaller pairing rank is substituted for any physical child. + +At geometric logical opcode boundaries each source row has l1 one and +each reader has its old value plus distinct source coefficients of total +l1 seven. Hence all prefix row l1 values are at most eight, and scalar +denominator exponent is at most four. Physical charts and wrappers are +unitary, so independent input norm at most M gives field norms at most +M for sources and 8M for readers. This is a finite local growth constant, +not a complete recursive rounding-error, precision or outer-admission bill. + +Actual mutation controls detect a global phase i despite an identical +signed tableau, a wrong parity S9 frame (requiring rank-two transport), +and omission of a literal K ADD (changing an independent input column). + +## 8. Remaining scope + +This fills the local K-native construction gate. It does not provide H, +remove H by a global basis change, make the F3 factor totals freely +available, prove a decoder/reader chronology, or close the mixed-Q +E=I-H interface. No whole-caller profit or kappa improvement is claimed. +The earlier planning profile and separated-helper obstruction cannot +be reused as a completed budget for this changed primitive. diff --git a/research/programmable-native-stage/native/verify_intertwiners.py b/research/programmable-native-stage/native/verify_intertwiners.py new file mode 100644 index 0000000000..3c39c1cdf3 --- /dev/null +++ b/research/programmable-native-stage/native/verify_intertwiners.py @@ -0,0 +1,73 @@ +#!/usr/bin/env python3 +"""Exact finite controls for the accompanying universal algebraic proof.""" +import json +P=65537 +IROOT=256 + +def need(ok,msg): + if not ok: raise ValueError(msg) +def eye(n): return [[int(i==j) for j in range(n)] for i in range(n)] +def scale(A,c): return [[x*c%P for x in row]for row in A] +def mul(A,B): + n=len(A);C=[[0]*n for _ in range(n)] + for i,row in enumerate(A): + for k,a in enumerate(row): + if a: + for j,b in enumerate(B[k]): + C[i][j]=(C[i][j]+a*b)%P + return C +def block(A,B,C,D):return [a+b for a,b in zip(A,B)]+[c+d for c,d in zip(C,D)] +def diag(A,B): + z=[[0]*len(A)for _ in A];return block(A,z,z,B) +def shear(A,lower=False): + I=eye(len(A));z=scale(I,0) + return block(I,z,A,I)if lower else block(I,A,z,I) +def gaussian(bits,axis): + n=1<>j)&1)else x^1^(1<1:need(mul(Cs[0],Cs[1])!=mul(Cs[1],Cs[0]),'noncommuting code control') + tests+=4 + print(json.dumps({'status':'PASS','exact_controls':tests,'modulus':P,'universal_evidence':'INTERTWINER-PROOF.txt','new_kappa':False},sort_keys=True)) +if __name__=='__main__':main() diff --git a/research/programmable-native-stage/precision/COMPOSITION.txt b/research/programmable-native-stage/precision/COMPOSITION.txt new file mode 100644 index 0000000000..6a67942de0 --- /dev/null +++ b/research/programmable-native-stage/precision/COMPOSITION.txt @@ -0,0 +1,64 @@ +A compositional sufficient exact-grid theorem for emitted dyadic callers + +This applies to a finite, fully specified circuit whose operations are ordinary +monomial words, exact dyadic scalar ADDs, and the source Gaussian children. It +is an arithmetic-format theorem. It does not admit an unimplemented caller or +charge a native child as ordinary work. + +Fix positive field-column width f and an initial grid 2^-g Z[i]. For each +original field v set b_v=g. Process the literal circuit in chronological order: + + monomial(v): b_v is unchanged; + Gaussian(rank r, v): b_v <- b_v + ceil(r f/2); + ADD(v <- v + c u), c=m/2^t with integer m and t>=0: + b_v <- max(b_v,b_u+t). + +At every prefix, each real and imaginary component of v lies in 2^-b_v Z. +The maximum of all prefix exponents is one sufficient common exact grid. +Negative m, zero coefficients, reused sources, and arbitrary dirty initial +values are allowed. Independent initial values are not replaced by zeros. + +Proof by chronological induction. A monomial permutes coordinates and +multiplies by Gaussian units. A scalar ADD sends the sum of two stated lattices +into the lattice with the larger exponent. A rank-r child is the tensor product +of r f one-axis Gaussian transforms. For k independent axes its coefficients +are Gaussian integers divided by 2^ceil(k/2), by the Gaussian-integer lemma in +PROOF.txt. This proves the update and covers intermediate butterfly stages as +well as child outputs. Taking a maximum covers all prefixes. No statistical +error estimate or rounding hypothesis occurs. + +The b_v values equal longest dependency-path weights in a directed acyclic +version of the emitted circuit: a Gaussian step has weight ceil(r f/2), a +scalar source edge has weight t, and unchanged-value edges have weight zero. +Consequently, if every path has total Gaussian rank at most R, at most s +Gaussian steps of odd rank, and scalar denominator-exponent sum at most T, +then + B = g + ceil(R f/2) + s + T +is sufficient. This deliberately loose bound follows from +sum_j ceil(r_j f/2) <= ceil((sum_j r_j) f/2) + s. +For a fixed finite template, R,s,T are constants independent of f, so B=O(f). +The source-bound verifier supplies the substantially sharper bounds for the +actual whole-K forward and backward words rather than this loose estimate. + +Magnitude bookkeeping is also constructive. Attach the polynomial 1 in +u=2^(f/2) to every input field. A monomial leaves it unchanged; a rank-r child +multiplies it by u^r; ADD with coefficient c replaces the target polynomial by +its old polynomial plus |c| times the source polynomial. Every physical prefix +has complex component magnitude at most H times its polynomial evaluated at u, +by the triangle inequality and the exact Gaussian row norm u^r. If all such +polynomials have degree at most d and coefficient sum at most A>=1, then all +prefixes have magnitude at most A H 2^ceil(d f/2). A signed numerator format of + + B + ceil(d f/2) + ceil(log2(A H)) + 4 + +bits is sufficient with conservative temporary-sum headroom. This bound is +linear in f for a fixed caller and fixed input-height bound. The arithmetic +cost of exact divisions, address maps, data movement and Gaussian evaluation +remains explicit; this theorem does not provide a constant-word or asymptotic +running-time shortcut. + +Credit and source convention: PR 5464, head +3981f9539e63630681f6903e3c6a50b3a0d2f2dd, for the actual whole-K native +programs and Gaussian convention; the tensor coefficient and lattice arguments +are elementary. The source-bound specialization and compositional statement +were prepared with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/programmable-native-stage/precision/PROOF.txt b/research/programmable-native-stage/precision/PROOF.txt new file mode 100644 index 0000000000..7fb69ca0bc --- /dev/null +++ b/research/programmable-native-stage/precision/PROOF.txt @@ -0,0 +1,61 @@ +Exact all-width dyadic precision for the actual whole-K native primitive + +Positive result. For the forward and backward whole-K programs pinned below, every field component can be evaluated with ZERO rounding error on one explicitly bounded dyadic grid, at every positive field-column width f. Both orientations admit the common sufficient fractional-bit budget + B = g + ceil(25 f/2) + 4. +Here input real and imaginary components lie in 2^-g Z. If initial complex component magnitudes are at most H>=1, every prefix has magnitude at most + 8 H 2^ceil(25 f/2). +A signed payload of g+2 ceil(25 f/2)+ceil(log2 H)+9 bits is sufficient, including conservative guard bits for temporary sums. This is a source-bound sufficient format theorem, not a minimal-grid claim, new kappa, or uncharged runtime theorem. + +For bounded integer/dyadic input amplitudes this format is linear in f. At g=0,H<=15 it fits within 25f+14 signed bits. The full whole-K family has 2*112^3 fields of 2^(25f) physical components; its positive signed address space already needs at most 25f+23 bits before additional caller scratch. Thus this local primitive's exact payload budget does not require asymptotically wider words than its physical address space. This statement does not assert that constant 64-bit words suffice for growing f or that address transformations cost one instruction. + +1. Frozen actual source and scope. +The source is PR 5464 head 3981f9539e63630681f6903e3c6a50b3a0d2f2dd, research/odd-e8-whole-k-native/K-PROGRAM.json.gz and B-PROGRAM.json.gz. Their immutable container and decompressed payload hashes are checked against SOURCES.json. The forward stream has 43,008 events; the backward stream has 44,544, including 1,536 explicit boundary monomials. Each uses 512 Gaussian children of every rank 8,9,15,16, 38,912 scalar ADDs and all source-declared monomial wrappers. Both root-cube streams have 1,024 arbitrary original fields. The checker examines every referenced phase/permutation word and rejects an unrecorded non-monomial operation. + +The all-family geometry/phase theorem belongs to the source. Our symbolic proof applies to each constructor instance because all instances have the same field-path ranks, signed coefficient magnitudes and chronology. We do not claim to have rerun every all-family absolute phase instance or the entire upstream scientific suite. The checker replays the two actual pinned root-cube streams as independent evidence for the precision bounds. + +2. Gaussian-integer coefficient lemma. +Use the source convention + C=((1+i) I+(1-i) X)/2. +For m independent bit axes, every nonzero entry of C tensor ... tensor C is + (1+i)^(m-h) (1-i)^h / 2^m + = (-i)^h (1+i)^m / 2^m. +If m=2s, (1+i)^m=2^s i^s. If m=2s+1 it equals 2^s i^s(1+i). Hence every entry is a Gaussian integer divided by 2^ceil(m/2). Conjugation gives the same bound for inverse children. Literal phase, signed translation and binary permutation gates multiply components by Gaussian units and permute their addresses, so they introduce no denominator. + +A rank-r child over f columns acts on r f independent axes. It therefore increases a sufficient dyadic denominator exponent by at most ceil(r f/2), rather than r f. This also covers intermediate butterfly stages: after k independent axes the same lemma gives ceil(k/2)<=ceil(rf/2). Computing with a fixed common grid does not require rounding at hidden intermediate steps; the exact mathematical lattice bound proves the corresponding integer numerators are divisible before a power-of-two division is performed. + +3. Literal forward grid. +Every source X first traverses rank 8; its initial grid exponent becomes g+4f. Every reader Y first traverses rank 9; its exponent becomes g+ceil(9f/2). Each actual ADD uses a source X at its rank-8 cut and coefficient of denominator at most 16. No source X is changed by any such ADD. Thus after all ADDs a reader lies on the grid with exponent + g+max(ceil(9f/2),4f+4). +Readers then traverse rank 15. Sources traverse rank 16, so every forward prefix and output is covered by + B_F = g+max(ceil(9f/2)+ceil(15f/2), + 4f+ceil(15f/2)+4, + 12f). +The third term is redundant but displays the source path. Repeated ADDs at a fixed grid do not accumulate denominator bits: their exponent is a maximum, not a sum. This is why the result has no factor from 38,912 ADDs or the number of ports. + +4. Literal backward grid. +The actual inverse-transpose program reverses ADD direction, with all native inverse children represented by positive Gaussian children and explicit monomials. Source Y reaches its rank-9 cut with exponent g+ceil(9f/2). An X field, initially at its rank-8 cut, receives signed dyadic multiples of these Y values and then traverses rank 16. Therefore + B_B = g+8f+ceil(9f/2)+4 + = g+ceil(25f/2)+4 +is sufficient for every backward prefix. Its other original fields follow rank 9 plus rank 15 and are covered by this bound. Directly considering even and odd f shows B_F<=B_B for every f>=1. The verifier independently carries symbolic affine envelopes for f=2k and f=2k+1, on their full unbounded integer domains. Sample widths are illustrations; universal validity is not inferred by finite sampling. + +5. Amplitude and integer payload bounds. +A rank-r Gaussian child has exactly 2^(rf) entries of magnitude 2^(-rf/2) per row, so its induced maximum-component norm is 2^(rf/2). Monomial words preserve component magnitudes. Each scalar K row has twelve coefficients of magnitude 1/4 and sixty-four of magnitude 1/16, with total absolute sum seven; each reader/source also retains its own old value with coefficient one. + +In the forward stream, each X bound evolves through exponents 8 and 16, giving at most H 2^(12f). Each Y bound, after its ADDs and rank-15 exit, is at most H(2^(12f)+7*2^(23f/2)). Thus all forward prefixes are bounded by 8H2^(12f). + +In the backward stream the ADDs instead put Y's rank-9 values into X before rank 16. This gives the bound H(2^(12f)+7*2^(25f/2)); the unchanged Y path remains below H2^ceil(24f/2). Every prefix is therefore bounded by 8H2^ceil(25f/2). The checker proves these bounds by positive polynomials in u=2^(f/2): no polynomial has degree above 25 or coefficient sum above eight. + +Multiplying this magnitude bound by the common denominator 2^B bounds the integer numerator. The stated signed payload length leaves conservative headroom for the real/imaginary temporary sums used by C and dyadic ADDs. No multiplication of two unrestricted payload words is needed for these particular linear gates: coefficients are Gaussian units and dyadic scalars. + +6. What this establishes and what is still charged. +This supplies an actual local ordinary finite-precision realization: exact Gaussian-integer/dyadic arithmetic has zero rounding error with the specified format, and the source's original data/frame/owned contracts remain unchanged. Integer division by powers of two, carry handling, permutations, address-bit calculations, storage and movement still have to be implemented and charged on the chosen ISA. A direct butterfly implementation is finite but is not thereby faster than the intended recursive supplier. Our word-width bound is not a claim of unit-cost arbitrary precision, nor does it supply the entire ordinary conversion or analytic integer-multiplication theorem. + +A complete caller may compose these bounds with its own actual ADDs, recodings and native children. The present note does not hide that missing composition inside an assumed residual gadget. It makes no replacement of the selected paid profile or selected frontier. + +Reproduce with Python 3.12+, standard library only: + python -B verify.py + python -O -B verify.py + +A mutation increases the denominator of a real emitted scalar edge; it is rejected by the universal grid test. + +Credit. THU New Media Research Center / thu-nmrc supplies PR 5464's actual whole-K geometry, field chronology, literal phases, forward/backward words and retained source lineage. Ali Romman's PR 5439 supplies the odd-E8 geometry; Dugongue PR4929 and Dillon Amburgey supply retained code/normalizer work; Cao Yifan, Cinna Davis, zxv, Jacob Alan Sussman and the native/Clifford/compiler predecessors retain their source credit. Matarener's PR 5438 and the Clifford denominator literature demonstrate why exact grids must be separated from crude height bounds. The Gaussian-integer coefficient identity is elementary and classical. This exact format/size specialization and symbolic precision checker were prepared with substantial OpenAI Codex assistance. Original work is Apache-2.0. diff --git a/research/programmable-native-stage/precision/RESULT.json b/research/programmable-native-stage/precision/RESULT.json new file mode 100644 index 0000000000..35a00af5fe --- /dev/null +++ b/research/programmable-native-stage/precision/RESULT.json @@ -0,0 +1,163 @@ +{ + "status": "PASS_WHOLE_K_UNIVERSAL_EXACT_DYADIC_PRECISION", + "forward": { + "events": 43008, + "event_counts": { + "MONOMIAL": 2048, + "PAID_PATH": 2048, + "ADD": 38912 + }, + "paid": { + "8": 512, + "9": 512, + "16": 512, + "15": 512 + }, + "conservative_grid_upper_envelope": [ + [ + 23, + 4 + ], + [ + 24, + 0 + ] + ], + "sufficient_grid_envelope": [ + [ + 23, + 4 + ], + [ + 24, + 0 + ] + ], + "magnitude_polynomial_degree": 24, + "magnitude_polynomial_coefficient_sum_upper": "8", + "all_original_fields": 1024, + "coarse_grid_bound_samples": { + "1": 27, + "2": 50, + "3": 73, + "4": 96, + "8": 192, + "16": 384, + "32": 768 + }, + "scope": "All positive f symbolic sufficient dyadic grid and component magnitude, conditional only on the source stream exact native semantics; not machine/recursive cost.", + "phase_permutation_word_definitions_checked": 4102, + "tight_gaussian_integer_grid_by_parity": [ + { + "f_parity": 0, + "k_minimum": 1, + "relative_grid_envelope_in_k": [ + [ + 23, + 4 + ], + [ + 24, + 0 + ] + ], + "variable": "f=2*k+parity" + }, + { + "f_parity": 1, + "k_minimum": 0, + "relative_grid_envelope_in_k": [ + [ + 23, + 16 + ], + [ + 24, + 13 + ] + ], + "variable": "f=2*k+parity" + } + ] + }, + "backward": { + "events": 44544, + "event_counts": { + "BOUNDARY_MONOMIAL": 1536, + "MONOMIAL": 2048, + "PAID_PATH": 2048, + "ADD": 38912 + }, + "paid": { + "8": 512, + "9": 512, + "16": 512, + "15": 512 + }, + "conservative_grid_upper_envelope": [ + [ + 25, + 4 + ] + ], + "sufficient_grid_envelope": [ + [ + 25, + 4 + ] + ], + "magnitude_polynomial_degree": 25, + "magnitude_polynomial_coefficient_sum_upper": "8", + "all_original_fields": 1024, + "coarse_grid_bound_samples": { + "1": 29, + "2": 54, + "3": 79, + "4": 104, + "8": 204, + "16": 404, + "32": 804 + }, + "scope": "All positive f symbolic sufficient dyadic grid and component magnitude, conditional only on the source stream exact native semantics; not machine/recursive cost.", + "phase_permutation_word_definitions_checked": 4105, + "tight_gaussian_integer_grid_by_parity": [ + { + "f_parity": 0, + "k_minimum": 1, + "relative_grid_envelope_in_k": [ + [ + 25, + 4 + ] + ], + "variable": "f=2*k+parity" + }, + { + "f_parity": 1, + "k_minimum": 0, + "relative_grid_envelope_in_k": [ + [ + 25, + 17 + ] + ], + "variable": "f=2*k+parity" + } + ] + }, + "common_grid_bits": "g+ceil(25*f/2)+4", + "common_complex_magnitude_upper": "8*H*2^ceil(25*f/2)", + "sufficient_signed_payload_bits": "g+2*ceil(25*f/2)+ceil(log2(H))+9, for H>=1", + "required_rounding_error": "zero when the stated exact dyadic storage and arithmetic are used", + "mutations": [ + "increased actual scalar denominator rejected" + ], + "not_claimed": [ + "new kappa", + "all-family emitted phase replay", + "whole caller budget", + "constant 64-bit word size for growing f", + "unit-cost arbitrary precision", + "native kernel proof verification" + ] +} diff --git a/research/programmable-native-stage/precision/SOURCES.json b/research/programmable-native-stage/precision/SOURCES.json new file mode 100644 index 0000000000..65b592353f --- /dev/null +++ b/research/programmable-native-stage/precision/SOURCES.json @@ -0,0 +1,22 @@ +{ + "files": [ + { + "orientation": "forward", + "package_path": "source/K-PROGRAM.json.gz", + "source": "research/odd-e8-whole-k-native/K-PROGRAM.json.gz", + "revision": "3981f9539e63630681f6903e3c6a50b3a0d2f2dd", + "sha256": "dd9d0ecae4aebbef05c8134f1772221c97d2bf818e7a2f464501dbfa9c2856c0", + "payload_sha256": "98941b295d428462b82dae52a369de97dcbf5be1dd7a369f6c495cda5fc6ac8a", + "url": "https://github.com/thu-nmrc/integer-mult-bounds/blob/3981f9539e63630681f6903e3c6a50b3a0d2f2dd/research/odd-e8-whole-k-native/K-PROGRAM.json.gz" + }, + { + "orientation": "backward", + "package_path": "source/B-PROGRAM.json.gz", + "source": "research/odd-e8-whole-k-native/B-PROGRAM.json.gz", + "revision": "3981f9539e63630681f6903e3c6a50b3a0d2f2dd", + "sha256": "fd30f46e210e4f46302fbeb4055a0e61aa5dce1268a864b53db58406be5a2ed9", + "payload_sha256": "f6b26f28f2a8f2dcfbf81f98c7ca18f967384b7b61518766494f8e821d5bf56f", + "url": "https://github.com/thu-nmrc/integer-mult-bounds/blob/3981f9539e63630681f6903e3c6a50b3a0d2f2dd/research/odd-e8-whole-k-native/B-PROGRAM.json.gz" + } + ] +} diff --git a/research/programmable-native-stage/precision/source/B-PROGRAM.json.gz b/research/programmable-native-stage/precision/source/B-PROGRAM.json.gz new file mode 100644 index 0000000000..6651986b9f Binary files /dev/null and b/research/programmable-native-stage/precision/source/B-PROGRAM.json.gz differ diff --git a/research/programmable-native-stage/precision/source/K-PROGRAM.json.gz b/research/programmable-native-stage/precision/source/K-PROGRAM.json.gz new file mode 100644 index 0000000000..86a14df78e Binary files /dev/null and b/research/programmable-native-stage/precision/source/K-PROGRAM.json.gz differ diff --git a/research/programmable-native-stage/precision/verify.py b/research/programmable-native-stage/precision/verify.py new file mode 100644 index 0000000000..c38862f6df --- /dev/null +++ b/research/programmable-native-stage/precision/verify.py @@ -0,0 +1,131 @@ +"""All-width exact dyadic grid/size bounds from the actual whole-K streams. +No recursive-tariff, whole-caller, or new kappa claim. Apache-2.0. +""" +from pathlib import Path +from fractions import Fraction as Q +from collections import Counter +import gzip,hashlib,json + + +def need(ok,message): + if not ok:raise ValueError(message) + + +def dominated(a,b): + """Affine a*f+b no greater than the other at every integer f>=1.""" + return a[0]<=b[0] and sum(a)<=sum(b) + + +def envelope(lines): + lines=set(lines) + return {x for x in lines if not any(y!=x and dominated(x,y) for y in lines)} + + +def check_monomials(stream): + definitions=stream['definitions'];used=set() + for event in stream['program']: + if event[0] in ('MONOMIAL','BOUNDARY_MONOMIAL'):used.add(event[3]) + elif event[0]=='PAID_PATH':used|={event[-1]['before_monomial'],event[-1]['after_monomial']} + need(used<=definitions.keys(),'all word definitions resolved') + for word in (definitions[key] for key in used): + for gate in word: + need(gate[0] in ('P','D','X','phase'),'non-monomial hidden in a phase wrapper') + if gate[0]=='P':need(len(gate[1])==25 and all(type(x)is int and 0<=x<1<<25 for x in gate[1]),'binary address-map shape') + if gate[0]=='D':need(len(gate[1])==len(gate[2])==25 and all(type(x)is int for x in gate[2]),'integral Z4 phase shape') + if gate[0] in ('X','phase'):need(type(gate[1])is int,'integral phase or XOR mask') + for event in stream['program']: + if event[0] in ('MONOMIAL','BOUNDARY_MONOMIAL'):need(event[3] in definitions,'resolved monomial definition') + elif event[0]=='PAID_PATH': + need(event[-1]['before_monomial'] in definitions and event[-1]['after_monomial'] in definitions,'resolved child wrappers') + return len(used) + +def replay(program,ports,backward): + # Exponents measure denominator bits relative to the initial 2^-g grid. + heights={(role,p):{(0,0)} for role in ('X','Y') for p in ports} + # Positive polynomials in u=2^(f/2), multiplied by initial magnitude bound H. + magnitude={(role,p):Counter({0:Q(1)}) for role in ('X','Y') for p in ports} + peak_lines={(0,0)};peak_degree=0;peak_coefficient_sum=Q(1) + counts=Counter();paid=Counter() + for event in program: + op=event[0];counts[op]+=1;target=tuple(event[1:3]) + need(target in heights,'named original owner') + if op in ('MONOMIAL','BOUNDARY_MONOMIAL'):pass + elif op=='PAID_PATH': + spec=event[-1];rank=spec['rank'];need(rank==len(spec['child_axes']) and rank>0,'actual child rank') + heights[target]={(a+rank,b) for a,b in heights[target]} + magnitude[target]=Counter({power+rank:c for power,c in magnitude[target].items()});paid[rank]+=1 + elif op=='ADD': + source=tuple(event[3:5]);need(source in heights and source!=target,'independent owner ADD') + coefficient=Q(event[5],event[6]);den=coefficient.denominator;num=abs(coefficient.numerator) + need(den&(den-1)==0 and num>0,'dyadic nonzero source coefficient') + numerator_twos=(num&-num).bit_length()-1;extra=den.bit_length()-1-numerator_twos + heights[target]=envelope(heights[target]|{(a,b+extra) for a,b in heights[source]}) + for power,c in magnitude[source].items():magnitude[target][power]+=abs(coefficient)*c + else:raise ValueError('unpriced/unbound event '+op) + peak_lines=envelope(peak_lines|heights[target]) + peak_degree=max(peak_degree,max(magnitude[target])) + peak_coefficient_sum=max(peak_coefficient_sum,sum(magnitude[target].values())) + # Simple all-f line certificates; backward exact envelope has one line. + sufficient={(25,4)} if backward else {(24,0),(23,4)} + need(all(any(dominated(line,bound) for bound in sufficient) for line in peak_lines),'universal exact grid bound') + need(peak_degree<=(25 if backward else 24) and peak_coefficient_sum<=8,'universal amplitude bound') + need(paid=={8:512,9:512,15:512,16:512},'complete actual cube paid profile') + return {'events':len(program),'event_counts':dict(counts),'paid':dict(paid), + 'conservative_grid_upper_envelope':sorted(peak_lines),'sufficient_grid_envelope':sorted(sufficient), + 'magnitude_polynomial_degree':peak_degree,'magnitude_polynomial_coefficient_sum_upper':str(peak_coefficient_sum), + 'all_original_fields':len(heights),'coarse_grid_bound_samples':{str(f):max(a*f+b for a,b in peak_lines) for f in (1,2,3,4,8,16,32)}, + 'scope':'All positive f symbolic sufficient dyadic grid and component magnitude, conditional only on the source stream exact native semantics; not machine/recursive cost.'} + + +def tight_grid(program,ports,backward,parity): + # f=2*k+parity; k>=1 for even f, k>=0 for odd f. + minimum_k=1-parity + def dom(a,b):return a[0]<=b[0] and a[0]*minimum_k+a[1]<=b[0]*minimum_k+b[1] + def env(lines): + lines=set(lines);return {x for x in lines if not any(x!=y and dom(x,y) for y in lines)} + heights={(role,p):{(0,0)} for role in ('X','Y') for p in ports};peak={(0,0)} + for event in program: + op=event[0];target=tuple(event[1:3]) + if op=='PAID_PATH': + rank=event[-1]['rank'];heights[target]={(a+rank,b+(rank*parity+1)//2) for a,b in heights[target]} + elif op=='ADD': + coefficient=Q(event[5],event[6]);n,d=abs(coefficient.numerator),coefficient.denominator + extra=d.bit_length()-1-((n&-n).bit_length()-1) + heights[target]=env(heights[target]|{(a,b+extra) for a,b in heights[tuple(event[3:5])]}) + peak=env(peak|heights[target]) + bound={(25,4+13*parity)} if backward else ({(24,0),(23,4)} if parity==0 else {(24,13),(23,16)}) + need(all(any(dom(line,b) for b in bound) for line in peak),'tight all-width Gaussian-integer grid') + return {'f_parity':parity,'k_minimum':minimum_k,'relative_grid_envelope_in_k':sorted(peak),'variable':'f=2*k+parity'} + +def verify(): + root=Path(__file__).parent;pins=json.loads((root/'SOURCES.json').read_text(encoding='utf-8'))['files'];streams={} + for pin in pins: + raw=(root/pin['package_path']).read_bytes();need(hashlib.sha256(raw).hexdigest()==pin['sha256'],'immutable input source') + payload=gzip.decompress(raw);need(hashlib.sha256(payload).hexdigest()==pin['payload_sha256'],'decompressed source') + streams[pin['orientation']]=json.loads(payload) + forward=streams['forward'];backward=streams['backward'] + need(forward['axis_dimension']==backward['axis_dimension']==25,'physical dimension') + need(forward['port_order']==backward['port_order'],'same original source cube') + nf=check_monomials(forward);nb=check_monomials(backward) + f=replay(forward['program'],forward['port_order'],False);b=replay(backward['program'],backward['port_order'],True) + f['phase_permutation_word_definitions_checked']=nf;b['phase_permutation_word_definitions_checked']=nb + f['tight_gaussian_integer_grid_by_parity']=[tight_grid(forward['program'],forward['port_order'],False,p) for p in (0,1)] + b['tight_gaussian_integer_grid_by_parity']=[tight_grid(backward['program'],backward['port_order'],True,p) for p in (0,1)] + # Control: denominator 2^20 in a real scalar edge exceeds the claimed grid. + import copy + bad=copy.deepcopy(forward['program']);edge=next(e for e in bad if e[0]=='ADD');edge[6]=1<<20 + try:replay(bad,forward['port_order'],False) + except ValueError:pass + else:raise ValueError('increased scalar denominator was not detected') + return {'status':'PASS_WHOLE_K_UNIVERSAL_EXACT_DYADIC_PRECISION','forward':f,'backward':b, + 'common_grid_bits':'g+ceil(25*f/2)+4','common_complex_magnitude_upper':'8*H*2^ceil(25*f/2)', + 'sufficient_signed_payload_bits':'g+2*ceil(25*f/2)+ceil(log2(H))+9, for H>=1', + 'required_rounding_error':'zero when the stated exact dyadic storage and arithmetic are used', + 'mutations':['increased actual scalar denominator rejected'], + 'not_claimed':['new kappa','all-family emitted phase replay','whole caller budget','constant 64-bit word size for growing f','unit-cost arbitrary precision','native kernel proof verification']} + +if __name__=='__main__':print(json.dumps(verify(),indent=2)) + + + + diff --git a/research/programmable-native-stage/verify.py b/research/programmable-native-stage/verify.py new file mode 100644 index 0000000000..e329e8144b --- /dev/null +++ b/research/programmable-native-stage/verify.py @@ -0,0 +1,25 @@ +"""Authenticate and replay constructive native-stage interfaces. Apache-2.0.""" +from pathlib import Path +from hashlib import sha256 +import json,subprocess,sys,secrets +ROOT=Path(__file__).resolve().parent +def need(ok,msg): + if not ok:raise ValueError(msg) +def integrity(): + records=json.loads((ROOT/'MANIFEST.json').read_text(encoding='utf8'))['files'];expected={r['path']:r for r in records} + actual={p.relative_to(ROOT).as_posix() for p in ROOT.rglob('*') if p.is_file() and '__pycache__' not in p.parts and p.suffix!='.pyc'}-{'MANIFEST.json'} + need(actual==set(expected),'Package inventory differs') + for name,r in expected.items(): + p=Path(name);need(not p.is_absolute() and '..'not in p.parts,'Unsafe path');raw=(ROOT/p).read_bytes();need(len(raw)==r['size'] and sha256(raw).hexdigest()==r['sha256'],'Changed bytes: '+name) + return len(expected)+1 +def main(): + count=integrity();checks=[] + for name in ['native/verify_intertwiners.py','native/programmable_stage.py','fusion/verify.py','precision/verify.py']: + cache=ROOT/('.bytecode-'+secrets.token_hex(16));need(not cache.exists(),'Fresh bytecode namespace required') + argv=[sys.executable,'-I','-B','-X','pycache_prefix='+str(cache)]+(['-O']if not __debug__ else[])+[str(ROOT/name)] + p=subprocess.run(argv,stdout=subprocess.PIPE,stderr=subprocess.PIPE,timeout=120) + if p.returncode: + sys.stderr.buffer.write(p.stderr);sys.stdout.buffer.write(p.stdout);raise RuntimeError('Scientific check failed: '+name) + checks.append({'component':name,'status':'PASS'}) + print(json.dumps({'status':'PASS_PROGRAMMABLE_NATIVE_STAGE','files':count,'optimized':not __debug__,'checks':checks,'new_kappa':False},indent=2)) +if __name__=='__main__':main()