From 9bb3f3f72925e8825c8b4851dfdc8e92b72db949 Mon Sep 17 00:00:00 2001 From: Dugongue <49054532+Dugongue@users.noreply.github.com> Date: Thu, 22 Oct 2026 10:31:33 -0700 Subject: [PATCH] Transfer conditional kappa 0.0030217758 to division-free Word RAM --- .../native-wordram-tightening/.gitattributes | 1 + .../CONTENT-HASHES.json | 45 + research/native-wordram-tightening/LICENSE | 201 + .../native-wordram-tightening/OVERLAP.json | 32 + research/native-wordram-tightening/README.md | 54 + .../native-wordram-tightening/SOURCES.json | 18 + research/native-wordram-tightening/TASK.json | 80 + .../native-wordram-tightening/VERIFY.json | 65 + .../formal/BIASED-LANE-COMPILER.md | 54 + .../formal/CHECK-RESULTS.json | 26 + .../formal/DIRTY-ARENA-RELOCATION.md | 27 + .../formal/FORMALIZATION-REUSE.md | 40 + .../formal/INDEPENDENT-REVIEW.md | 33 + .../formal/PUBLIC-SOURCE-PINS.json | 143 + .../formal/check_lanes.py | 56 + .../formal/check_newton_review.py | 53 + .../formal/check_relocation.py | 97 + .../literature/BOUNDARY-TRANSFER.md | 94 + .../literature/KRONECKER-NORMALIZATION.md | 41 + .../literature/LITERATURE.md | 58 + .../literature/SEARCH-QUERIES.json | 49 + .../literature/verify_boundary.py | 41 + .../literature/verify_normalization.py | 66 + .../native-runtime/DIVISION-CHECK.json | 7 + .../native-runtime/DIVISION-FREE.md | 52 + .../native-runtime/check_division.py | 54 + .../sources/PR4630-NATIVE-ASSEMBLY.md | 145 + .../sources/PR4630-OFFLINE-SETUP.md | 9 + .../transfer/ACTUAL-WORD.json.gz | Bin 0 -> 207673 bytes .../transfer/ARITHMETIC.json | 241 + .../transfer/CONTROLLER.json | 5224 +++++++++++++++++ .../transfer/INPUT-PINS.json | 11 + .../transfer/LATEST-ARITHMETIC.json | 241 + .../transfer/LICENSE | 201 + .../transfer/NATIVE-LIFT.md | 104 + .../transfer/NATIVE-TRANSFER.md | 93 + .../transfer/RESULT.json | 242 + .../transfer/SOURCE-PROVENANCE.json | 59 + .../transfer/critical_engine.py | 365 ++ .../transfer/majorant-benchmarks.json | 164 + .../transfer/native_lift.py | 85 + .../transfer/provider_rebind.py | 73 + .../transfer/verify.py | 43 + research/native-wordram-tightening/verify.py | 40 + 44 files changed, 8827 insertions(+) create mode 100644 research/native-wordram-tightening/.gitattributes create mode 100644 research/native-wordram-tightening/CONTENT-HASHES.json create mode 100644 research/native-wordram-tightening/LICENSE create mode 100644 research/native-wordram-tightening/OVERLAP.json create mode 100644 research/native-wordram-tightening/README.md create mode 100644 research/native-wordram-tightening/SOURCES.json create mode 100644 research/native-wordram-tightening/TASK.json create mode 100644 research/native-wordram-tightening/VERIFY.json create mode 100644 research/native-wordram-tightening/formal/BIASED-LANE-COMPILER.md create mode 100644 research/native-wordram-tightening/formal/CHECK-RESULTS.json create mode 100644 research/native-wordram-tightening/formal/DIRTY-ARENA-RELOCATION.md create mode 100644 research/native-wordram-tightening/formal/FORMALIZATION-REUSE.md create mode 100644 research/native-wordram-tightening/formal/INDEPENDENT-REVIEW.md create mode 100644 research/native-wordram-tightening/formal/PUBLIC-SOURCE-PINS.json create mode 100644 research/native-wordram-tightening/formal/check_lanes.py create mode 100644 research/native-wordram-tightening/formal/check_newton_review.py create mode 100644 research/native-wordram-tightening/formal/check_relocation.py create mode 100644 research/native-wordram-tightening/literature/BOUNDARY-TRANSFER.md create mode 100644 research/native-wordram-tightening/literature/KRONECKER-NORMALIZATION.md create mode 100644 research/native-wordram-tightening/literature/LITERATURE.md create mode 100644 research/native-wordram-tightening/literature/SEARCH-QUERIES.json create mode 100644 research/native-wordram-tightening/literature/verify_boundary.py create mode 100644 research/native-wordram-tightening/literature/verify_normalization.py create mode 100644 research/native-wordram-tightening/native-runtime/DIVISION-CHECK.json create mode 100644 research/native-wordram-tightening/native-runtime/DIVISION-FREE.md create mode 100644 research/native-wordram-tightening/native-runtime/check_division.py create mode 100644 research/native-wordram-tightening/sources/PR4630-NATIVE-ASSEMBLY.md create mode 100644 research/native-wordram-tightening/sources/PR4630-OFFLINE-SETUP.md create mode 100644 research/native-wordram-tightening/transfer/ACTUAL-WORD.json.gz create mode 100644 research/native-wordram-tightening/transfer/ARITHMETIC.json create mode 100644 research/native-wordram-tightening/transfer/CONTROLLER.json create mode 100644 research/native-wordram-tightening/transfer/INPUT-PINS.json create mode 100644 research/native-wordram-tightening/transfer/LATEST-ARITHMETIC.json create mode 100644 research/native-wordram-tightening/transfer/LICENSE create mode 100644 research/native-wordram-tightening/transfer/NATIVE-LIFT.md create mode 100644 research/native-wordram-tightening/transfer/NATIVE-TRANSFER.md create mode 100644 research/native-wordram-tightening/transfer/RESULT.json create mode 100644 research/native-wordram-tightening/transfer/SOURCE-PROVENANCE.json create mode 100644 research/native-wordram-tightening/transfer/critical_engine.py create mode 100644 research/native-wordram-tightening/transfer/majorant-benchmarks.json create mode 100644 research/native-wordram-tightening/transfer/native_lift.py create mode 100644 research/native-wordram-tightening/transfer/provider_rebind.py create mode 100644 research/native-wordram-tightening/transfer/verify.py create mode 100644 research/native-wordram-tightening/verify.py diff --git a/research/native-wordram-tightening/.gitattributes b/research/native-wordram-tightening/.gitattributes new file mode 100644 index 0000000000..625449502b --- /dev/null +++ b/research/native-wordram-tightening/.gitattributes @@ -0,0 +1 @@ +* -text diff --git a/research/native-wordram-tightening/CONTENT-HASHES.json b/research/native-wordram-tightening/CONTENT-HASHES.json new file mode 100644 index 0000000000..c3f153f17d --- /dev/null +++ b/research/native-wordram-tightening/CONTENT-HASHES.json @@ -0,0 +1,45 @@ +{ + ".gitattributes": "8b9c3028d6467ff3be7c793141927841d70f47f52d0590677438f488ca154992", + "formal/BIASED-LANE-COMPILER.md": "76c469520e48e2fb53b52cf41b34a6af39953222dee07aef2f20c28c54c1356e", + "formal/CHECK-RESULTS.json": "6692d59fc86ba129bbdddfdeae4067d1d6706e307a3d47b0f72231fa1d825ea5", + "formal/check_lanes.py": "64ca339e7d6ab8da0df40819010c5dd2f4090b170be529e3228e806ffc8bad74", + "formal/check_newton_review.py": "7b5fd2f87eea8ee5e04769781e41d7f9106586091c9fe06e5c8d05d558057bef", + "formal/check_relocation.py": "a3f3a0413c5f0922e2830fbf59dd1dd9028fdc235f99a636d355661a54d02f75", + "formal/DIRTY-ARENA-RELOCATION.md": "e082bf1491c7b2be9f6abd8e9cb2ce2fbd42acc8847848458634a7d9fe00cb35", + "formal/FORMALIZATION-REUSE.md": "ee012009dbd4c62ea46ba305ba97e6cf04ac25253b08e151a7b54bdb793e5dec", + "formal/INDEPENDENT-REVIEW.md": "87a1996f93bb1d7ab2de283c4dedd1ae44a9bc779c7ffb3373e7299d7af524ed", + "formal/PUBLIC-SOURCE-PINS.json": "db76b9c501bb64c32c29518d906a8158315e7831c696832f94336e49db98878a", + "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "literature/BOUNDARY-TRANSFER.md": "975b9977f3dc5aaf09a28e648bc81a6be764021d6bfdd85f2aa38b0b1176e852", + "literature/KRONECKER-NORMALIZATION.md": "89e6808bf60a7fdaf291245982e1a450e8e0ed78f49dbf77f4884abb8f50c55d", + "literature/LITERATURE.md": "052537c1dc171ceaa151d299c877f0439956230cc340777360146ee3bf2a3b0c", + "literature/SEARCH-QUERIES.json": "1742eb3660c8f74536f9c92344b7795e7588aa0f544067843adb361cd1376918", + "literature/verify_boundary.py": "4dfa745fc0a271a273833f7524984a53b387ce04cfb14c1f49fcaaca2c094d33", + "literature/verify_normalization.py": "ba12834f4deda74ebe29454c29321c8448226ebd3da686b84c7a0b0ca604284e", + "native-runtime/check_division.py": "b1518189f329dc9a3e22ee1ea79d8b73000010d69005111111f950b5185c8dbd", + "native-runtime/DIVISION-CHECK.json": "df727b224c627bdb69742dd3e159a0de0a1d569df4819747738fb9d75d600762", + "native-runtime/DIVISION-FREE.md": "6d481391a9547768ca17a6001d70439b61f24f06eac55d5f2d600c3f7e65f327", + "OVERLAP.json": "da7379646b0f86fd280d4ed0b8c7d7a015f6669ba12cf4e084336874951595c8", + "README.md": "956954ec1c39f01462335fae1c834c90589fd9965d5d36937d572fcc94df1f91", + "sources/PR4630-NATIVE-ASSEMBLY.md": "a1f200292ea13d72bd64cb91a4daa28261bc220a80fe9c94983f3b9a1dffaa42", + "sources/PR4630-OFFLINE-SETUP.md": "cb9becabc6102270e93f83dfe808f367771a0f1f4eff729ff01b998fb91f85dc", + "SOURCES.json": "918c9cbe30ff30332defb39b3ce6d5cea4c16f4f51853910ab5d83a6546a4582", + "TASK.json": "241933c746aa4fea0b25eef75cd6d00ef5331a07d4ba3db05a213cd9f854dbee", + "transfer/ACTUAL-WORD.json.gz": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05", + "transfer/ARITHMETIC.json": "ab10f6a4a8a4f589d4b094aac663e002c43ec44774e6bd181c51915c7fa7e521", + "transfer/CONTROLLER.json": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f", + "transfer/critical_engine.py": "e656ef12f73a8dd3bdb256eca95a712de1269facb18a652fc4068ba718619b4d", + "transfer/INPUT-PINS.json": "725ba70a2b13ba539088423d883d818eabbc7cf4508367c3217716e039f84694", + "transfer/LATEST-ARITHMETIC.json": "b4f720a7ccbb5b46e472eaf85dc8739a40598986f19b37d26c4f9ecfbd31f0de", + "transfer/LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "transfer/majorant-benchmarks.json": "513efe2fe74af82891c1918e462ba8338b1bbd06403cbfcec284bcf3b4f8f850", + "transfer/NATIVE-LIFT.md": "66188d374905361062d30710b2cd0510defcf50d3786c1e54323847c3d9f9d08", + "transfer/NATIVE-TRANSFER.md": "f19fb98feb3c20ca23ab03b339ffde5243fd4587a7620624a0b7a3678faac0ab", + "transfer/native_lift.py": "c9cbf4d8baeb993b393388a948520b1b4031ae896c10be5616a5a9bdda9dc2d9", + "transfer/provider_rebind.py": "7bf9fc5c8ebe5da0f08d04c0b85ed42864756826ba7b2fdad3bc2ee51a41cf19", + "transfer/RESULT.json": "a3a7a590340ec774ede7ce68ccf76689e73910942fc48ae00eea664ff00c50ec", + "transfer/SOURCE-PROVENANCE.json": "a6cb56e960156e637bf46663fef5985375fdbc170cb51ebce60e7a9b14f8b528", + "transfer/verify.py": "0f01c006eea27f4a6282debdb92fbc0f5f60a1a5f0432bfeed94b5ba238789a8", + "VERIFY.json": "a76f59fb65f667888a27cdb2a16456800e9c9ae1e90c7ce144f2078964569484", + "verify.py": "b7bc7349d8cf50eca3322a02b408e27705ee8e9d1b49cbd174867694535d954d" +} diff --git a/research/native-wordram-tightening/LICENSE b/research/native-wordram-tightening/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/native-wordram-tightening/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/native-wordram-tightening/OVERLAP.json b/research/native-wordram-tightening/OVERLAP.json new file mode 100644 index 0000000000..dca0d41a60 --- /dev/null +++ b/research/native-wordram-tightening/OVERLAP.json @@ -0,0 +1,32 @@ +{ + "searched_at": "2026-10-22T17:25:29.297185+00:00", + "base": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "queries": [ + "word ram", + "native", + "division" + ], + "remote_coverage": { + "open_prs": null, + "discussions": null + }, + "limitations": [ + "Broad helper refresh failed with public API rate limits; no complete PR/comment history coverage claimed.", + "Sparse local inventory did not cover all historical notes.", + "Specific source PRs and recent 60 updated PR metadata were read separately; Word RAM search returned 11 relevant PRs." + ], + "actual_source_prs": [ + 4610, + 4630, + 4635, + 4641, + 4658, + 4659, + 4694, + 4698, + 4703, + 4707 + ], + "literature_queries": 43, + "worldwide_novelty_claimed": false +} diff --git a/research/native-wordram-tightening/README.md b/research/native-wordram-tightening/README.md new file mode 100644 index 0000000000..8e903887f3 --- /dev/null +++ b/research/native-wordram-tightening/README.md @@ -0,0 +1,54 @@ +# Conditional native Word RAM kappa = 0.0030217758, without division + +Prepared for Dugongue with substantial OpenAI Codex assistance: one lead and three research/review workers. Apache-2.0; retained source notices apply. + +This source-bound transfer raises the native Word RAM saving from 0.0030217754 in PR #4635 to 0.0030217758, an exact gain of 4 times 10^-10. It gives O(n / (log n)^0.0030217758) operations for packed n-bit inputs and outputs on words of C log n bits. It uses native arrays and bounded-word arithmetic, without a TM simulator or TM multiplier. + +This matches PR #4610's latest headline; it does not exceed its raw crossing, change the paid profile, or establish a new global multiplication record. The numerical gain is native provider funding and transfer tightening. The division elimination strengthens the instruction-set conclusion while preserving that saving. + +## Result and inherited premises + +[transfer/NATIVE-TRANSFER.md](transfer/NATIVE-TRANSFER.md) freezes PR #4610 at 20bb93cd990d2ff683e4d0fc56b87a42cd5d3296. It reconstructs the complete 64,404-call paid invoice and 10,928 productive fields from the literal word and actual p16 controller, then funds the critical majorant at q_C = 1057621533/350000000000 and N = 2^38569300000000000. The absorption logarithm has exact lower bound 6611668/5. All nine native rows have strict margins over the target. + +The actual native algorithms are retained in sources/PR4630-NATIVE-ASSEMBLY.md. The supplier and its constants are effectively specified but not materialized. No practical cutoff or complete executable multiplier is supplied. + +The conclusion remains conditional on the inherited all-fiber identities, native phases and normalizers, whole-job and owned-storage contracts, chronological compiler, conditioning, Gaussian/Poisson and fine-padding reduction, precision and exact recovery. Arithmetic replay does not independently prove those premises. No fresh Lean kernel/axiom check, physical phase replay, maintainer admission or independent human acceptance is claimed. + +[native-runtime/DIVISION-FREE.md](native-runtime/DIVISION-FREE.md) proves an exact all-divisor reciprocal Newton construction using O(log w) native operations and constant-limb temporaries. Replacing every bounded-word DIV adds only a polylog(log n) factor, absorbed by the strict margins. The machine explicitly has both logical shifts, low-word multiplication, Boolean operations, comparisons, add/subtract and indexed memory. Lax13 derives right shift using division, so this does not delete DIV from that literal machine. Classical reciprocal division is credited, not claimed new. + +## Constructive support and literature + +The support results are separate sufficient constructions, not extra numerical gains attributed to this bound: + +- formal/BIASED-LANE-COMPILER.md batches bounded signed scalar traces across independent dirty columns, with odd exact division and explicit conversion/address costs. Full-word lanes give no growing packing factor. +- formal/DIRTY-ARENA-RELOCATION.md preserves arbitrary dirty exterior with no arena-copy pass and at most 3T+1 instructions. FORMALIZATION-REUSE.md identifies the actual Problem 1.8 lower-level native compiler and ownership ports; its polynomial-time convenience wrapper does not ensure logarithmic words. +- literature/KRONECKER-NORMALIZATION.md explicitly normalizes nonzero 2 by 2 tensor factors to OR-indexed matrices, paying every diagonal and permutation. It connects to Alman and Li's 2025 shallow-circuit theorem, not a faster current dominant transform. +- literature/BOUNDARY-TRANSFER.md gives precision and native tariffs for a fixed bilinear matrix-multiplication certificate. Strassen permits ceiling 12/125 instead of 3/32, but the much smaller provider saving remains binding. + +The literature/LITERATURE.md report records 43 queries, 10 primary publications and 8 pinned public Lean files across 4 repositories. This is a systematic bounded search, not an exhaustive search of all literature, comments, repositories or the semantic DAG. No claim of first-ever application is inferred from missing matches. Source-only statements and challenge statements with sorry are distinguished from checked proofs. No third-party Lean source is vendored. + +## Reproduction + +From the repository root with Python 3.12 or later, standard library only: + +```sh +python3 -I -O -B research/native-wordram-tightening/verify.py +``` + +The verifier authenticates the complete inventory and runs isolated components without Git/network or external dependencies. It reconstructs the full invoice, funds the root/mirror/majorant, checks all nine rational guards and five provider/parameter mutants, and checks the supporting scalar, relocation, tensor and boundary identities. Two independent division scripts check exact quotients and intermediate invariants. Source-corruption checks first accept an unmodified baseline, then reject changes. Python big integers are verifier tools, not native unit-cost instructions. + +Finite checks corroborate the supplied proofs; they do not establish the inherited full multiplication theorem. Local Windows replay is claimed, not a new Linux run or complete native implementation. Formal source inspection is not a fresh Lean build. + +## Sources, overlap and credit + +Canonical main: b58ad9ef4d4e861b0eaa5dba41742bdc072dca51, priority revision 7. The selected conditional value remains 0.00302015. transfer/SOURCE-PROVENANCE.json and INPUT-PINS.json bind public source paths, commits and bytes. Frozen upstream bytes are unchanged. + +PR #4641 already identified the profile-only origin of #4635's earlier gain; this package agrees. PR #4703 has complementary B/C suppliers but no profitable consumer. PR #4694/#4698 have coupled centers and a homogeneous consumer whose actual chart embedding remains unresolved; neither funds this bound. PR #4658/#4659 cover scoped path-family ceilings, not universal RAM barriers. PR #4707 tightens an older selected root. Live overlap coverage limits are in OVERLAP.json. + +Credit Cao Yifan / intqwq (#4610), Cinna Davis and the #4470 joint-helper/controller lineage, Dugongue (#4630/#4635/#4703), Dillon, zxv, Jacob Alan Sussman, Ryanson Jonathan, Vlado Vojdanovski, Chafik Boukhalfa, Tim Trudgian, Jeremy Kothe, eumemic, icekylinx, Harvey and van der Hoeven, and all retained source owners. Formal reuse credits Jan Dreier and Claude Fable 5, the Lax archive, the Anthropic 3SUM/APSP compiler, Hex and Sendov packing developments and public authors named in the literature report. Publication mechanisms credit Alman and Li, Chan/Jin/Vassilevska Williams/Xu, Strassen, Granlund/Montgomery and Moller/Granlund. Substantial AI assistance is disclosed. + +## Open next questions + +1. Find an admitted changed provider or actual coupled-center consumer improving the raw moment. Start with physical entrance/exit charts and every paid conversion; stripped scalar rank does not give free physical access. +2. Independently audit the inherited all-fiber, compiler, analytic and recovery composition. The transfer does not upgrade those premises to fresh kernel or human acceptance. +3. Implement a complete native caller and fixed-limb backend before claiming practical measured speedups. These checkers and asymptotic proofs do not supply that benchmark. diff --git a/research/native-wordram-tightening/SOURCES.json b/research/native-wordram-tightening/SOURCES.json new file mode 100644 index 0000000000..4916cee8e5 --- /dev/null +++ b/research/native-wordram-tightening/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + } + ] +} diff --git a/research/native-wordram-tightening/TASK.json b/research/native-wordram-tightening/TASK.json new file mode 100644 index 0000000000..fd53f80e64 --- /dev/null +++ b/research/native-wordram-tightening/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Transfer the latest funded native provider to kappa 0.0030217758 on Word RAM, then remove the division instruction while preserving all paid native rows.", + "scope_change_reason": "User explicitly assigned native Word RAM improvement and literature/formalization search. The native saving improves over PR4635; the profile and global raw crossing are unchanged.", + "bottleneck_link": "Binds the actual latest finite provider to all nine native tariffs and a weaker arithmetic instruction set; does not replace missing all-fiber or analytic premises.", + "budget_minutes": 60, + "stop_rule": "One bounded session, three independent leaves, exact source/parameter checks and portable packaging; no new raw-root claim without a changed admitted profile.", + "outcome": "completed", + "evidence": "transfer/NATIVE-TRANSFER.md, native-runtime/DIVISION-FREE.md and verify.py establish the stated conditional transfer and exact component checks.", + "author": "Dugongue", + "ai_assistance": "Prepared for Dugongue with substantial OpenAI Codex assistance; one lead and three parallel workers.", + "open_questions": [ + { + "question": "Can a changed admitted provider improve the raw moment?", + "why_it_matters": "Would improve the binding native row.", + "first_step": "Construct the actual whole-job interface and complete paid bill.", + "blocked_by": "No profitable coupled-center or complementary consumer found." + }, + { + "question": "Can the inherited full composition be independently audited?", + "why_it_matters": "Would strengthen conditional status.", + "first_step": "Audit one exact all-fiber/compiler/analytic caller.", + "blocked_by": "Fresh arithmetic does not establish universal predecessor premises." + } + ] +} diff --git a/research/native-wordram-tightening/VERIFY.json b/research/native-wordram-tightening/VERIFY.json new file mode 100644 index 0000000000..002eb2c749 --- /dev/null +++ b/research/native-wordram-tightening/VERIFY.json @@ -0,0 +1,65 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/native-wordram-tightening/.gitattributes", + "research/native-wordram-tightening/LICENSE", + "research/native-wordram-tightening/OVERLAP.json", + "research/native-wordram-tightening/README.md", + "research/native-wordram-tightening/SOURCES.json", + "research/native-wordram-tightening/TASK.json", + "research/native-wordram-tightening/VERIFY.json", + "research/native-wordram-tightening/formal/BIASED-LANE-COMPILER.md", + "research/native-wordram-tightening/formal/CHECK-RESULTS.json", + "research/native-wordram-tightening/formal/DIRTY-ARENA-RELOCATION.md", + "research/native-wordram-tightening/formal/FORMALIZATION-REUSE.md", + "research/native-wordram-tightening/formal/INDEPENDENT-REVIEW.md", + "research/native-wordram-tightening/formal/PUBLIC-SOURCE-PINS.json", + "research/native-wordram-tightening/formal/check_lanes.py", + "research/native-wordram-tightening/formal/check_newton_review.py", + "research/native-wordram-tightening/formal/check_relocation.py", + "research/native-wordram-tightening/literature/BOUNDARY-TRANSFER.md", + "research/native-wordram-tightening/literature/KRONECKER-NORMALIZATION.md", + "research/native-wordram-tightening/literature/LITERATURE.md", + "research/native-wordram-tightening/literature/SEARCH-QUERIES.json", + "research/native-wordram-tightening/literature/verify_boundary.py", + "research/native-wordram-tightening/literature/verify_normalization.py", + "research/native-wordram-tightening/native-runtime/DIVISION-CHECK.json", + "research/native-wordram-tightening/native-runtime/DIVISION-FREE.md", + "research/native-wordram-tightening/native-runtime/check_division.py", + "research/native-wordram-tightening/sources/PR4630-NATIVE-ASSEMBLY.md", + "research/native-wordram-tightening/sources/PR4630-OFFLINE-SETUP.md", + "research/native-wordram-tightening/transfer/ACTUAL-WORD.json.gz", + "research/native-wordram-tightening/transfer/ARITHMETIC.json", + "research/native-wordram-tightening/transfer/CONTROLLER.json", + "research/native-wordram-tightening/transfer/INPUT-PINS.json", + "research/native-wordram-tightening/transfer/LATEST-ARITHMETIC.json", + "research/native-wordram-tightening/transfer/LICENSE", + "research/native-wordram-tightening/transfer/NATIVE-LIFT.md", + "research/native-wordram-tightening/transfer/NATIVE-TRANSFER.md", + "research/native-wordram-tightening/transfer/RESULT.json", + "research/native-wordram-tightening/transfer/SOURCE-PROVENANCE.json", + "research/native-wordram-tightening/transfer/critical_engine.py", + "research/native-wordram-tightening/transfer/majorant-benchmarks.json", + "research/native-wordram-tightening/transfer/native_lift.py", + "research/native-wordram-tightening/transfer/provider_rebind.py", + "research/native-wordram-tightening/transfer/verify.py", + "research/native-wordram-tightening/verify.py", + "research/native-wordram-tightening/CONTENT-HASHES.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Authenticate exact inventory, reconstruct and fund latest provider, verify all nine native rows and negative controls, check division and constructive support, reject drift. Conditional premises stay explicit." + } + ] +} diff --git a/research/native-wordram-tightening/formal/BIASED-LANE-COMPILER.md b/research/native-wordram-tightening/formal/BIASED-LANE-COMPILER.md new file mode 100644 index 0000000000..cd971e7225 --- /dev/null +++ b/research/native-wordram-tightening/formal/BIASED-LANE-COMPILER.md @@ -0,0 +1,54 @@ +# A direct native compiler for bounded exact scalar traces + +Status: proved informally below, with finite regression checks in check_lanes.py. This is not a new multiplication κ and is not a freshly kernel-checked Lean theorem. The mechanism is a concrete adaptation of classical guard-bit / Kronecker packing to the independent dirty-column interface. No priority claim is made for packing itself. + +## Sufficient theorem + +Let a fixed straight-line scalar program have T gates, r input registers, and o requested output registers. Its permitted gates are copy, negation, addition, subtraction, multiplication by a fixed integer c with |c| ≤ C, and exact division by a positive fixed integer d in a finite set Δ. Here C ≥ 1. All f executions have the same control and register addresses. Suppose their inputs, every gate result, and every live scalar are integers in [−H,H]. Each division gate is certified to have d dividing its argument in every column. There is no relation among columns or among the dirty helper inputs beyond these bounds and exact-divisibility promises. + +Choose B ≥ max(H,1) divisible by every d in Δ; for example B = D ceil(max(H,1)/D), where D is their least common multiple (D = 1 for no divisions). Choose s with R = 2^s > 2(C+2)B. Let k ≥ 1 satisfy ks ≤ w. Suppose all memory addresses used for packed registers and counters are below 2^w; their total number is the original register count times ceil(f/k), plus fixed scratch space. Then a single uniform native Word RAM program evaluates all f columns exactly in + + O((r+o)f + T ceil(f/k) + s + f) + +word instructions, with the constant depending only on the fixed scalar gate set and address layout. With packed input and output already in this ABI, the conversion terms become O((r+o) ceil(f/k)). The program uses multiplication/division only on w-bit words and never simulates a Turing machine. The ordinary unpacked conversion cost is retained in the first bound. + +## Encoding and identities + +For a group of k columns, write Rep = Σ(j=0..k−1) R^j and E(v) = Σ(j=0..k−1) (v_j+B) R^j. A short final group is padded with zero-valued columns. Since 0 ≤ v_j+B ≤ 2B < R, these are canonical base-R digits and are uniquely decodable. All preconditions apply to padded executions too; linear homogeneous gates keep those added columns zero. + +The exact native implementations are: + +- addition: E(x+y) = E(x)+E(y)−B Rep; +- subtraction: E(x−y) = E(x)+B Rep−E(y), with the addition performed first; +- negation: E(−x) = 2B Rep−E(x); +- positive c multiplication: E(cx) = c E(x)−(c−1)B Rep; +- c = 0: return B Rep; +- negative c: negate, then use |c| multiplication; +- exact division by d: E(x/d) = E(x)/d + ((d−1)B/d) Rep; +- copy: copy the packed word. + +For division, d divides both x_j and B; therefore every encoded digit x_j+B is divisible by d. Consequently E(x)/d = Σ ((x_j+B)/d) R^j as an exact integer identity. No assumption d divides R is needed. This addresses odd exact divisors as well as powers of 2. The displayed correction (d−1)B/d means the integer (d−1)(B/d), and is computed in that order. Division d = 1 is the identity. If d exceeds B, divisibility and B > 0 imply B ≥ d, so this case cannot arise under the chosen B. + +## Proof of machine safety and correctness + +Each digit of the addition temporary is at most 4B; each subtraction temporary is at most 3B; each positive-multiplication temporary is at most 2CB; each negation temporary is at most 2B. All are strictly below R by its choice. Each final digit lies in [0,2B] because the scalar gate result has magnitude at most H ≤ B. The division intermediate has nonnegative digits at most 2B/d, and its final corrected digits are at most 2B. Thus no intermediate carry reaches another lane. Every packed intermediate is below R^k ≤ 2^w, so native modular arithmetic is identical to ordinary natural arithmetic. Every subtraction is nonnegative: its difference is the encoding of a scalar result known to lie in [−B,B]; hence natural-number monus is also ordinary subtraction. Constants B Rep, 2B Rep and (c−1)B Rep fit for the same reason. For negative c, the negated intermediate remains within [−H,H]. + +Induction over gates now proves that every packed register is the encoding of the exact k independent scalar registers. This proves the theorem for all f and all admissible dirty inputs, not only for sampled data. Register overwriting is safe by reading the original operands into scratch words before writing the destination; the proof does not assume distinct gate destination and input addresses. The address-fit hypothesis excludes address wraparound, independently of value fit. + +To construct the encoding from unpacked input, scan each group once, multiplying the accumulated word by R and adding the next biased digit in reverse lane order. The intermediate prefixes remain below R^k. Build Rep in the same way, using O(k) steps once; all recurrent affine correction constants then require O(1) operations because the gate set is fixed. Decode by repeated division/remainder by R and subtraction of the known bias using a signed two-word or sign/magnitude output convention; output costs O(of). B can be derived by integer division/multiplication from the supplied bound H and fixed D. For k >= 2, s < w, so construct R by s doublings. For k = 1 and s = w, R itself does not fit; bypass multiplication/remainder by R, since a one-lane word needs neither operation. Its repunit is 1 and its sole decoded digit is the word itself. These charges give the asserted bound. All scalar bound and count parameters stored in machine cells must fit; this includes f if a one-word outer-loop counter is used. The fixed constants C and D fit whenever the stated R and B hypotheses are satisfiable. For an asymptotic family, finitely many smaller widths may use a separately specified finite base case. A uniform implementation receives f, s and the bound H, rather than baking an input-dependent packed word into its program. + +## Link to the native exponent, stated without a new value + +Use the native normalization W(n) = O(n/(log n)^kappa0), with n and the input/output ABI exactly as in the native predecessor theorem. Suppose a complete algorithm in that same model has actually batchable scalar work S(n) = O(n/(log n)^kappa0), lane width s(n) = O((log n)^(1-delta)), word width w(n) = Theta(log n), and enough independent columns to fill Omega((log n)^delta) lanes. Suppose, additionally, all conversion, control and unbatched work totals O(n/(log n)^(kappa0+delta)). Then the concrete construction above gives native cost O(n/(log n)^(kappa0+delta)). Proof: k = Omega((log n)^delta), so S(n)/k has the target bound; add the explicitly charged remaining work. This is a sufficient native algorithmic implication. It does not establish those premises for the current supplier/controller. In particular s(n) = Theta(log n) gives only constant lane count, and an unpacked O(n) boundary would dominate the proposed native cost. A complete improvement must demonstrate growing usable packing and its boundary ABI within the already established native model; changing the unit of cost is not a contribution to this exponent. + +## Reuse and attribution + +The direct machine endpoint is the existing Problem 1.8 Lax13 compiler. Mathproof.Meta.Problem18RAMLax13ProofsSimulation20261001.compile_correct accepts a bounded IMP BigStepB run, explicit Layout.FitsWords and a representing machine state; it produces a native run with time ≤ Layout.const times the IMP cost. Its compileProgram_runsTo theorem handles literal input/output, clean initial memory and genuine halt. The theorem permits arbitrary initial represented environments in its local form. The scalar macro frame discipline in Problem18ClaudeFieldMacros20261001 gives the model for separating output slices, inputs and scratch. No RAM→TM module is needed in this route. + +These statements were inspected as source only in this session; no current-source Lean replay or transitive axiom audit was run. PUBLIC-SOURCE-PINS.json fixes the inspected bytes. The source catalog search covered registered lexical hits for word RAM and packing; it did not exhaustively semantically inspect the entire DAG. The typed workspace query for compileProgram_runsTo returned no indexed hit. Existing compiled artifacts, if present elsewhere, do not upgrade this session's evidence. + +Classical antecedents include Kronecker substitution and word-parallel arithmetic. Public formalization leads checked on 22 October 2026: Jan Dreier and Claude Fable 5's Lax word-RAM compiler (https://laxarchive.org/lax-13/index.html; superseded by https://github.com/lax-archive/lax-submissions/tree/9394e531cc51cb67a0214bca3f9264dfe97ba5c7/word-ram), the 3SUM/APSP native compiler (https://github.com/anthropics/formal-math/blob/main/3sum-apsp/docs/MACHINE.md), signed Kronecker correctness in https://github.com/leanprover/hex-poly-z/blob/main/SPEC/hex-poly-z.md, and https://github.com/teorth/sendov/blob/master/docs/design.md. The last two sources establish relevant precedents, not a fresh machine-cost theorem for this package; source paths behind their documented claims were not replayed here. No source copied from them is included. + +## Open next questions + +Apply the bound H to the actual retained supplier trace, including arbitrary dirty inputs and every recursive denominator grid. Determine whether an independently growing column multiplicity survives whole-job boundary conversions. Port the exact native finite trace to the bounded IMP semantics, then invoke the existing compiler and independently audit the resulting native theorem. These are applications of the proved sufficient construction above; no missing result is assumed to claim a higher κ. diff --git a/research/native-wordram-tightening/formal/CHECK-RESULTS.json b/research/native-wordram-tightening/formal/CHECK-RESULTS.json new file mode 100644 index 0000000000..5edcad8fb9 --- /dev/null +++ b/research/native-wordram-tightening/formal/CHECK-RESULTS.json @@ -0,0 +1,26 @@ +{ + "check_lanes.py": { + "status": "PASS_FINITE_REGRESSION_ONLY", + "exact_checks": 195102, + "basis": "w-bit modular multiply/add, monus, integer division", + "proof_scope": "informal universal argument in BIASED-LANE-COMPILER.md" + }, + "check_relocation.py": { + "status": "PASS_FINITE_REGRESSION_ONLY", + "seeds": 1200, + "checked_step_or_halt_correspondences": 20593, + "checked_completed_steps": 19696 + }, + "unicode_controls": { + "BIASED-LANE-COMPILER.md": "valid UTF-8; no replacement/control characters", + "DIRTY-ARENA-RELOCATION.md": "valid UTF-8; no replacement/control characters", + "FORMALIZATION-REUSE.md": "valid UTF-8; no replacement/control characters" + }, + "check_newton_review.py": { + "status": "PASS_INDEPENDENT_NEWTON_ARITHMETIC", + "exhaustive_small_word_quotients": 86868, + "large_word_quotients": 2160, + "largest_width": 1024, + "scope": "Arithmetic identities and invariants only; primitive shifts/full products still require their stated native lowering." + } +} diff --git a/research/native-wordram-tightening/formal/DIRTY-ARENA-RELOCATION.md b/research/native-wordram-tightening/formal/DIRTY-ARENA-RELOCATION.md new file mode 100644 index 0000000000..1c28a966d8 --- /dev/null +++ b/research/native-wordram-tightening/formal/DIRTY-ARENA-RELOCATION.md @@ -0,0 +1,27 @@ +# Native dirty-arena relocation with bounded addresses + +Status: an informal universal sufficient theorem with an explicit machine construction. No new κ and no fresh Lean proof are claimed. + +## Theorem + +Let p be a native Lax13 word-RAM program at word width w. Let A ≥ 1. Assume every direct memory operand in p is below A. Consider any execution of T steps in which every indirect address actually used is below A. Arithmetic values may occupy the full range [0,2^w); only addresses need the bound A. Choose an arena origin b with b+A+2 ≤ 2^w. There is a mechanically constructed relocated program p_b, running at the same word width, that reproduces the source input/output and all active source cells at addresses b+i, uses at most 3T+1 instructions to reach the corresponding state, and leaves every address outside [b,b+A+2) untouched. Initial memory outside the embedded active source cells is arbitrary. Only the two cells b+A and b+A+1 are added scratch. No copy of the arena and no initialization of its dirty exterior is needed. The fixed program p_b depends on b, but the same construction works for every permitted b. + +## Construction + +Reserve a base cell c = b+A and pointer scratch s = b+A+1. Begin with SET c b. Replace each source instruction by a block of exactly three instructions, padding unused slots with SET s 0. Every direct operand i is replaced by b+i. Arithmetic, SET literals, READ and WRITE retain their values unchanged. In particular data literals are not confused with addresses and are never blindly shifted. + +For LOAD a z use ADD s c (b+z), then LOAD (b+a) s, then padding. For STORE z a use ADD s c (b+z), then STORE s (b+a), then padding. Thus logical pointer values remain exactly their original values, and the origin is added only at the point of dereference. A source JUMP l becomes two padding instructions followed by JUMP (1+3l). A source JZERO z l becomes two padding instructions followed by JZERO (b+z) (1+3l). A source HALT becomes two padding instructions followed by HALT. The initial origin setup is at program counter 0; source counter j corresponds to counter 1+3j. Program counters are natural numbers, not data addresses, in the Lax13 model. Reaching the first out-of-range source counter corresponds to the first out-of-range translated counter and halts as well. + +## Proof + +After setup, relate each source cell i < A to target cell b+i, and source counter j to 1+3j. The base cell holds b; input and output lists agree. All translated direct operands are below b+A. At each dereference, the source pointer z is below A by hypothesis, so b+z < b+A ≤ 2^w; the address addition is exact. Its scratch cell cannot alias any source cell. The LOAD or STORE therefore reads or writes precisely the related cell. Arithmetic instructions have identical operands and the same modulus 2^w, so identical results even when intermediate mathematical values overflow a word. Branches inspect identical words and jump to related counters. READ and WRITE observe identical tapes. Padding touches only scratch. Induction on the source execution proves the relation after each completed block and equality of external input/output. Each source step uses at most three target steps, plus the single setup instruction. Every target write is to a related active cell or one of the two scratch cells, establishing the arbitrary-exterior frame property. The conclusion concerns completed source steps; native HALT is observed at the corresponding final block instruction and preserves genuine halt. + +## Why this is directly useful here + +The arbitrary dirty helper values in a supplier remain literal data at their existing arena locations. Their values need not be moved or cleaned merely to install an addressing convention. Independent supplier arenas can be relocated and composed provided the caller chooses disjoint owned scratch and respects each actual address bound. This avoids a false inference from the clean initial-state theorem compileProgram_runsTo to a dirty hosted run. The existing Problem 1.8 local theorem compile_correct already begins with an arbitrary representing native state; its Represents predicate constrains only declared scalar cells and valid array entries. Expression-block Reaches.frame gives the corresponding explicit scratch discipline. The present native wrapper supplies a separate constructive arena embedding and frame theorem. + +This does not prove a complete recursive ownership schedule or an improved multiplication exponent. It eliminates memory copying for this specific offset adapter with an explicit constant instruction cost. No source-memory bound can be omitted: full-word arithmetic values are allowed, but actual pointer values must fit the selected arena. An arbitrary global memory permutation does not preserve pointer arithmetic without such a dereference adapter. + +## Provenance and evidence + +The inspected machine is Mathproof/Meta/Problem18RAMLax13Ram20261001.lean, derived from Jan Dreier and Claude Fable 5's Lax13 Word RAM. Relevant source declarations are Instr, Instr.effect, step, RunsTo; the local compiler proof is Mathproof/Meta/Problem18RAMLax13ProofsSimulation20261001.lean, Represents at line 56, Reaches at line 70, compile_correct at line 544, compileProgram_runsTo at line 896. These are source-inspection precedents, not a new kernel audit. A historical .olean exists for the simulation module, dated 1 October; no fresh audit binds it to the source inspected here. PUBLIC-SOURCE-PINS.json records current bytes. Standard register-machine relocation and separation-style frame reasoning are antecedents; no claim of first use is made. diff --git a/research/native-wordram-tightening/formal/FORMALIZATION-REUSE.md b/research/native-wordram-tightening/formal/FORMALIZATION-REUSE.md new file mode 100644 index 0000000000..844003270c --- /dev/null +++ b/research/native-wordram-tightening/formal/FORMALIZATION-REUSE.md @@ -0,0 +1,40 @@ +# Exact reusable formal interfaces and their evidence + +This is discovery and source inspection, not a fresh Lean compilation or axiom audit. The active canonical modules and DAG are unchanged. The source hashes in PUBLIC-SOURCE-PINS.json identify the inspected bytes; new proofs in this directory are informal. + +## 1. Direct bounded IMP-to-native Word RAM compilation + +Source: Mathproof/Meta/Problem18RAMLax13ProofsSimulation20261001.lean. + +Theorem `Lax13Proofs.Simulation.compile_correct` at line 544 takes a bounded terminating semantic run `BigStepB B c sigma sigma' k`, `Com.Ok L c`, input boundedness, a machine state representing sigma, code at its actual program counter, and `L.FitsWords B w`. It yields a run of the literal native compiled code, the representing final state, the next program counter, and an instruction count at most `L.const*k`. The caller can supply an arbitrary represented initial environment; this is the appropriate local contract for arbitrary dirty helpers. The whole-program `compileProgram_runsTo` at line 896 also establishes genuine halt and tape output from clean machine initialization. + +`Layout.FitsWords`, in Problem18RAMLax13ProofsCompile20261001.lean at line 107, requires `1 < B`, `B <= 2^w`, and `L.span B <= 2^w`. Here `L.span B = temps+2+scalar_count+array_count*B`. For array index i and array a, physical address is `temps+2+scalar_count+idxOf(a)+array_count*i`; `arrAddr_inj` proves disjointness. This is a fixed strided ABI, not a promise that all array metadata allocation is free. + +Important limitation: the convenience wrapper `Problem18IMPUniformCompiler20261001.compileProgram_runs_polynomial` is a polynomial-time computability theorem. Its word-width lower bound adds total input bitSize and a polynomial in bitSize. It must not be used as evidence of standard logarithmic word width. For the native multiplication application, prove FitsWords directly at the actual word width using the lower-level theorem. No RAM-to-Turing compilation is needed. + +## 2. Framed scalar and field macros + +Source: Mathproof/Meta/Problem18Claude/Problem18ClaudeFieldMacros20261001.lean. + +`MacroInput` requires valid register names, encoded field degree and prime, arithmetic and inversion word bounds, actual input/output slice fits, output disjoint from input and modulus slices, and canonical coordinates. `BinarySpec` quantifies over every B and initial environment satisfying these obligations, then gives an actual Run, the exact decoded output, canonical output and `MacroFrame`. `MacroFrame` preserves all unrelated scalar variables, unrelated arrays, memory outside the output slice, array lengths, and input/output tapes. Its `BinarySpec.call` theorem additionally charges argument installation: `3 + a.size + b.size + o.size + cost`. + +This is a reusable compositional ownership discipline. It supports a real caller-state proof instead of assuming clean helpers, and distinguishes output from scratch. The instantiated finite-field macros should not be treated as native complex arithmetic without a representation and ring-homomorphism proof; they are precedents for the contract, not magic Gaussian operations. + +## 3. Cross-machine bridge as a model audit precedent + +Source: Mathproof/LibraryBridges/Claude/ThreeSumRamSimulation_20261007.lean. + +The existing bridge compiles the 3SUM/APSP EndStatement RAM to Lax13 and gives an explicit bound `12 + 12*input_length + 35*t`. It uses one extra word bit and an arena offset, and states `CellsFit` for literal cell names. Its separate `sim` theorem exposes the final memory. This is concrete precedent that model conversion can have a real address-bit and I/O charge, which must be kept when claiming a transferred exponent. It is not a theorem that any RAM model or arbitrary word width automatically preserves every asymptotic claim. + +## 4. Public formal packing sources inspected + +- Jan Dreier and Claude Fable 5: Lax13 Word RAM and verified compiler pipeline. Current successor source: https://github.com/lax-archive/lax-submissions/tree/9394e531cc51cb67a0214bca3f9264dfe97ba5c7/word-ram . The archive landing page https://laxarchive.org/lax-13/index.html explicitly distinguishes machine definitions from downstream proof obligations. Its old v4.30.0 environment is superseded by v4.33.0; do not silently mix imports. +- `Hex.ZPoly.natAbs_mulCoeff_le_min` in https://github.com/leanprover/hex-poly-z/blob/main/HexPolyZ/Kronecker.lean at lines 188-195 proves the asymmetric coefficient bound `abs(coeff_n(p*q)) <= min(p.size,q.size)*A*C`. The current source already contains it, although SPEC prose describes a related refinement as unspent. It is therefore not a new result of this session. `kronecker_identity` at line 551 proves signed recovery under an explicit coefficient budget; `mulKroneckerAt_eq` at line 664 and `mulKronecker_eq` at line 724 discharge runtime branch/width choices. This is algebraic correctness, not a native w-bit instruction-cost proof. +- https://github.com/teorth/sendov/blob/master/Sendov/FiniteRange/Pack.lean: `unpackN_pow` at line 163, `unpackZ_pevZ` at line 227. These are direct polynomial-digit recovery precedents; their large-Nat performance does not establish one-word packing or an asymptotic integer multiplier. +- https://github.com/anthropics/formal-math/blob/main/3sum-apsp/docs/MACHINE.md describes a separate native RAM compiler and polynomial-limit word-size slopes. The exact generous model assumptions in that guide remain part of its claims. + +The retrieved external Lean files are retained privately as discovery snapshots with original notices; they are not dependencies of the new informal lemmas. No external theorem has been independently rebuilt in this session. No exhaustive negative novelty claim is made: bounded web searches and registered lexical queries can identify mechanisms, but cannot prove nobody has applied them. + +## Reproducible evidence in this directory + +`check_lanes.py` passes 195102 exact finite identities using modular word arithmetic, natural-number monus and exact integer division, including odd divisors. `check_relocation.py` checks 1200 seeded native programs: 20593 step-or-halt correspondences, including 19696 completed source steps, with arbitrary dirty exterior preserved. Both run successfully with `python -I -O -B`; their checks use explicit exceptions and remain active under optimization. These are regression controls, not proofs of the universal lemmas, whose informal proofs are written separately. diff --git a/research/native-wordram-tightening/formal/INDEPENDENT-REVIEW.md b/research/native-wordram-tightening/formal/INDEPENDENT-REVIEW.md new file mode 100644 index 0000000000..7fb2923217 --- /dev/null +++ b/research/native-wordram-tightening/formal/INDEPENDENT-REVIEW.md @@ -0,0 +1,33 @@ +# Independent source and mathematics review + +Reviewer lane: formalization and model interfaces. Prepared for Dugongue with substantial OpenAI Codex assistance. This records source inspection and informal mathematical review, not independent human approval, fresh Lean verification, or a complete proof audit of inherited sources. + +## Native provider and nine-row transfer + +Independently executed `frontier/native_transfer/provider_rebind.py` using Python 3.12 with -I -O -B. It passed, reconstructing the actual decompressed source word, local primal/raw-dual paid histograms, independent helper ranks, all controller event counts, and the complete 64404 paid / 10928 productive inventory. The narrower root interval is [.99697822412,.99697822414]. The retained mirror-window and shifted-log critical-majorant checks pass for the changed profile. The fetched uniform saving is 1057621533/350000000000, and the fixed rank is 2^38569300000000000. The conservative logarithmic absorption surplus is 6611668/5. These are exact source-bound arithmetic conclusions; they do not discharge the inherited all-fiber endpoint, whole-job normalizer, compiler-construction or analytic identities. + +Read the copied #4635 NATIVE-LIFT.md and #4630 NATIVE-ASSEMBLY.md. All nine advertised savings agree with their actual tariff rows. For c = 3/32, the universal delta choice gives the key strict inequalities, including beta+1-epsilon = 1-2delta and chirp slack 2(c-q)+delta*(122/25+2q). Main, fused Gaussian, group scans, both addressing passes, complete boundary algebra, sparse visits, global-precision record products and core-face recovery are all accounted for. The source-native model uses packed n-bit input, O(log n)-bit words with a fixed sufficiently large coefficient, and O(n/(log n)^kappa) word operations. It is not a transfer into a fresh smaller word machine per record. + +The provider witness is now bound by NATIVE-TRANSFER.md and RESULT.json to PR #4610 head 20bb93cd990d2ff683e4d0fc56b87a42cd5d3296, with q_C = 1057621533/350000000000 and H = 38569300000000000; the earlier stale-witness issue is resolved in the fresh arithmetic replay. The numerical increase keeps the identical paid profile and critical root. It should be described as native transfer / finite-absorption tightening, not discovery of a better paid supplier or a new combinatorial mechanism. + +## Kronecker normalization + +The explicit L_i, R_i, complement J and tensor diagonal identity in literature/KRONECKER-NORMALIZATION.md are correct over every field under the stated nonzero-entry hypothesis. Their O(N+k) algebraic construction can be implemented by binary expansion of factor choices. The entrywise proof uses OR, and both complement permutations are necessary. The stated external diagonal magnitude/reciprocal bounds follow directly from the one-factor bounds; they do not bound the interior coefficients of a shallow circuit. + +Primary source checked: https://arxiv.org/html/2509.14489v1 , Corollary 1.1 (lines 165-173 in the fetched HTML). It states exactly depth 4 and size O(N^1.249424) for f(x OR y), and explicitly notes unbounded coefficients can be confined to one layer. Thus the shallow circuit applicability is supported. It still requires actual coefficient-generation, precision and complete native caller costs before it yields an exponent improvement. No claim that this already improves the dominant transform row is justified. + +## Boundary certificate theorem + +The fixed finite bilinear-certificate construction in literature/BOUNDARY-TRANSFER.md has the expected O(W^log_r(m)) scalar count and a polynomial-in-W amplification bound. Because the algorithm is bilinear, along a path at most one data-data multiplication occurs; recursively formed linear inputs and linear recombination give O(H+P+log W) precision for fixed coefficient data. The theorem is about products, so it correctly retains the caller's matrix-inverse, pivoting and conditioning hypotheses. + +The boundary substitution c0 = (3-log_r(m))/2 matches the actual W_band = O(sqrt(p) polylog(p)) tariff. Strassen's inequality 7^125 < 2^351 gives the conservative c = 12/125. The generalized parameter proof with delta <= (1/2-c)/4 preserves xi > 1/2. For q > 1/3 the fused row must be bounded by q-delta*(3q-1), rather than asserted to exceed q; the written proof supplies a sufficient strict bound. The remaining eight rows still exceed the target. This extends a sufficient interface and does not improve the present much smaller provider-limited value by itself. + +For publication clarity, the coefficient preparation hypothesis should explicitly say polynomial-time approximation from fixed rational/algebraic defining data. Bare effective approximability does not imply a polynomial-time supplied approximation procedure, although fixed algebraic numbers with an explicit defining polynomial and isolating data have standard polynomial-time bit approximation. + +## DIV-free Newton lowering reviewed separately + +For nonzero d < 2^w, choose d' = d*2^s in [2^(w-1),2^w), a = d'/2^w, B = 2^(4w), A = d'*2^(3w). The integer iteration X' = floor((2B^2 X-A X^2)/B^2), starting X = B, is downward-rounded reciprocal Newton. Its invariants are 1 <= X/B <= 1/a and 0 <= e = 1-aX/B <= 1/2. It satisfies e_next <= e^2+1/B. Comparing with the exact sequence a_j = 2^(-2^j), both terms stay at most 1/2, so the squaring map is 1-Lipschitz on the interval and e_j <= a_j+j/B. For k = ceil(log2(4w)), e_k <= (k+1)*2^(-4w) <= 2^(-2w). Therefore t = floor(n*2^s*X/2^(5w)) is floor((n/d)*(1-e)); it underestimates floor(n/d) by at most one. Test n-t*d >= d for the unique possible correction. All subtraction numerators are nonnegative and all temporaries have O(w) bits; the full-word product is lowered using half-word products to a fixed number of native limbs. Zero divisor and finitely many tiny widths need explicit base cases. + +Model boundary: the actual Lax13 instruction set has primitive left shift only; its published right shift uses division. The DIV-free strengthening explicitly targets a standard Word RAM with both logical shifts primitive, rather than claiming the same Lax13 machine with DIV deleted; this model boundary is retained in the root proof. Normalization can find the leading bit in O(log w) comparisons and shifts. Word-width discovery may be paid once at setup. All online divisions can then be replaced by O(log w) such native operations; this adds a polylog(p) factor absorbed by the existing strict exponent margins. This is classical reciprocal division reused constructively, not a new reciprocal algorithm. + +Independent arithmetic regression `check_newton_review.py` checks all 86868 quotient pairs at widths 2 through 8, plus 2160 larger cases at widths through 1024. Every Newton round additionally checks the reciprocal and error invariants using cross-multiplied exact integers. All checks passed under -I -O -B. This is independent executable component evidence, not a replacement for the universal proof or native lowering. diff --git a/research/native-wordram-tightening/formal/PUBLIC-SOURCE-PINS.json b/research/native-wordram-tightening/formal/PUBLIC-SOURCE-PINS.json new file mode 100644 index 0000000000..d5bafd193e --- /dev/null +++ b/research/native-wordram-tightening/formal/PUBLIC-SOURCE-PINS.json @@ -0,0 +1,143 @@ +{ + "schema": 1, + "scope": "Canonical Mathproof-relative discovery provenance. These local source snapshots were inspected, not freshly compiled; no absolute machine paths or identifying filesystem metadata are included. They are precedents for the informal lemmas, not portable build dependencies.", + "files": { + "Mathproof/Meta/Problem18RAMLax13Ram20261001.lean": { + "sha256": "b95844098a3c402ec895c542d07a4b60354455cf66fe77bad1050d15583ec948", + "bytes": 13687, + "evidence": "SOURCE_INSPECTION_ONLY", + "declarations": [ + { + "name": "Instr", + "line": 144 + }, + { + "name": "Instr.effect", + "line": 212 + }, + { + "name": "step", + "line": 272 + }, + { + "name": "RunsTo", + "line": 292 + } + ] + }, + "Mathproof/Meta/Problem18RAMLax13ProofsCompile20261001.lean": { + "sha256": "bc2237188b9b7c6f4d5524bad17d353bab873ab693ddb2e947574739dc2aae2c", + "bytes": 22016, + "evidence": "SOURCE_INSPECTION_ONLY", + "declarations": [ + { + "name": "Layout", + "line": 75 + }, + { + "name": "Layout.FitsWords", + "line": 107 + }, + { + "name": "Layout.arrAddr", + "line": 93 + }, + { + "name": "Layout.span", + "line": 98 + }, + { + "name": "arrAddr_inj", + "line": 425 + } + ] + }, + "Mathproof/Meta/Problem18RAMLax13ProofsSimulation20261001.lean": { + "sha256": "2db5af757e7808c62ac1b578a26e198532c24b17388a06719c127f08de23811c", + "bytes": 51699, + "evidence": "SOURCE_INSPECTION_ONLY", + "declarations": [ + { + "name": "Represents", + "line": 56 + }, + { + "name": "Reaches", + "line": 70 + }, + { + "name": "compile_correct", + "line": 544 + }, + { + "name": "compileProgram_runsTo", + "line": 896 + } + ] + }, + "Mathproof/Meta/Problem18IMPWordBounds20261001.lean": { + "sha256": "71f52fba1c2c1af482c55dcd54a6da5c20fea8cff4336cb3dac572a37905bb4f", + "bytes": 1766, + "evidence": "SOURCE_INSPECTION_ONLY", + "declarations": [ + { + "name": "layoutFitsWords", + "line": 8 + } + ] + }, + "Mathproof/Meta/Problem18IMPUniformCompiler20261001.lean": { + "sha256": "7d62ae5e1c80f8c93d5aad9a2c754560344e597000ca96be6fc3389c8d1e3627", + "bytes": 2919, + "evidence": "SOURCE_INSPECTION_ONLY", + "declarations": [ + { + "name": "wordBound", + "line": 8 + }, + { + "name": "compileProgram_runs_polynomial", + "line": 14 + } + ] + }, + "Mathproof/Meta/Problem18Claude/Problem18ClaudeFieldMacros20261001.lean": { + "sha256": "dfbfb862c94fe8e1057d80eeb37f719abd8ce77f0b9391cc333efebb1fecf71b", + "bytes": 10855, + "evidence": "SOURCE_INSPECTION_ONLY", + "declarations": [ + { + "name": "MacroInput", + "line": 54 + }, + { + "name": "MacroFrame", + "line": 81 + }, + { + "name": "BinarySpec", + "line": 102 + }, + { + "name": "BinarySpec.call", + "line": 194 + } + ] + }, + "Mathproof/LibraryBridges/Claude/ThreeSumRamSimulation_20261007.lean": { + "sha256": "81c3cbdbef8a0cfe0a4bbac8672e24235f33290fef42af0772364aab3adc64da", + "bytes": 82439, + "evidence": "SOURCE_INSPECTION_ONLY", + "declarations": [ + { + "name": "sim", + "line": 730 + }, + { + "name": "runsTo_compile", + "line": 1098 + } + ] + } + } +} diff --git a/research/native-wordram-tightening/formal/check_lanes.py b/research/native-wordram-tightening/formal/check_lanes.py new file mode 100644 index 0000000000..1fad67949f --- /dev/null +++ b/research/native-wordram-tightening/formal/check_lanes.py @@ -0,0 +1,56 @@ +"""Finite regression controls for the informal all-input lane theorem.""" +import itertools, json + +def need(ok, message): + if not ok: + raise ValueError(message) + +def encode(xs, b, r): + return sum((x+b)*r**j for j,x in enumerate(xs)) + +def main(): + checks = 0 + for b in (6,12): + cmax = 3 + s = (2*(cmax+2)*b).bit_length() + r = 1 << s + domain = tuple(range(-b,b+1)) + for k in (1,2,3): + w = k*s + mask = (1 << w)-1 + rep = sum(r**j for j in range(k)) + vectors = itertools.product(domain,repeat=k) + for x in vectors: + e = encode(x,b,r) + neg = max(2*b*rep-e,0)&mask + need(neg==encode(tuple(-v for v in x),b,r),'neg') + checks += 1 + for c in (0,1,2,3): + if all(abs(c*v)<=b for v in x): + tmp=(c*e)&mask + result=max(tmp-(c-1)*b*rep,0)&mask if c else b*rep + need(result==encode(tuple(c*v for v in x),b,r),'scalar') + checks += 1 + for d in (1,2,3,6): + if all(v%d==0 for v in x): + result=(e//d+(d-1)*(b//d)*rep)&mask + need(result==encode(tuple(v//d for v in x),b,r),'division') + checks += 1 + # Independent lanes and mixed signs, with a bounded subset of y. + for y in (tuple(0 for _ in x),tuple(-v for v in x),x, + tuple((-1)**j for j in range(k))): + ey=encode(y,b,r) + if all(abs(a+z)<=b for a,z in zip(x,y)): + result=max(((e+ey)&mask)-b*rep,0)&mask + need(result==encode(tuple(a+z for a,z in zip(x,y)),b,r),'add') + checks += 1 + if all(abs(a-z)<=b for a,z in zip(x,y)): + result=max(((e+b*rep)&mask)-ey,0)&mask + need(result==encode(tuple(a-z for a,z in zip(x,y)),b,r),'sub') + checks += 1 + print(json.dumps({'status':'PASS_FINITE_REGRESSION_ONLY', + 'exact_checks':checks,'basis':'w-bit modular multiply/add, monus, integer division', + 'proof_scope':'informal universal argument in BIASED-LANE-COMPILER.md'},indent=2)) + +if __name__=='__main__': + main() diff --git a/research/native-wordram-tightening/formal/check_newton_review.py b/research/native-wordram-tightening/formal/check_newton_review.py new file mode 100644 index 0000000000..6768b6c352 --- /dev/null +++ b/research/native-wordram-tightening/formal/check_newton_review.py @@ -0,0 +1,53 @@ +"""Independent exact-integer regression of root's DIV-free reciprocal formulas. + +This checks arithmetic, not a compiler lowering or a complexity theorem. +""" +from random import Random +import json + +def need(ok,msg): + if not ok:raise ValueError(msg) + +def prepare(w,d): + need(w>=2 and 0=0,'nonnegative Newton numerator') + X=N>>(8*w) + need(B<=X and A*X<=B*B,'reciprocal invariant') + # e_j <= 2^(-2^j)+j/B, checked by integer cross products. + denom=1<<(1<>(5*w) + need(0<=n-t*d<2*d,'one-correction interval') + ans=t+int(n-t*d>=d) + need(ans==n//d,'exact quotient') + return ans + +def main(): + exhaustive=random=0 + for w in range(2,9): + for d in range(1,1<=len(program): return None + ins=program[pc];op=ins[0];a=ins[1:];mod=1<=A:break + if ins[0]=='store' and mem[ins[1]]>=A:break + sn=step(program,source,w) + for _ in range(3):target=step(q,target,w) + if sn is None: + need(target is None,'halt mismatch');checks+=1;break + need(target is not None,'early halt') + need(target[0]==1+3*sn[0],'counter') + need(target[2:]==sn[2:],'input/output') + need(all(target[1][b+i]==sn[1][i] for i in range(A)),'active cells') + need(all(target[1][i]==outside[i] for i in range(mod) + if not b<=i 12/125. The earlier c = 3/32 is smaller. Neither ceiling matters for the currently much smaller admitted supplier saving. + +If the user’s matrix-multiplication development supplies a fixed exact stable certificate with ω₀ arbitrarily close above 9/4, this interface admits any c < 3/8. A theorem stating only ω ≤ 9/4 does not by itself identify the required certificate or establish its concrete coefficient-generation/precision contract. This document does not claim that such an explicit certificate was extracted or audited here. + +## Universal native assembly for the replacement tariff + +Retain every actual supplier, analytic, all-column, stock, conditioning, coefficient-generation and recovery hypothesis in PR #4635 `NATIVE-LIFT.md`. Let its fixed provider saving be q_C > 0, and choose rational + + 0 < κ < Q := min(q_C,c), + q = (κ+Q)/2, + stop = (q_C−q)/(2q_C), + δ = min(1/100, (q−κ)/(4(q+1)), (c−q)/16, (1/2−c)/4), + ε = 1−δ, β = 1−3δ, + r_group = δ/10, layout = δ/100, + ξ = ε(1+q)−c+layout. + +The symbol r_group is the source grouping parameter, not the matrix block side r. All parameters are fixed before n grows. Then the same actual native caller multiplies packed n-bit integers in O(n / (log n)^κ) word operations. + +**Proof of every changed guard.** We have δ > 0, δ ≤ 1/100, β ≥ 97/100, 0 < q < c < 1/2, and q_C(1−stop)−q = (q_C−q)/2 > 0. The complete address-key size remains O(p^(β+1−ε) + p^β log p) = o(p), since β+1−ε = 1−2δ < 1. Thus its explicitly enumerated table costs n^o(1). The retained membership guard is 1−β−2(1−ε) = δ > 0, and 1−ε−r_group = 9δ/10 > 0. + +Since δ ≤ (1/2−c)/4, + + ξ > 1−δ−c > 1/2. + +Moreover + + ε−ξ = c−εq−layout ≥ c−q−δ/100 > 0. + +The exact chirp/conditioning slack remains + + 1−(β+2ξ−2+r_group) + = 2(c−q) + δ(122/25+2q) > 0. + +Therefore the full source analytic grouping/guard-bit arguments remain applicable. + +The nine actual native rows now have savings + + εq, + 1, + 1−ε+qβ = q+δ(1−3q), + 1, + 1−ε+β = 1−2δ, + c+ξ−ε = εq+layout, + 1/2+ξ−ε = (1/2−c)+εq+layout, + ε, + 79−ε−β. + +The first exceeds κ because δq < (q−κ)/4. For the fused row, q ≤ 1/3 gives saving at least q; if q > 1/3, its loss δ(3q−1) is less than 2δ(q+1) ≤ (q−κ)/2, so it still exceeds κ. The boundary row exceeds the main row by layout; the indexed sparse-axis row exceeds the boundary row by 1/2−c > 0. The remaining rows have savings at least 97/100 or 1, and κ < 1/2. Every row therefore has a fixed positive margin over κ. The complete coefficient and field representations have O(p) bits by the retained native bounds and the fixed-recursion precision theorem. Setup and table work are n^o(1), and source recovery remains exact. This proves the sufficient assembly. + +## Scope and attribution + +This extends a positive source-bound interface, rather than asserting a necessary condition or a barrier. It reuses the actual native algorithms and all their frozen proof obligations from Dugongue’s PR #4630 and #4635, the finite supplier/controller lineage, the Gaussian/Poisson and recovery foundations of Harvey and van der Hoeven, and Strassen’s explicit recursion. The new material is an explicit fixed-certificate precision boundary and a single universal parameter proof that permits c up to 1/2, with a correction to the fused-row comparison when q exceeds 1/3. + +There is **no current κ improvement from this boundary replacement alone**: the main simultaneous-transform row remains limited by q_C. A numerical improvement must come from a stronger actually admitted provider, or a different complete native caller whose dominant row changes. No selected-frontier update or independent audit of the inherited full multiplication theorem is claimed. diff --git a/research/native-wordram-tightening/literature/KRONECKER-NORMALIZATION.md b/research/native-wordram-tightening/literature/KRONECKER-NORMALIZATION.md new file mode 100644 index 0000000000..41d3dfb98f --- /dev/null +++ b/research/native-wordram-tightening/literature/KRONECKER-NORMALIZATION.md @@ -0,0 +1,41 @@ +# Paid OR normalization of nonzero 2 × 2 tensor factors + +Prepared for Dugongue with substantial OpenAI Codex assistance. This is an informal all-input algebraic theorem and its implementation boundary. It is not a new multiplication κ claim. + +## Theorem + +Let F be a field and let G_i = [[a_i,b_i],[c_i,d_i]] for i = 0,…,k−1, with all four entries nonzero. Set N = 2^k, t_i = a_i d_i / (b_i c_i), and + + f(z) = ∏_{i : z_i = 0} t_i for z ∈ {0,1}^k, + M_f[x,y] = f(x ∨ y). + +There are explicit invertible diagonal matrices D_out,D_in and the bit-complement permutation P on k-bit indices such that + + ⊗_i G_i = D_out P M_f P D_in. + +All diagonal values, f values and address maps can be generated in O(N + k) field/address operations, with O(N) memory and no search. Given any explicit circuit for M_f, the theorem supplies a circuit for ⊗G_i with O(N) extra field operations and O(N) moves. It computes the exact action on every input vector, including arbitrary independently initialized entries. + +## Proof and construction + +For one factor define L_i = diag(1/a_i,1/c_i), R_i = diag(1,a_i/b_i), and J = [[0,1],[1,0]]. Direct multiplication gives + + L_i G_i R_i = [[1,1],[1,t_i]], + J L_i G_i R_i J = K_i := [[t_i,1],[1,1]]. + +Consequently G_i = L_i^−1 J K_i J R_i^−1. Tensor multiplication distributes over composition, so with D_out = ⊗L_i^−1, D_in = ⊗R_i^−1 and P = ⊗J, the claimed decomposition follows from ⊗K_i = M_f. The latter identity holds entrywise: K_i[x_i,y_i] equals t_i exactly when x_i = y_i = 0 and equals 1 otherwise. The product of these entries is f(x ∨ y). This proves the identity over every field, without a characteristic restriction. + +For arbitrary nonzero factor choices α_i(0),α_i(1), generate all tensor diagonal products by starting with [1] and appending the old list multiplied by each of the two next choices. This takes at most 2(2^k−1) multiplications and writes. Apply the same recursion to f using choices [t_i,1]. Compute t_i and the one-factor inverses in O(k) operations. The bit-complement index is x XOR (N−1), so each accessed address takes O(1) ordinary word operations when k fits the address width. + +The input diagonal pass, the first permutation, the supplied M_f circuit, the second permutation and the output diagonal pass are actual operations. A caller may absorb a permutation into an existing address map, but no cost reduction is claimed unless that complete map is charged there. The O(N) bound above pays for separate passes if necessary. Distinct input/output buffers implement the construction directly. An in-place or borrowed-register contract requires the supplied M_f evaluator to satisfy that same contract; the algebra alone does not supply it. + +## Precision and scalar preparation boundary + +Suppose F = ℂ and all |a_i|, |b_i|, |c_i|, |d_i| and their reciprocals are at most 2^A for A ≥ 0. Then |t_i| ≤ 2^(4A), each f(z) has magnitude at most 2^(4Ak), entries of D_out have magnitude at most 2^(Ak), and entries of D_in have magnitude at most 2^(2Ak). The same reciprocal bounds hold for those diagonals. These follow by multiplying at most k one-factor bounds. Thus Ak = O(p) is an explicit sufficient magnitude condition for O(p) integer bits in the external factors. It does not bound the internal coefficients or intermediate amplification of the M_f circuit. + +For exact dyadic or algebraic factors, prepare and apply their values with the corresponding exact arithmetic. For approximate complex factors, use directed enclosures or an explicit straight-line perturbation bound for every multiplication, division and circuit layer. Nonzero exact entries do not alone guarantee that an approximation safely admits division. In particular the theorem does not silently equip a Word RAM with exact complex division or roots of unity. + +## Application to a newer shallow-circuit theorem + +Alman and Li, *Kronecker Powers, Orthogonal Vectors, and the Asymptotic Spectrum*, FOCS 2025, Corollary 1.1, https://arxiv.org/abs/2509.14489 , gives M_f a depth-4 circuit of size O(N^1.249424), improving the older N^1.25 shallow exponent. The reduction above identifies the exact Gaussian/tensor factors and explicitly charges the diagonals and permutations needed to use that result. The asymptotic size statement is external predecessor mathematics. Our added scope is the concrete normalizer, enumeration tariff and precision boundary, not priority for the general reduction already discussed in that paper. + +This is useful when a caller needs a shallow tensor evaluator and currently pays the older exponent. It does not beat a native O(N log N) evaluator of the same unconstrained problem, and does not improve the current multiplication κ without a changed complete caller invoice. The finite test script checks exact rational instances and rejects malformed zero-entry factors; finite tests do not replace the universal proof above. diff --git a/research/native-wordram-tightening/literature/LITERATURE.md b/research/native-wordram-tightening/literature/LITERATURE.md new file mode 100644 index 0000000000..5991cf75cf --- /dev/null +++ b/research/native-wordram-tightening/literature/LITERATURE.md @@ -0,0 +1,58 @@ +# Primary-source literature and GitHub Lean search + +Prepared for Dugongue with substantial OpenAI Codex assistance, 2026-10-22. This is a research search record, not an assertion of a new multiplication exponent or an exhaustive worldwide novelty search. + +## Correct comparison + +The native target is **O(n / (log n)^κ)** word operations on packed n-bit inputs with words of C log n bits, for a fixed sufficiently large C. It is not the multitape tariff O(n (log n)^(1−κ)). A unit instruction may multiply word-size operands; it may not multiply arbitrary n-bit operands. One can implement a fixed number of words of precision using a fixed number of ordinary word instructions. Every table and constant preparation cost remains charged. + +Fürer’s 2014 Theorems 4.1(a) and 4.2 establish O(n) integer multiplication on a log-RAM. This is an important baseline, not a new improvement over an existing native O(n / (log n)^κ) result. The source-native transfer in PR #4635 already avoids a Turing-machine simulation and explicitly pays the O(p)-bit scalar arithmetic with p = Θ(log n). + +## Primary sources inspected and actionable use + +1. Martin Fürer, *How Fast Can We Multiply Large Integers on an Actual Computer?* (2014), https://arxiv.org/abs/1402.1811 . Sections 2 and 4 specify logarithmic registers with unit multiplication and division. Theorem 4.1(a) gives the complex Schönhage–Strassen log-RAM baseline. This rules out claiming ordinary FFT word packing as a new κ mechanism. + +2. Timothy M. Chan, Ce Jin, Virginia Vassilevska Williams and Yinzhan Xu, *Faster Algorithms for Text-to-Pattern Hamming Distances*, FOCS 2023; corrected arXiv v3 dated 2024-12-19, https://arxiv.org/abs/2310.13174 . Lemma 2.2 and Appendix B supply deterministic length-L convolution over F_q in O(L log q) word operations. Their implementation uses two recursive smooth-root levels, packed finite-field arithmetic, and sublogarithmic transforms evaluated from prepared tables. The proof explicitly repairs an older incomplete extension-field shortcut. Apply this to genuinely low-modulus convolution leaves, after accounting for extension-field preparation and coefficient reconstruction. It cannot be substituted for a p-bit Gaussian evaluation merely because both computations contain convolutions. + +3. Josh Alman and Baitian Li, *Kronecker Powers, Orthogonal Vectors, and the Asymptotic Spectrum*, FOCS 2025, https://arxiv.org/abs/2509.14489 . Corollary 1.1 gives depth-4 size O(N^1.249424) for matrices f(x ∨ y), and depth-2d size O(N^(1+0.498848/d)) for even d. It applies, after explicit diagonal factors, to Kronecker products of 2 × 2 matrices. The paper confines unrestricted coefficients to one layer in this general reduction. This is a concrete alternative to using the older depth-4 N^1.25 bound in a caller that truly needs a shallow circuit. The resulting shallow bound alone does not beat an O(N log N) unrestricted-depth evaluator. + +4. Josh Alman and Kevin Rao, *Faster Walsh-Hadamard and Discrete Fourier Transforms From Matrix Non-Rigidity*, STOC 2023, https://arxiv.org/abs/2211.06459 . The reported improvements are leading constants: 23/24 for Walsh–Hadamard and 15/4 for real DFT arithmetic. Their low-rank-plus-sparse decomposition is relevant to finite-template synthesis. The constants are not a power saving in log n and must not be reported as a larger κ. + +5. David Harvey and Joris van der Hoeven, *Integer multiplication in time O(n log n)*, Annals of Mathematics 193 (2021), 563–617, https://annals.math.princeton.edu/2021/193-2/p04 . Gaussian resampling, multidimensional power-of-two transforms and the original analytic precision/recovery foundations are predecessor work. Their native bit-complexity theorem is a multitape theorem; any word-RAM improvement needs an independently charged implementation. + +6. David Harvey, Joris van der Hoeven and Grégoire Lecerf, *Even faster integer multiplication* (2014/2016), https://arxiv.org/abs/1407.3360 . Recursive short multiplication and coefficient-ring choices distinguish a valid short leaf from a circular multiplication oracle. Calling an existing algorithm on a genuinely smaller integer does not make its charged cost zero. + +7. David Harvey and Daniel S. Roche, *An in-place truncated Fourier transform and applications to polynomial multiplication* (2010), https://arxiv.org/abs/1001.5272 . Truncation and in-place storage reduce padding/workspace in an actual transform implementation. They do not by themselves improve the dominant simultaneous Gaussian exponent. + +8. Leslie Greengard and John Strain, *The Fast Gauss Transform*, SIAM J. Sci. Stat. Comput. 12 (1991), 79–94, https://doi.org/10.1137/0912004 ; author PDF https://math.nyu.edu/~greengar/fgt_1991.pdf . Hermite/Taylor separation gives linear work with a precision-dependent constant in fixed dimension. Integer recovery needs errors exponentially small in p. The dependence on precision, dimension and signed input norm must be retained; quoting fixed-tolerance linear time is insufficient. + +9. Nir Ailon, *An n log n Lower Bound for Fourier Transform Computation in the Well Conditioned Model* (2014), https://arxiv.org/abs/1403.1307 ; *Paraunitary Matrices, Entropy, Algebraic Condition Number and Fourier Computation* (2016), https://arxiv.org/abs/1609.03278 . These lower bounds concern restricted conditioning models, not all native algorithms. They identify why a numerical lowering requires intermediate amplification data, rather than only an exact endpoint identity. + +10. Rezaul Chowdhury, Francesco Silvestri and Flavio Vella, *A Computational Model for Tensor Core Units* (2019), https://arxiv.org/abs/1908.06649 . The model grants matrix-unit operations beyond an ordinary scalar Word RAM. GPU or tensor-core timings can guide a search but are not a scalar RAM complexity proof. + +## Concrete mechanisms nominated + +**A. Two-level tabulated low-modulus convolution.** Use the corrected finite-field algorithm in item 2 for low-modulus exact polynomial leaves. The complete replacement cost includes reduction, field construction, tables, reconstruction and output. No reviewed native caller binding was produced here; in the PR #4635 ledger the global-precision record-product row is already subdominant, so replacing that row alone does not improve κ. + +**B. OR-normalized Kronecker circuits with one unrestricted layer.** The constructive normalization lemma in `KRONECKER-NORMALIZATION.md` proves that every all-nonzero 2 × 2 tensor factor reduces to the f(x ∨ y) family with two paid diagonal passes and two coordinate flips. This gives a direct applicability test for the newer Alman–Li shallow circuit theorem. An improvement needs an actual caller whose charged shallow exponent changes; it does not follow from comparing isolated circuit sizes. + +**C. Hermite/Taylor Gaussian separation.** This is relevant only when the exact physical kernel is an ordinary Euclidean Gaussian sum satisfying the source’s separated-box hypotheses. A Boolean/symplectic Gaussian operator is not automatically such a sum. No precision-uniform bound improving the native simultaneous transform was proved here. + +## GitHub Lean inspection + +`LEAN-SOURCE-PINS.json` records exact commit, file URL, SHA-256, byte length and observed declaration headers for eight files from four repositories. No Lean process, kernel replay or axiom audit was run in this session. The inspection supplies reusable interfaces, not accepted proof evidence for a new complete theorem. + +- `openai/math` at `1581d4cbdd69a0faf34b2089614fe2a814316a6a`: `lean/ComparatorChallenges/UniformFourier.lean` states exact scalar/index RAM goals. Its complex scalar type is ℂ; only integer peaks are polynomially bounded. The comparator endpoints use `sorry` as challenge statements. This is not the implementation proof file and its placeholders must not be described as a discovered defect in the implementation. The repository’s scope note explicitly excludes a bit-precision claim. The recursive Git tree API response was truncated; no full-tree completeness claim is made. +- `Verified-zkEVM/CompPoly` at `1cb8f5cd0e22a8c9ec165000915c21d0f8e12525`: actual source includes `additiveNTT_correctness`, `computableAdditiveNTTFast_eq_additiveNTT`, `NTTFast.safeFastMul_eq_mul`, and `NTTFast.withFallback_eq_mul`. These can ground exact finite-field leaf semantics and domain-fit conditions. They do not supply the required scalar word-operation complexity theorem merely by being executable Lean. +- `BlueFatWhale/flpoint` at `d5c0fa90c69c36f794f176c96f2dd4d293bb5aa3`: `matVec_backward_error` and `matVec_error_bound` use an abstract `FPModel`. They support compositional error proofs but do not establish a concrete word format’s rounding or overflow contract. +- `alerad/leancert` at `f704278b3ed525ab5dc80b2ce9545c9b8047ec30`: concrete dyadic source has directed-rounding and normalization inequalities, including `toRat_shiftDown_le`, `toRat_shiftUp_ge`, `toRat_normalizeDown_le`, and `toRat_normalizeUp_ge`. These are useful precedents for checked coefficient enclosures. No asymptotic runtime transfer is inferred from them. + +## Overlap and coverage limits + +The current source-bound native transfer and recent PR bodies were read through the coordinating worker’s frozen `frontier/` artifacts, including PR #4635 `NATIVE-LIFT.md`. Historical main packages `word-precision53`, `chirp-packed-correlation-audit`, and `central-factor-packed` were read to distinguish directed dependencies, correlation guard bits, and exact packed verification from new mechanisms. Main’s selected result is #4470 with inherited precision/analytic obligations. Existing tensor/lookup mechanisms already receive explicit credit in #4635; no claim is made that the literature concepts above have never appeared in any of the thousands of historical PRs. + +Searches covered integer multiplication/log-RAM, packed complex arithmetic and precision, modular convolution and extension fields, shallow Kronecker circuits and matrix non-rigidity, Gaussian resampling/Hermite separation, tensor-core model changes, and public Lean FFT/NTT/rounding code. Exact query strings are in `SEARCH-QUERIES.json`. Search-engine indexing and the truncated openai/math tree limit coverage. Only primary papers and repository-owned sources support mathematical assertions; incidental third-party search results were not used as theorem evidence. + +## Conclusion of this leaf + +No independently verified superior native κ was produced by the literature leaf. The positive reusable result is the all-input diagonal/flip normalization with full operation and error accounting; the two leading mechanisms have explicit applicability tests. The coordinating worker must bind any claimed κ improvement to an actual changed paid supplier or charged native caller, rather than relabel known O(n) RAM multiplication or a local constant saving. diff --git a/research/native-wordram-tightening/literature/SEARCH-QUERIES.json b/research/native-wordram-tightening/literature/SEARCH-QUERIES.json new file mode 100644 index 0000000000..b0ed9b6b60 --- /dev/null +++ b/research/native-wordram-tightening/literature/SEARCH-QUERIES.json @@ -0,0 +1,49 @@ +{ + "date": "2026-10-22", + "queries": [ + "integer multiplication log RAM F\u00fcrer O(n) word RAM FFT multiplication instructions", + "integer multiplication word RAM O(n log n / log log n) Harvey van der Hoeven", + "packed FFT word RAM integer multiplication precomputation circuit uniformity", + "Martin Furer log RAM integer multiplication 2014 arxiv", + "integer multiplication word RAM packed arithmetic O(n) Furer log RAM depth cost", + "site:github.com/CrocSwap/integer-mult-bounds \"log-RAM\"", + "site:github.com/CrocSwap/integer-mult-bounds \"packing\" \"Word\"", + "site:github.com Lean FFT integer multiplication BitVec word RAM", + "site:github.com lean4 FFT FastFourierTransform arithmetic verified", + "site:github.com/CrocSwap/integer-mult-bounds \"F\u00fcrer\"", + "site:github.com/CrocSwap/integer-mult-bounds \"linear\" \"RAM\"", + "\"integer multiplication\" \"word RAM\" \"sublinear\"", + "\"Fourier\" \"sublinear\" \"word RAM\" multiplication", + "\"integer multiplication\" \"log-RAM\" \"o(n)\"", + "\"Fourier circuits\" \"conditioning\" Morgenstern Ailon bounded coefficient", + "integer multiplication packed FFT Word RAM Harvey Roche precomputed table polynomial multiplication", + "Alman Rao 2023 DFT non rigidity FFT stable algorithm coefficients bounded", + "Ailon 2014 FFT well conditioned computation lower bound log condition number", + "site:github.com/openai/math \"precision\" \"Fourier\" \"depth\"", + "simultaneous Gaussian transform integer multiplication batched Gaussian resampling fast rectangular matrix multiplication", + "Harvey van der Hoeven Gaussian resampling matrix multiplication simultaneous transforms algorithm", + "FFT word RAM lookup tables \"log\" \"batch\"", + "packed polynomial multiplication \"word RAM\" deterministic", + "\"integer-mult-bounds\" \"Chan\" \"Jin\"", + "\"integer-mult-bounds\" \"Alman\" \"Li\"", + "\"integer-mult-bounds\" \"Four Russians\"", + "\"integer-mult-bounds\" \"bit-packed\"", + "site:github.com/leanprover-community/mathlib4 \"fastFourierTransform\"", + "site:github.com/leanprover-community/mathlib4 \"fft\" \"Polynomial\"", + "site:github.com/openai/math \"UniformFourier.lean\"", + "site:github.com \"Lean\" \"WordRAM\" multiplication", + "Greengard Strain fast Gauss transform 1991 error p expansion precision Gaussian sum", + "fast Gauss transform arbitrary accuracy complexity log epsilon Hermite error bound", + "Gaussian kernel fast multipole algorithm high precision exponential convergence error uniform", + "Gaussian matrix low rank approximation high accuracy butterfly separation rank", + "\"integer multiplication\" \"word RAM\" \"2025\"", + "\"integer multiplication\" \"word RAM\" \"2026\"", + "\"Gaussian\" \"tensor\" \"integer multiplication\" algorithm", + "\"bit-packed FFT\" arithmetic precision", + "site:arxiv.org \"Kronecker\" \"linear circuits\" \"rebalancing\" 2023", + "site:arxiv.org \"rectangular matrix multiplication\" \"2024\" \"2.371\"", + "site:github.com/Verified-zkEVM/CompPoly \"ntt\" \"correct\"", + "site:github.com/alerad/leancert \"sin\" \"sound\"" + ], + "coverage": "systematic bounded search; not worldwide exhaustive; exact-string no-match is not novelty proof" +} diff --git a/research/native-wordram-tightening/literature/verify_boundary.py b/research/native-wordram-tightening/literature/verify_boundary.py new file mode 100644 index 0000000000..6215aa1f27 --- /dev/null +++ b/research/native-wordram-tightening/literature/verify_boundary.py @@ -0,0 +1,41 @@ +"""Exact arithmetic controls for the positive universal boundary transfer.""" +from fractions import Fraction as F +import json + + +def construct(c,qc,kappa): + if not (00 and 00 for s in slacks) or not all(s>kappa for s in savings): + raise ValueError("positive guard or complete-row margin failed") + return q,delta,min(s-kappa for s in savings) + + +def main(): + if not 7**125 < 2**351: + raise ValueError("Strassen rational ceiling certificate failed") + count=above_third=0; minmargin=None + for c in [F(3,32),F(12,125),F(1,4),F(3,8),F(49,100),F(499,1000)]: + for qc in [F(1,10**8),F(30217758,10**10),F(156,10**4),F(1,3),F(2,5),F(1,2),F(3,4)]: + for part in [F(1,1000),F(1,3),F(99,100),F(999999,10**6)]: + kappa=part*min(c,qc);q,delta,margin=construct(c,qc,kappa) + above_third += q>F(1,3); count+=1 + minmargin=margin if minmargin is None else min(minmargin,margin) + rejected=0 + for args in [(F(1,2),F(1,4),F(1,8)),(F(1,4),F(1,8),F(1,8)),(F(1,4),F(0),F(1,8)),(F(1,4),F(1,8),F(0))]: + try:construct(*args) + except ValueError:rejected+=1 + else:raise ValueError("strict boundary control was accepted") + print(json.dumps({"status":"PASS_FIXED_BILINEAR_BOUNDARY_TRANSFER","exact_cases":count,"q_above_one_third_cases":above_third,"rejected_boundary_controls":rejected,"minimum_nine_row_margin":str(minmargin),"strassen_exact_certificate":"7^125 < 2^351","new_kappa_established":False},sort_keys=True)) + + +if __name__ == "__main__":main() diff --git a/research/native-wordram-tightening/literature/verify_normalization.py b/research/native-wordram-tightening/literature/verify_normalization.py new file mode 100644 index 0000000000..4cbeffc897 --- /dev/null +++ b/research/native-wordram-tightening/literature/verify_normalization.py @@ -0,0 +1,66 @@ +"""Exact rational controls for the separately proved all-field normalizer.""" +from fractions import Fraction as F +from itertools import product +from random import Random +import json + + +def normalizer(factors): + if not factors or any(len(g) != 4 or any(z == 0 for z in g) for g in factors): + raise ValueError("nonempty list of all-nonzero 2 by 2 factors required") + n = 1 << len(factors) + ts = [a*d/(b*c) for a,b,c,d in factors] + left, right, values = [], [], [] + for x in range(n): + l = r = v = F(1) + for i,(a,b,c,d) in enumerate(factors): + bit = (x >> i) & 1 + l *= c if bit else a + r *= b/a if bit else 1 + v *= 1 if bit else ts[i] + left.append(l); right.append(r); values.append(v) + return left, right, values + + +def direct(factors,x,y): + ans=F(1) + for i,g in enumerate(factors): + ans *= g[2*((x>>i)&1)+((y>>i)&1)] + return ans + + +def check(factors): + left,right,values=normalizer(factors) + n=len(values); mask=n-1 + changed=False + for x in range(n): + for y in range(n): + actual=direct(factors,x,y) + supplied=left[x]*values[(x^mask)|(y^mask)]*right[y] + if actual != supplied: + raise ValueError("normalizer does not preserve complete matrix") + # Omitting complement is a meaningful wrong identity control. + changed |= actual != left[x]*values[x|y]*right[y] + return n*n,changed + + +def main(): + rng=Random(20261022); count=entries=controls=0 + domain=[F(a,b) for a in [-5,-3,-2,-1,1,2,3,5] for b in [1,2,3]] + for k in range(1,7): + for _ in range(12): + gs=[tuple(rng.choice(domain) for _ in range(4)) for _ in range(k)] + checked,changed=check(gs); entries+=checked; count+=1 + if changed:controls+=1 + rejected=0 + for i in range(4): + g=[F(1),F(2),F(3),F(5)];g[i]=0 + try:normalizer([g]) + except ValueError:rejected+=1 + else:raise ValueError("zero-entry guard accepted malformed input") + if rejected != 4 or controls < 60: + raise ValueError("controls did not exercise declared domain") + print(json.dumps({"status":"PASS_EXACT_PAID_OR_NORMALIZATION", "rational_factor_cases":count,"matrix_entries_checked":entries,"omitted_flip_controls":controls,"zero_entry_rejections":rejected,"new_kappa_established":False},sort_keys=True)) + + +if __name__ == "__main__":main() diff --git a/research/native-wordram-tightening/native-runtime/DIVISION-CHECK.json b/research/native-wordram-tightening/native-runtime/DIVISION-CHECK.json new file mode 100644 index 0000000000..a6c0785458 --- /dev/null +++ b/research/native-wordram-tightening/native-runtime/DIVISION-CHECK.json @@ -0,0 +1,7 @@ +{ + "status": "PASS_FINITE_DIVISION_IDENTITY_CHECKS", + "exact_pairs": 106868, + "omitted_correction_failures": 2546, + "invalid_inputs_rejected": 5, + "scope": "finite identities plus separate universal proof; not a complete multiplier implementation" +} diff --git a/research/native-wordram-tightening/native-runtime/DIVISION-FREE.md b/research/native-wordram-tightening/native-runtime/DIVISION-FREE.md new file mode 100644 index 0000000000..76189c671b --- /dev/null +++ b/research/native-wordram-tightening/native-runtime/DIVISION-FREE.md @@ -0,0 +1,52 @@ +# Remove unit-cost division from the native transfer + +Prepared for Dugongue with substantial OpenAI Codex assistance. Apache-2.0. + +## Sufficient theorem + +A w-bit unsigned integer division with nonzero divisor can be implemented on a native Word RAM with additions, subtractions, Boolean operations, comparisons, both primitive logical left and right shifts, and low-word multiplication, using O(log w) operations and a constant number of scratch words. Both quotient and remainder are exact. There is no Turing-machine simulation, unbounded-word multiplication, precomputed exponential table, floating point or leading-zero instruction. This is a concrete application of classical reciprocal/Newton division; no priority is claimed for that method. + +For w >= 2 and 0 <= n < 2^w, 1 <= d < 2^w, find the highest nonzero bit of d by binary search with shifts and comparisons. Put s = w - 1 - floor(log2 d), dn = d*2^s, so a = dn/2^w lies in [1/2,1). Let B = 2^(4w), A = dn*2^(3w), X0 = B, and k = ceil(log2(4w)). Evaluate exactly, k times, + + X_next = floor((2*B^2*X - A*X^2)/B^2). + +The division in this display is only a shift by 8w on a constant-limb integer. In particular it is not the division primitive being removed. Return + + t = floor(n*2^s*Xk / 2^(5w)), + if n - t*d >= d, increment t, + remainder = n - t*d. + +The final denominator is again a power of 2. Signed division uses magnitudes and the source's specified sign/rounding convention, with one conditional adjustment for floor division. If the source model defines division by zero as zero, an explicit d = 0 branch returns zero; it does not run Newton. The w = 1 cases are a fixed finite table. + +## Universal proof + +Write x_i = X_i/B and e_i = 1 - a*x_i. Exact Newton would replace x by x*(2-a*x). The displayed integer formula rounds this value downward by less than 1/B. Starting with x0 = 1, induction gives 1 <= x_i <= 1/a, and 0 <= e_i <= 1/2: the exact Newton map lies between x_i and 1/a, rounding cannot pass below the integer X_i, and e_next <= e_i^2 + 1/B <= 1/4 + 1/B <= 1/2. + +Set z_i = 2^(-2^i). We claim e_i <= z_i + i/B. The initial inequality holds. When e_i <= z_i, squaring gives the next inequality directly. Otherwise e_i + z_i <= 1, so e_i^2 - z_i^2 <= e_i - z_i <= i/B; the rounding term adds at most 1/B. Thus + + e_k <= 2^(-2^k) + k/B + <= (k+1)*2^(-4w) <= 2^(-2w). + +Here 2^k >= 4w and k <= 2w for every w >= 2, with 2w+1 <= 2^(2w). The real number before the final floor is exactly (n/d)*(1-e_k). It underestimates n/d by at most n*e_k < 2^(-w) < 1. Consequently t is either floor(n/d) or one less. The final comparison chooses the exact quotient, with 0 <= remainder < d. This proves correctness for every admissible input. + +## Exact native cost and storage + +All intermediates have O(w) bits: B has 4w+1 bits, X <= 2B, and the largest Newton numerator/product has at most 12w+O(1) bits. Store them in a fixed number of limbs, not in a unit-cost unbounded integer. Addition, subtraction, comparison and shifts on a fixed limb count use O(1) native instructions. A full product of two w-bit words is obtained by splitting them into half-word pieces and using a fixed number of low-word products, additions and carry operations. For odd widths, use smaller pieces so each piece product fits; the number remains fixed. Grade-school multiplication on the fixed limb count is therefore O(1) native instructions. Constructing the single-bit constants B and B^2 uses fixed limb initialization; no register must contain 2^w itself. + +Binary search for the leading bit costs O(log w). The k Newton updates cost O(log w); the final correction is O(1). Scratch can be placed in a separate bounded arena and the unrelated dirty memory is untouched. This strengthens the generic two-shift Word RAM used by the native assembly. It does not delete DIV from the literal Lax13 instruction set: that separate machine has primitive left shift but derives right shift using division. The two-shift model is stated explicitly and no unsupported Lax13 lowering is claimed. This is an informal algorithm and complexity proof. check_division.py uses exact Python integers to test the identities and is not itself an instruction-level implementation of the fixed-limb backend. + +For division of operands occupying at most a fixed c words, apply the same construction at conceptual width c*w, with a fixed number of actual w-bit limbs. The cost remains O(log w). This covers the retained native caller's constant-limb signed fixed-point arithmetic. Offline polynomial-sized rational constructors may instead retain binary long division implemented by shifts and subtractions; their polynomial setup remains n^o(1). + +## Composition with the actual nine-row native invoice + +The inherited native algorithms in PR #4630 and #4635 use bounded-word MUL/DIV. Replace every online DIV by the construction above, keeping all other operations and the actual source Gaussian/provider contracts. If a row has bound O(T*p^(1-saving)*polylog(p)), w = O(p), this adds at most another O(log p) factor. Every saving is strictly larger than the target kappa in NATIVE-TRANSFER.md. For fixed positive eta, any fixed power of log p is O(p^eta); spend at most half the smallest proved margin on all these factors. Thus the complete bound remains + + O(n / (log n)^kappa), + +now without a division instruction. This preserves, rather than increases, the numerical kappa established by the new source-bound transfer. It is a stronger instruction-set conclusion. The inherited all-fiber, compiler, precision, analytic and recovery premises remain explicit; this proof does not discharge them. + +## Attribution and evidence + +The reciprocal-division literature includes Torbjorn Granlund and Peter L. Montgomery, Division by Invariant Integers using Multiplication, PLDI 1994, https://doi.org/10.1145/178243.178249 and https://gmplib.org/~tege/divcnst-pldi94.pdf; Niels Moller and Torbjorn Granlund, Improved Division by Invariant Integers, https://gmplib.org/~tege/division-paper.pdf. Those papers address efficient reciprocal-based sequences; this document supplies its own conservative all-divisor Newton error proof and binds its O(log w) tariff to the current native rows. Credit the native and mathematical predecessor owners listed in README.md. No claim that this classical method has never appeared elsewhere in the repository is made. + +The finite check exhausts all numerator/divisor pairs for widths 2 through 8 and tests deterministic wide cases through 512 bits, checks the one-correction invariant, rejects malformed bounds, and demonstrates failures when correction is omitted. The all-input result is the proof above, not an inference from these tests. diff --git a/research/native-wordram-tightening/native-runtime/check_division.py b/research/native-wordram-tightening/native-runtime/check_division.py new file mode 100644 index 0000000000..ee0ee65f8e --- /dev/null +++ b/research/native-wordram-tightening/native-runtime/check_division.py @@ -0,0 +1,54 @@ +"""Exact finite checks for the informal division-elimination theorem; Apache-2.0. +Dugongue with substantial OpenAI Codex assistance. Python integers verify the +identities; they are not a unit-cost arbitrary-precision machine model. +""" +import random,json + +def need(ok,why): + if not ok:raise ValueError(why) + +def divide(n,d,w,correct=True): + need(w>=2 and 0<=n<(1<>1 + if d>>mid:lo=mid + else:hi=mid + s=w-1-lo;dn=d<=0,'Newton numerator') + X=numerator>>(2*q) + need(B<=X and A*X<=B*B,'reciprocal interval') + err_num=B*(1<=0 and (err_num<<(2*w))<=B*(1<>(w+q) + need(t*d<=n<(t+2)*d,'one-correction bound') + if correct and n-t*d>=d:t+=1 + return t,n-t*d + +def main(): + checks=0;corrections=0 + for w in range(2,9): + for d in range(1,1<0,'omitted-correction mutant must fail') + rejected=0 + for n,d,w in [(0,0,32),(-1,1,32),(1<<32,1,32),(1,1<<32,32),(1,1,1)]: + try:divide(n,d,w) + except ValueError:rejected+=1 + need(rejected==5,'input controls') + print(json.dumps({'status':'PASS_FINITE_DIVISION_IDENTITY_CHECKS','exact_pairs':checks,'omitted_correction_failures':corrections,'invalid_inputs_rejected':rejected,'scope':'finite identities plus separate universal proof; not a complete multiplier implementation'},indent=2)) +if __name__=='__main__':main() diff --git a/research/native-wordram-tightening/sources/PR4630-NATIVE-ASSEMBLY.md b/research/native-wordram-tightening/sources/PR4630-NATIVE-ASSEMBLY.md new file mode 100644 index 0000000000..93116735b7 --- /dev/null +++ b/research/native-wordram-tightening/sources/PR4630-NATIVE-ASSEMBLY.md @@ -0,0 +1,145 @@ +# Source-bound native Word RAM multiplication with saving 0.0030201655 + +## Precise claim and retained mathematical inputs + +On the standard finite-word random-access model with indexed memory, add/subtract, shifts, Boolean operations, comparison and multiplication/division of O(log n)-bit words, the constructions below give packed n-bit integer multiplication in + + O(n/(log n)^kappa), kappa=0.0030201655. + +The word-width coefficient is a sufficiently large fixed constant. This is a Word RAM claim, not a stronger multitape-TM exponent. It is conditional on the correctness of the specifically retained algebraic and analytic predecessor proofs listed next. It imports no TM algorithm or TM complexity theorem. No new unknown compiler, stability oracle, fast multiplier or unpriced coefficient instruction is a premise. + +Retain these mathematical source results: + +1. The literal all-input dyadic native identity and chronological finite compiler of PR #4470/#4483/#4532/#4535, including distinct productive fields, all paid jobs, owned scratch restoration, exact endpoint phase normalizers and the finite compiler majorant. The pinned #4535 certificate funds a fixed uniform provider saving q_C=0.0030201656 at N=2^(10^12). In particular P_leaf/W