diff --git a/research/wordram-ntt-kernel/INTEGRATION-RESULTS.json b/research/wordram-ntt-kernel/INTEGRATION-RESULTS.json
new file mode 100644
index 0000000000..f8df94a147
--- /dev/null
+++ b/research/wordram-ntt-kernel/INTEGRATION-RESULTS.json
@@ -0,0 +1,396 @@
+{
+  "status": "PASS",
+  "cases": 277,
+  "models": "Literal tcslib ISA at W=64; fixed lengths and fixed modulus; interpreted program includes setup, constant synthesis, arithmetic, carry, clearing and final accept",
+  "tests": "All single-hex-digit pairs; boundary/random cases through 1024-bit operands; dirty owned memory; operand/exterior preservation; all owned temporaries zero; independent NTT and integer product oracles; same-ABI fused vs recomputation control",
+  "records": [
+    {
+      "lengths": [
+        1,
+        1
+      ],
+      "n": 1,
+      "butterflies": 0,
+      "fused_static_instructions": 369,
+      "duplicate_static_instructions": 369,
+      "owned_temporary_words": 24,
+      "output_words": 2,
+      "comparisons": {
+        "exhaustive_256_cases": true,
+        "minimum_steps": 313,
+        "maximum_steps": 319
+      }
+    },
+    {
+      "lengths": [
+        1,
+        2
+      ],
+      "n": 2,
+      "butterflies": 3,
+      "fused_static_instructions": 726,
+      "duplicate_static_instructions": 873,
+      "owned_temporary_words": 38,
+      "output_words": 3,
+      "comparisons": [
+        {
+          "fused_steps": 563,
+          "duplicate_steps": 662,
+          "saved_instructions": 99,
+          "fused_instruction_histogram": {
+            "one": 19,
+            "sub": 204,
+            "add": 190,
+            "mul": 7,
+            "bltz": 142,
+            "accept": 1
+          }
+        },
+        {
+          "fused_steps": 583,
+          "duplicate_steps": 682,
+          "saved_instructions": 99,
+          "fused_instruction_histogram": {
+            "one": 19,
+            "sub": 204,
+            "add": 210,
+            "mul": 7,
+            "bltz": 142,
+            "accept": 1
+          }
+        },
+        {
+          "fused_steps": 571,
+          "duplicate_steps": 670,
+          "saved_instructions": 99,
+          "fused_instruction_histogram": {
+            "one": 19,
+            "sub": 204,
+            "add": 198,
+            "mul": 7,
+            "bltz": 142,
+            "accept": 1
+          }
+        }
+      ]
+    },
+    {
+      "lengths": [
+        2,
+        2
+      ],
+      "n": 4,
+      "butterflies": 12,
+      "fused_static_instructions": 1610,
+      "duplicate_static_instructions": 2198,
+      "owned_temporary_words": 71,
+      "output_words": 5,
+      "comparisons": [
+        {
+          "fused_steps": 1182,
+          "duplicate_steps": 1578,
+          "saved_instructions": 396,
+          "fused_instruction_histogram": {
+            "one": 20,
+            "sub": 496,
+            "add": 253,
+            "mul": 20,
+            "bltz": 392,
+            "accept": 1
+          }
+        },
+        {
+          "fused_steps": 1243,
+          "duplicate_steps": 1650,
+          "saved_instructions": 407,
+          "fused_instruction_histogram": {
+            "one": 20,
+            "sub": 496,
+            "add": 314,
+            "mul": 20,
+            "bltz": 392,
+            "accept": 1
+          }
+        },
+        {
+          "fused_steps": 1226,
+          "duplicate_steps": 1628,
+          "saved_instructions": 402,
+          "fused_instruction_histogram": {
+            "one": 20,
+            "sub": 496,
+            "add": 297,
+            "mul": 20,
+            "bltz": 392,
+            "accept": 1
+          }
+        }
+      ]
+    },
+    {
+      "lengths": [
+        3,
+        5
+      ],
+      "n": 8,
+      "butterflies": 36,
+      "fused_static_instructions": 3737,
+      "duplicate_static_instructions": 5501,
+      "owned_temporary_words": 149,
+      "output_words": 9,
+      "comparisons": [
+        {
+          "fused_steps": 2677,
+          "duplicate_steps": 3865,
+          "saved_instructions": 1188,
+          "fused_instruction_histogram": {
+            "one": 22,
+            "sub": 1206,
+            "add": 396,
+            "mul": 52,
+            "bltz": 1000,
+            "accept": 1
+          }
+        },
+        {
+          "fused_steps": 2832,
+          "duplicate_steps": 4061,
+          "saved_instructions": 1229,
+          "fused_instruction_histogram": {
+            "one": 22,
+            "sub": 1206,
+            "add": 551,
+            "mul": 52,
+            "bltz": 1000,
+            "accept": 1
+          }
+        },
+        {
+          "fused_steps": 2817,
+          "duplicate_steps": 4048,
+          "saved_instructions": 1231,
+          "fused_instruction_histogram": {
+            "one": 22,
+            "sub": 1206,
+            "add": 536,
+            "mul": 52,
+            "bltz": 1000,
+            "accept": 1
+          }
+        }
+      ]
+    },
+    {
+      "lengths": [
+        8,
+        8
+      ],
+      "n": 16,
+      "butterflies": 96,
+      "fused_static_instructions": 8689,
+      "duplicate_static_instructions": 13393,
+      "owned_temporary_words": 328,
+      "output_words": 17,
+      "comparisons": [
+        {
+          "fused_steps": 6161,
+          "duplicate_steps": 9329,
+          "saved_instructions": 3168,
+          "fused_instruction_histogram": {
+            "one": 25,
+            "sub": 2877,
+            "add": 698,
+            "mul": 128,
+            "bltz": 2432,
+            "accept": 1
+          }
+        },
+        {
+          "fused_steps": 6582,
+          "duplicate_steps": 9901,
+          "saved_instructions": 3319,
+          "fused_instruction_histogram": {
+            "one": 25,
+            "sub": 2877,
+            "add": 1119,
+            "mul": 128,
+            "bltz": 2432,
+            "accept": 1
+          }
+        },
+        {
+          "fused_steps": 6653,
+          "duplicate_steps": 10054,
+          "saved_instructions": 3401,
+          "fused_instruction_histogram": {
+            "one": 25,
+            "sub": 2877,
+            "add": 1190,
+            "mul": 128,
+            "bltz": 2432,
+            "accept": 1
+          }
+        }
+      ]
+    },
+    {
+      "lengths": [
+        16,
+        13
+      ],
+      "n": 32,
+      "butterflies": 240,
+      "fused_static_instructions": 20073,
+      "duplicate_static_instructions": 31833,
+      "owned_temporary_words": 736,
+      "output_words": 33,
+      "comparisons": [
+        {
+          "fused_steps": 14201,
+          "duplicate_steps": 22121,
+          "saved_instructions": 7920,
+          "fused_instruction_histogram": {
+            "one": 33,
+            "sub": 6725,
+            "add": 1410,
+            "mul": 304,
+            "bltz": 5728,
+            "accept": 1
+          }
+        },
+        {
+          "fused_steps": 15228,
+          "duplicate_steps": 23628,
+          "saved_instructions": 8400,
+          "fused_instruction_histogram": {
+            "one": 33,
+            "sub": 6725,
+            "add": 2437,
+            "mul": 304,
+            "bltz": 5728,
+            "accept": 1
+          }
+        },
+        {
+          "fused_steps": 15413,
+          "duplicate_steps": 24051,
+          "saved_instructions": 8638,
+          "fused_instruction_histogram": {
+            "one": 33,
+            "sub": 6725,
+            "add": 2622,
+            "mul": 304,
+            "bltz": 5728,
+            "accept": 1
+          }
+        }
+      ]
+    },
+    {
+      "lengths": [
+        64,
+        64
+      ],
+      "n": 128,
+      "butterflies": 1344,
+      "fused_static_instructions": 103751,
+      "duplicate_static_instructions": 169607,
+      "owned_temporary_words": 3712,
+      "output_words": 129,
+      "comparisons": [
+        {
+          "fused_steps": 73735,
+          "duplicate_steps": 118087,
+          "saved_instructions": 44352,
+          "fused_instruction_histogram": {
+            "one": 129,
+            "sub": 34901,
+            "add": 7280,
+            "mul": 1600,
+            "bltz": 29824,
+            "accept": 1
+          }
+        },
+        {
+          "fused_steps": 79413,
+          "duplicate_steps": 126822,
+          "saved_instructions": 47409,
+          "fused_instruction_histogram": {
+            "one": 129,
+            "sub": 34901,
+            "add": 12958,
+            "mul": 1600,
+            "bltz": 29824,
+            "accept": 1
+          }
+        },
+        {
+          "fused_steps": 81919,
+          "duplicate_steps": 131791,
+          "saved_instructions": 49872,
+          "fused_instruction_histogram": {
+            "one": 129,
+            "sub": 34901,
+            "add": 15464,
+            "mul": 1600,
+            "bltz": 29824,
+            "accept": 1
+          }
+        }
+      ]
+    },
+    {
+      "lengths": [
+        256,
+        256
+      ],
+      "n": 512,
+      "butterflies": 6912,
+      "fused_static_instructions": 507701,
+      "duplicate_static_instructions": 846389,
+      "owned_temporary_words": 17920,
+      "output_words": 513,
+      "comparisons": [
+        {
+          "fused_steps": 361525,
+          "duplicate_steps": 589621,
+          "saved_instructions": 228096,
+          "fused_instruction_histogram": {
+            "one": 513,
+            "sub": 171797,
+            "add": 34334,
+            "mul": 7936,
+            "bltz": 146944,
+            "accept": 1
+          }
+        },
+        {
+          "fused_steps": 391079,
+          "duplicate_steps": 636835,
+          "saved_instructions": 245756,
+          "fused_instruction_histogram": {
+            "one": 513,
+            "sub": 171797,
+            "add": 63888,
+            "mul": 7936,
+            "bltz": 146944,
+            "accept": 1
+          }
+        },
+        {
+          "fused_steps": 406526,
+          "duplicate_steps": 667219,
+          "saved_instructions": 260693,
+          "fused_instruction_histogram": {
+            "one": 513,
+            "sub": 171797,
+            "add": 79335,
+            "mul": 7936,
+            "bltz": 146944,
+            "accept": 1
+          }
+        }
+      ]
+    }
+  ]
+}
diff --git a/research/wordram-ntt-kernel/LICENSE b/research/wordram-ntt-kernel/LICENSE
new file mode 100644
index 0000000000..261eeb9e9f
--- /dev/null
+++ b/research/wordram-ntt-kernel/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/wordram-ntt-kernel/MANIFEST.json b/research/wordram-ntt-kernel/MANIFEST.json
new file mode 100644
index 0000000000..915d43afc7
--- /dev/null
+++ b/research/wordram-ntt-kernel/MANIFEST.json
@@ -0,0 +1,37 @@
+{
+  "algorithm": "sha256",
+  "files": {
+    "INTEGRATION-RESULTS.json": "fd866e701664a240059bdb3212898fa97fd5f5a1759e2fb84c37f07947e69d40",
+    "lean/IntegerKernelRecovery20261024.lean": "1cfed8b805c3236ae205d5774badd79118e5743fa9343ee70313083efc308e9a",
+    "lean/STATUS.json": "1b66f49217a082e44d56e97f7ce8e6edc9f3199ffec23cb6b168e9bd26672361",
+    "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4",
+    "NOTICE.txt": "c7a35a43ceeca4d0b820c00e5b3c589d119033748a46de91769f284e869ac33b",
+    "ntt/CATCRYPT-LICENSE.txt": "1ae0577444a82462c225f35a8cbd770e449ef4507e58f8638e5f121b6238712a",
+    "ntt/exact_ntt.py": "b512200d63c736c5d347247028eb1b1f3431cea44aba01c86f2772910d6b41bf",
+    "ntt/MANIFEST.json": "2cb299d5166af9ea5a849e23af64f92f137a1ae0da5fd85ae83581dce67a9a61",
+    "ntt/NTT-APPLICATION.txt": "09ed4367c0808d786c6a9ca9e552bc4592da1da16b66ffa60812c6a2dd65753a",
+    "ntt/sources.json": "b7ddef8bb58bdcf2c6a5029826291c83dc7492e2b06cbfb66cf0828e7ad017e4",
+    "ntt/TEST-RESULT.json": "16e4463688fd7b08a8056e842e78baeb24091a11136ac2899984d2cd938f6a92",
+    "ntt/test_exact_ntt.py": "e2fcd058685ab49f2cec71f806563888452ee5dce6b696e04b0ef0ea84687123",
+    "PROOF.txt": "f1d6549b55337e6704b575806fb6be6cec8bbc9a761a6bf3a320aec40cbee9df",
+    "ram/circuit-verification.json": "d7423872b05db58c6157930f9f89ffd5bf36e0059ed51a4a8739900a4ece5d7d",
+    "ram/circuit_sharing.py": "0eadf9ef954c5d97aa5e5f0949b6bf90ecb90fbb9d0321f472b2c6e97140c24f",
+    "ram/PROOFS.txt": "e62d76c0caaa4e24651d2282a7a19cb935c63e16932c90a14cb74182d3934df8",
+    "ram/sources.json": "329ce129c36e78d93710104864a94eb0ed1918733e78fd2fcde96ab7f5b58929",
+    "ram/verification.json": "8d3efbc0916af425143ae6bd5bd94bb9d70ac72d1de2b920a3b2d4bcc9e3b46b",
+    "ram/verify_wordram.py": "02b2c09ff1542e6f947aedaad67c9a1872ed0098a447b71076cfbfe14373efbb",
+    "ram/wordram_kernel.py": "b1a6133e505e5faf5832a5274eea23f96b033257c3d16cc24479c4a4c7059a2e",
+    "ram_multiplier.py": "6c3ae23ad90c92741f5a505ae9dd85a4bbaaafb72ebdf50291e07d1ae4c52476",
+    "README.md": "23084a8deb72003a42d79e01816f2275e9f38d8250e2ad411fed74a1e6d7bed8",
+    "recovery/fixedpoint_fft.py": "e9ffceb08684d73e9971b8be9451caefdd2836235eaf059356fc38dc43861bb6",
+    "recovery/REPORT.txt": "eff4e3bdabdf0216604493e2d768cbe9862e40c61cba21c8964d6fc339b85138",
+    "recovery/SOURCES.json": "3f29acd9aee095197f2b0829774d40ba930e1977fe9ab1a5f7efb4b2935a07c3",
+    "recovery/verification-31bits.json": "8a56a5bbe68cee7540a39e03ee041ca4fc5a6aaaa2bf39b109002c05fa0adc6b",
+    "recovery/verification.json": "3593b43218392896cbcccad591b3bfdf2fb65f1b8d1b60d1b28320ebb1134041",
+    "SOURCES.json": "3610732a3a0accd3766c92b1de904ed7a41c05970942e0fe5eb89fa697b26f7d",
+    "TASK.json": "33d03eb9b15b920ae29387a91212fcd67d3a95be81723670a5177b3b56fe612e",
+    "VERIFY.json": "a6125ea7187eaed24f883dd9600c5cef692e61d1788dabd82d8a521333870a58",
+    "verify.py": "84283f0581ed63f099a453be34e8d615d90a3ca5dd6f24cdc4a38d93710e594a",
+    "verify_integration.py": "ef0f3721a9db3f96985f11f446e7bb0bd9c8e20763344c30e4b39f57cbcaaea5"
+  }
+}
diff --git a/research/wordram-ntt-kernel/NOTICE.txt b/research/wordram-ntt-kernel/NOTICE.txt
new file mode 100644
index 0000000000..b0dc94cb9d
--- /dev/null
+++ b/research/wordram-ntt-kernel/NOTICE.txt
@@ -0,0 +1,3 @@
+Original bounded-kernel integration prepared for Dugongue with substantial OpenAI Codex assistance. Apache-2.0. Reusable mathematical/formal interfaces retain all upstream credit listed in SOURCES.json and README.md. CatCrypt source attribution and MIT notice are retained in ntt/. No complete upstream library is vendored.
+
+The base Word RAM semantics retain Anthropic, PBC / anthropics/formal-math [AFM26], `3sum-apsp/EndStatement.lean` at `e1a4e6508154ea59f030480661590a9fe3018011`, as attributed in tcslib’s source header.
diff --git a/research/wordram-ntt-kernel/PROOF.txt b/research/wordram-ntt-kernel/PROOF.txt
new file mode 100644
index 0000000000..d0d0d6486e
--- /dev/null
+++ b/research/wordram-ntt-kernel/PROOF.txt
@@ -0,0 +1,38 @@
+BOUNDED INTEGER MULTIPLICATION: SUFFICIENT ASSEMBLY AND COST PROOF
+
+1. Frozen scope and computation model.
+Fix 1<=s,t<=256, hexadecimal digits a_i,b_j in {0,...,15}, p=65537 and N the least power of two >=s+t-1. Thus N<=512. Input words occupy addresses 1000+i and 2000+j; output words 3000..3000+N. The owned temporary region is exactly the generated fresh addresses >=10000 plus the explicitly reserved scratch set. Regions are disjoint. Arbitrary other memory, including negative signed addresses, is permitted. Initial owned words can be dirty.
+The machine uses 64-bit modular words, signed comparison against zero, direct arithmetic operands and a charged halt. Word multiplication is unit cost by this explicitly chosen model; full arbitrary-size multiplication is not a primitive. The program generator uses only lengths and fixed field constants, never input digits. It creates a fixed finite program for each pair of lengths; its generation is not claimed as free work in an all-size algorithm.
+
+2. Prime and roots.
+The concrete checker tests primality by trial divisors through floor(sqrt(p)); every integer in that finite exhaustive divisor interval is checked, so a passing test is a primality certificate by the elementary least-prime-factor argument. For each actual N it sets omega=3^((p-1)/N) mod p and checks omega^N=1 and, if N>1, omega^(N/2)!=1. Since N is a power of two, these two conditions imply exact order N: every proper divisor of N divides N/2. N=1 is direct. Hence geometric-sum orthogonality and division by N are valid in F_p.
+
+3. No wrap and unique coefficients.
+Extend both digit vectors by zero to N. Ordinary product coefficients c_k=sum_{i+j=k}a_i b_j satisfy 0<=c_k<=225 min(s,t)<=57600<p. Any nonzero term has i+j<=s+t-2<N. Thus cyclic convolution has no wrap and equals the ordinary convolution, with zero tail. DFT/product/inverse computes those coefficients modulo p, by finite geometric-sum orthogonality; the least residue is exactly c_k because it is already in [0,p). The iterative positive-exponent transform has the radix-2 invariant given in ntt/NTT-APPLICATION.txt. Precomputed twiddles in the fixed program match those powers; their runtime binary literal synthesis is charged. Inverse twiddles and the final N inverse are likewise validated constants.
+
+4. Literal modular multiply.
+For x,y in [0,65536], z=xy<=2^32. The program starts with a single actual word multiplication, which is exact at W = 64. Setup constructs p,2p,...,2^15 p. Since z<p*2^16, descending greedy tests/subtractions leave z mod p: before testing 2^j p the invariant is 0<=r<2^(j+1)p; after conditionally subtracting that threshold, 0<=r<2^j p. At j=0 the result is in [0,p). A negative tentative subtraction is recognized by signed bltz; all magnitudes are below 2^33, so wrapped negative words have the intended signed meaning and no positive value crosses 2^63. Each selected quotient bit executes one extra copy. Therefore the isolated multiplication block costs33+popcount(floor(xy/p)) instructions, between 33 and49, excluding shared setup/cleanup. See ram/PROOFS.txt for the literal instructions and frame details.
+
+5. Shared butterfly and whole transform.
+Compute v=b*w mod p once. Then plus=u+v reduced once and minus=u+p-v reduced once both lie in [0,p). This yields the two required radix-2 outputs. No input is modified. A pair of fresh output cells is allocated per butterfly. Induction over the literal assembled blocks gives exactly the mathematical NTT states at every stage, for every valid input. Pointwise products and N-inverse scaling use the same proved modular multiply. Every prior non-output value remains in a known owned cell until the explicitly charged final clearing, so no missing liveness or erasure premise is assumed.
+
+6. Carry normalization without hidden division.
+The ordinary finite distributive identity gives sum_k c_k16^k = A*B. Maintain carry h<=15 min(s,t)<=3840, initially 0. Then c_k+h<=240 min(s,t)<=61440. The program obtains quotient and remainder on division by 16 via greedy subtraction of16*2^j for j=11,...,0, accumulating the selected2^j in the quotient. The same descending invariant proves 0<=remainder<16 and c_k+h=16*nextCarry+remainder; every operation is an actual allowed ISA instruction. The carry bound is preserved because floor((225m+15m)/16)=15m. Weighted telescoping proves product value is preserved. The final remaining carry is<16 because A*B<16^(s+t)<=16^(N+1); it is emitted as the final output word, allowing a leading zero. The actual program therefore emits normalized base-16 digits representing A*B, including the N=1 case.
+
+7. Exterior/input preservation and cleanup.
+Every written address is either a known output, a generated temporary or reserved scratch. Inputs never overlap these regions. Each temporary is assigned before being read, so its initial dirty value is irrelevant. After outputs have been copied, each generated temporary is set to zero by its own subtraction instruction, and all reserved scratch is similarly zeroed; setup had set the distinguished zero cell to zero. All these instructions are counted. Thus inputs and arbitrary exterior words are unchanged, all owned intermediates are zero, outputs are correct, and final accept is executed. These assertions describe the concrete program, not an assumed clean memory oracle.
+
+8. Complete instruction bound.
+Let L=log2 N and B=3NL/2 (B=0 at N=1). There are B shared butterflies, each at most58 instructions; N pointwise products and N inverse scales, each49 static instructions; 3N initial transform copies; 51N carry instructions plus one final carry copy; 35 shared setup instructions; 19 scratch clears; one accept. Let C be the number of distinct synthesized constants and H their literal instruction count. The fresh temporary count is T=7N+2B+C, each cleared in one instruction. All constants are at most65536, including carry thresholds. Thus each costs at most33 instructions; there are at most N+32 distinct constants (at most N-1 nonzero root powers, an inverse scale, zero, and 24 carry thresholds/weights). Consequently:
+ static length = 60B+159N+C+H+56
+              <= 60B+193N+1144.
+All branches are forward and skip only optional copying, so executed steps never exceed static length. The exact literal template at N = 512 has C = 512,T = 17920 and 507701 static instructions. These space counts intentionally include retained states; they are not a claimed low-space implementation.
+
+9. Same-ABI savings theorem.
+The comparison program is generated identically except that every butterfly recomputes the same modular product immediately before its second output. Its state at each block boundary is unchanged, so every other branch, input, output and cleanup action has identical values. Its extra product costs33+popcount(floor(b*w/p)), where b and w are the actual local residues. Therefore the exact dynamic difference is the sum of those quantities over all B butterflies, always between 33B and 49B. It adds exactly 49B static instructions and no extra live cells. This proves a genuine fully charged same-output improvement over the specified recomputation control, not an improvement over a different optimized algorithm or the selected project kappa.
+
+10. Dyadic recovery is a separate sufficient implementation route.
+recovery/REPORT.txt proves E_next=(2+W)E+WM+delta, including twiddle/input error interaction; pointwise product error<=2ME+E^2+delta; inverse normalization divides the bound byN. Rational Machin/Taylor certificates establish actual twiddle bounds W=delta=2^(-b). For every admitted pair at N = 512, b = 31 suffices for coefficient error<1/2; b = 40 gives<.001. Strict closeness to a known integer recovers that integer under floor(x+1/2). Equality at a half unit is not sufficient and is a negative control. This does not provide a 64-bit cost bound for the approximate backend: its intermediates are explicitly multiword. Exact NTT and approximate FFT are two proved sufficient paths to the same product, not an unjustified mixture of field and rounded arithmetic.
+
+11. Evidence status and first integration boundary.
+The universal arguments above are informal. The portable verifier executes the concrete programs against independent schoolbook/packed-product oracles and checks every counted instruction, memory frame and clearing contract on its stated finite controls. Four local Lean lemmas, when independently audited, cover only strict integer recovery and elementary butterfly identities. They do not formally certify the assembler, all-input NTT program, prime/root procedure or floating transcendental bounds. Upstream Lean interfaces are exact pinned precedents, not rebuilt dependencies. The next project-specific step is one real consumer with a full paid-profile comparison; the present finite RAM comparison alone yields no new asymptotic kappa or selected-frontier change.
diff --git a/research/wordram-ntt-kernel/README.md b/research/wordram-ntt-kernel/README.md
new file mode 100644
index 0000000000..4e37ca5265
--- /dev/null
+++ b/research/wordram-ntt-kernel/README.md
@@ -0,0 +1,57 @@
+# Bounded integer multiplication with counted Word RAM execution
+
+This package applies four reviewed Lean-library interfaces to one working bounded integer-multiplication construction: tcslib's literal Word RAM semantics, FastPoly's fixed-syntax/shared-value discipline, CatCrypt's exact NTT identities, and mpfx's sufficient recovery endpoint.
+
+For every pair of unsigned inputs of at most 256 hexadecimal digits (1,024 bits each), the exact backend supplies a fixed input-independent 64-bit Word RAM instruction program producing the base-16 product. It preserves the input cells and arbitrary exterior memory and clears every owned intermediate word. The included informal proof covers all admissible inputs; executable controls independently check the implementation. The complete machine theorem is **not Lean-formalized**.
+
+## Concrete result
+
+The 512-point template has 6,912 shared butterflies, 507,701 static instructions and 17,920 owned temporary words. Every instruction runs through an interpreter of the retained tcslib ISA: `one`, `add`, `sub`, `mul`, `bltz` and final `accept`. No division, shift, FFT, modulus reduction or arbitrary-precision multiplication is smuggled in as a RAM instruction. Runtime constant construction, carry normalization and clearing are charged.
+
+For the all-15 input pair (two maximal 1,024-bit unsigned integers), the program takes **391,079 instructions**, versus **636,835** for a same-ABI control that independently recomputes each butterfly product: **245,756 fewer instructions (38.59%)**. This is a comparison with that explicit control, not with the selected project algorithm or every FFT implementation.
+
+For every admitted input pair, the same-output sharing transformation saves between `33 B` and `49 B` executed instructions, where `B = 3 N log2(N)/2`. The fused template has a uniform upper bound of `60 B + 193 N + 1,144` instructions, including setup and clearing. This is a bounded-template result, **not a new asymptotic kappa**.
+
+A separate exact-rationally certified complex fixed-point FFT backend recovers every coefficient at 31 fractional bits under its stated complete error bound; 40 bits give a bound below 0.001. Its multiword intermediates are **not** priced as single 64-bit RAM operations. Four local algebra/recovery lemmas passed a fresh Lean 4.33.0 kernel/transitive-axiom audit; only the standard propext, Classical.choice and Quot.sound axioms occur.
+
+## Apply the four sources
+
+| Source interface | Application here | Exact boundary |
+|---|---|---|
+| tcslib base Word RAM and instruction steps | Literal, fully interpreted multiply/reduce/butterfly/whole-product programs with explicit word, memory and halt contracts | We do not instantiate `compileProgram_correct`; the assembler targets the base ISA directly. No unfinished extended-RAM simulation is used. |
+| FastPoly fixed program / circuit sharing | One shared butterfly product, fixed before input values, with a same-ABI recomputation control | This applies the proof pattern. Our executed scalar products are not FastPoly nonscalar rank or the project's paid rank moment. |
+| CatCrypt convolution / general inverse / radix split | Prime-field NTT, zero padding, least-residue coefficient lifting and exact carry normalization | The Python implementation is original; upstream Lean theorems are cited and their mathematical interfaces adapted, not imported or rebuilt here. |
+| mpfx strict lattice recovery | Sufficient coefficient recovery after complete dyadic FFT error propagation, with exact twiddle certificates | The strict local endpoint and three butterfly identities passed a separate fresh Lean audit; the entire FFT and RAM implementation do not thereby become Lean-verified. |
+
+## Reproduce
+
+From this directory, on Python 3.10 or later with no third-party dependencies:
+
+```sh
+python3 -B verify.py
+```
+
+The checker validates the package hashes, runs independent transform and integer-product oracles, replays the actual RAM instructions with dirty owned memory, compares the recomputation control, and regenerates both exact-rational precision checks in memory. It does not need Git, Lean, network access, Windows, a GPU or upstream library installations. It fails under Python `-O`, because executable certificates use assertions.
+
+`PROOF.txt` gives the complete informal assembly and cost proof. `ram/PROOFS.txt`, `ntt/NTT-APPLICATION.txt` and `recovery/REPORT.txt` provide the component arguments. `INTEGRATION-RESULTS.json` and component receipts are finite evidence, not replacements for their universal arguments. `SOURCES.json` retains exact upstream revisions/hashes; `VERIFY.json` specifies this standalone replay. No global repository checker or selected record is changed.
+
+## Frontier and overlap
+
+The inspected base is `32890bc5de034ab8fc93ac88ead7279a6a416d04`. Its authoritative selected record is the conditional PR 5413 construction, with PR 5407 provider, PR 5414 companion audit and the retained predecessor lineage. This package neither discharges all five framework assumptions nor replaces that selected result.
+
+Pending PR 5443 addresses owned-bank lifetime/splitting, PR 5438 exact grids, PR 5451 physical operator error and PR 5442 all-width identities. This package supplies a different bounded, directly executable arithmetic kernel; it does not claim to supersede those statements. Updated open-PR titles/bodies were screened for overlap, not exhaustively mathematically audited. Standard Cooley-Tukey NTT/FFT, product sharing, base conversion and strict-half recovery are classical; no broad mathematical novelty is claimed.
+
+## Open next questions
+
+1. **Formalize the exact literal-program refinement.** Encode the assembler and prove its all-input output/frame/cost theorem against tcslib at one compatible toolchain. First bridge one butterfly and greedy reduction. Blocker: full instruction semantics are currently paper-proved and independently interpreted, rather than checked by Lean.
+2. **Lower storage without repaying the saved work.** Replace fresh per-stage cells by a proved liveness schedule. Start with one in-place stage and count load/store/clearing changes. Blocker: no same-cost lifetime refinement has yet been established; the present 17,920-word figure is explicit.
+3. **Connect an actual selected consumer.** Identify one real multiplication/recombination call whose complete bill this kernel improves, including conversions and precision. Blocker: the project's paid-rank/outer invoice differs from this fixed RAM instruction model. Only a proved complete-budget improvement would justify a kappa claim.
+4. **Extend beyond the fixed field/size.** Construct a uniform modulus/CRT or recursive blocking route, charge prime selection/table generation and word widths, and retain exact integer recovery. Blocker: the current fixed-size family alone is not an asymptotic algorithm.
+
+## Credit and license
+
+Original integration and implementations prepared for Dugongue with substantial OpenAI Codex assistance from four workers. Credit for the reusable formal interfaces belongs to Shilun-Allan-Li/tcslib, Thomas Ahle/fast-polynomials, Bas Spitters and CatCrypt-core contributors, and Brett Saiki/mpfx-lean and their credited predecessors (including Flocq/Pierre Roux for cited rounding developments). Exact pins and source hashes are in `SOURCES.json`; existing project contributor attribution remains unchanged. Original package code and prose are Apache-2.0; the retained CatCrypt MIT notice applies to that upstream source material. No whole upstream library is vendored.
+
+The base Word RAM semantics retain Anthropic, PBC / anthropics/formal-math [AFM26], `3sum-apsp/EndStatement.lean` at `e1a4e6508154ea59f030480661590a9fe3018011`, as attributed in tcslib’s source header.
+
+Local helper proof receipt: `lean/STATUS.json` binds the exact source hash and transitive axioms. The source can be checked in an existing Mathlib v4.33.0 environment with `lake env lean <path-to-this-package>/lean/IntegerKernelRecovery20261024.lean`. The supplied portable numerical replay does not install or invoke Lean.
diff --git a/research/wordram-ntt-kernel/SOURCES.json b/research/wordram-ntt-kernel/SOURCES.json
new file mode 100644
index 0000000000..a9831371ac
--- /dev/null
+++ b/research/wordram-ntt-kernel/SOURCES.json
@@ -0,0 +1,119 @@
+{
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "usage": "External source precedents, not runtime dependencies; source files locally rehashed at acquisition/application; no vendored Lean libraries",
+  "tcslib_and_fastpoly": [
+    {
+      "repository": "Shilun-Allan-Li/tcslib",
+      "revision": "3a211c0cd7725e077637fff97931909731a3f1f4",
+      "path": "TCSlib/Programs/WordRAM/Basic.lean",
+      "sha256": "f4f498c800d0231ee7c8ac222ae162cc9de149694b07c8c5e094c93530acf1f3",
+      "url": "https://github.com/Shilun-Allan-Li/tcslib/blob/3a211c0cd7725e077637fff97931909731a3f1f4/TCSlib/Programs/WordRAM/Basic.lean",
+      "evidence": "SOURCE_ONLY_NOT_BUILT"
+    },
+    {
+      "repository": "Shilun-Allan-Li/tcslib",
+      "revision": "3a211c0cd7725e077637fff97931909731a3f1f4",
+      "path": "TCSlib/Programs/WordRAM/Steps.lean",
+      "sha256": "7bc4819544c0f0c50270c15b53746c0abf83185ed71063294a94db85a91918fa",
+      "url": "https://github.com/Shilun-Allan-Li/tcslib/blob/3a211c0cd7725e077637fff97931909731a3f1f4/TCSlib/Programs/WordRAM/Steps.lean",
+      "evidence": "SOURCE_ONLY_NOT_BUILT"
+    },
+    {
+      "repository": "Shilun-Allan-Li/tcslib",
+      "revision": "3a211c0cd7725e077637fff97931909731a3f1f4",
+      "path": "TCSlib/Programs/Light/Compiler/WholeProgram.lean",
+      "sha256": "3d2b93e17218377cf46d7447156e6423a1daec7e00be90936896ad56e3409120",
+      "url": "https://github.com/Shilun-Allan-Li/tcslib/blob/3a211c0cd7725e077637fff97931909731a3f1f4/TCSlib/Programs/Light/Compiler/WholeProgram.lean",
+      "evidence": "SOURCE_ONLY_NOT_BUILT"
+    },
+    {
+      "repository": "thomasahle/fast-polynomials",
+      "revision": "09a36b0e7a6c153462bd43b91d4a3bb7ac886bef",
+      "path": "FastPoly/Cost/Circuit.lean",
+      "sha256": "1ed86f02b9321ca5d2ef17eb860db31801fed135e4a62b7d7035acb43372db0a",
+      "url": "https://github.com/thomasahle/fast-polynomials/blob/09a36b0e7a6c153462bd43b91d4a3bb7ac886bef/FastPoly/Cost/Circuit.lean",
+      "evidence": "SOURCE_ONLY_NOT_BUILT"
+    },
+    {
+      "repository": "thomasahle/fast-polynomials",
+      "revision": "09a36b0e7a6c153462bd43b91d4a3bb7ac886bef",
+      "path": "FastPoly/Cost/MultiplicationProgram.lean",
+      "sha256": "dcd92f8086d09d4be671e295db44dbcee16761b953ed43b5b8be2b6f77adf477",
+      "url": "https://github.com/thomasahle/fast-polynomials/blob/09a36b0e7a6c153462bd43b91d4a3bb7ac886bef/FastPoly/Cost/MultiplicationProgram.lean",
+      "evidence": "SOURCE_ONLY_NOT_BUILT"
+    }
+  ],
+  "catcrypt": {
+    "sources": [
+      {
+        "repository": "spitters/CatCrypt-core",
+        "revision": "dc39071735465240b54b43db9b98335d66660d48",
+        "path": "CatCryptCore/Crypto/Lattice/CyclicConvolutionGeneric.lean",
+        "declaration": "dft_cyclicConv",
+        "line": 59,
+        "file_sha256": "c306d2780c3dbd1a46f8a4fb588ec142c4b943b548f488d185fc7cc485e09ee0",
+        "declaration_region_sha256": "d2cde7839db41588cb12883cf28ac8f47d2f0f1840316f59018f3116630846bf",
+        "declaration_hash_rule": "UTF-8 source from theorem header until next theorem or namespace end, trailing whitespace removed then LF appended; includes intervening comments",
+        "url": "https://github.com/spitters/CatCrypt-core/blob/dc39071735465240b54b43db9b98335d66660d48/CatCryptCore/Crypto/Lattice/CyclicConvolutionGeneric.lean#L59",
+        "evidence": "SOURCE_ONLY_NOT_BUILT",
+        "toolchain": "leanprover/lean4:v4.33.1",
+        "license": "MIT; CatCrypt Contributors"
+      },
+      {
+        "repository": "spitters/CatCrypt-core",
+        "revision": "dc39071735465240b54b43db9b98335d66660d48",
+        "path": "CatCryptCore/Crypto/Lattice/NTTFullInversionGeneric.lean",
+        "declaration": "idft_dft",
+        "line": 63,
+        "file_sha256": "4a9cd2b4f7e632410782aae854b63b2d9b1658b9370018f48855cc7cc9938eb5",
+        "declaration_region_sha256": "d36e213c5e7641d84aaa94aef8aa0eb8974e8c483ba93bccb49f2527833789b3",
+        "declaration_hash_rule": "UTF-8 source from theorem header until next theorem or namespace end, trailing whitespace removed then LF appended; includes intervening comments",
+        "url": "https://github.com/spitters/CatCrypt-core/blob/dc39071735465240b54b43db9b98335d66660d48/CatCryptCore/Crypto/Lattice/NTTFullInversionGeneric.lean#L63",
+        "evidence": "SOURCE_ONLY_NOT_BUILT",
+        "toolchain": "leanprover/lean4:v4.33.1",
+        "license": "MIT; CatCrypt Contributors"
+      },
+      {
+        "repository": "spitters/CatCrypt-core",
+        "revision": "dc39071735465240b54b43db9b98335d66660d48",
+        "path": "CatCryptCore/Crypto/Lattice/NTTRecursionPass.lean",
+        "declaration": "dft_even_odd_split",
+        "line": 104,
+        "file_sha256": "4404b4df84677caea3623c3dfc071af3dade3acc62eb5688bb20801844698b11",
+        "declaration_region_sha256": "635c8097025f611f0f9138067478c0a5a199a756c077933b9dcb60d2a016f190",
+        "declaration_hash_rule": "UTF-8 source from theorem header until next theorem or namespace end, trailing whitespace removed then LF appended; includes intervening comments",
+        "url": "https://github.com/spitters/CatCrypt-core/blob/dc39071735465240b54b43db9b98335d66660d48/CatCryptCore/Crypto/Lattice/NTTRecursionPass.lean#L104",
+        "evidence": "SOURCE_ONLY_NOT_BUILT",
+        "toolchain": "leanprover/lean4:v4.33.1",
+        "license": "MIT; CatCrypt Contributors"
+      }
+    ],
+    "use": "Mathematical identities and convention cross-check. Original Python implementation and informal sufficient bridge; no Lean import/build claim."
+  },
+  "mpfx_and_circuits": [
+    {
+      "repository": "bksaiki/mpfx-lean",
+      "revision": "8bd80452927ae9234fc378c07a00f2962e1e5b6f",
+      "source": "Mpfx/Rounding/Ulp.lean",
+      "sha256": "fae20b63b9d9cca472181f2f0c83d8b0146d7627a9d7835d9032a61b9e688d55",
+      "url": "https://github.com/bksaiki/mpfx-lean/blob/8bd80452927ae9234fc378c07a00f2962e1e5b6f/Mpfx/Rounding/Ulp.lean",
+      "evidence": "SOURCE_ONLY_NOT_BUILT; mathematical application, not upstream import"
+    },
+    {
+      "repository": "thomasahle/fast-polynomials",
+      "revision": "09a36b0e7a6c153462bd43b91d4a3bb7ac886bef",
+      "source": "FastPoly/Cost/Circuit.lean",
+      "sha256": "1ed86f02b9321ca5d2ef17eb860db31801fed135e4a62b7d7035acb43372db0a",
+      "url": "https://github.com/thomasahle/fast-polynomials/blob/09a36b0e7a6c153462bd43b91d4a3bb7ac886bef/FastPoly/Cost/Circuit.lean",
+      "evidence": "SOURCE_ONLY_NOT_BUILT; mathematical application, not upstream import"
+    },
+    {
+      "repository": "thomasahle/fast-polynomials",
+      "revision": "09a36b0e7a6c153462bd43b91d4a3bb7ac886bef",
+      "source": "FastPoly/Cost/MultiplicationProgram.lean",
+      "sha256": "dcd92f8086d09d4be671e295db44dbcee16761b953ed43b5b8be2b6f77adf477",
+      "url": "https://github.com/thomasahle/fast-polynomials/blob/09a36b0e7a6c153462bd43b91d4a3bb7ac886bef/FastPoly/Cost/MultiplicationProgram.lean",
+      "evidence": "SOURCE_ONLY_NOT_BUILT; mathematical application, not upstream import"
+    }
+  ]
+}
diff --git a/research/wordram-ntt-kernel/TASK.json b/research/wordram-ntt-kernel/TASK.json
new file mode 100644
index 0000000000..c1d552b810
--- /dev/null
+++ b/research/wordram-ntt-kernel/TASK.json
@@ -0,0 +1,6 @@
+{
+  "assignment": "Explicit user task: apply shortlist items1-4 with root and three agents, combine one deliverable",
+  "scope": "Bounded integer multiplication using exact NTT, counted direct Word RAM program, fixed circuit sharing and sufficient dyadic recovery",
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "outcome": "Working portable exact backend and complete instruction comparison; separate approximate sufficient backend; no new kappa claim"
+}
diff --git a/research/wordram-ntt-kernel/VERIFY.json b/research/wordram-ntt-kernel/VERIFY.json
new file mode 100644
index 0000000000..4ae0f65622
--- /dev/null
+++ b/research/wordram-ntt-kernel/VERIFY.json
@@ -0,0 +1,19 @@
+{
+  "format": "standalone source-export research package",
+  "inputs": [
+    "MANIFEST.json"
+  ],
+  "commands": [
+    [
+      "python3",
+      "-B",
+      "verify.py"
+    ]
+  ],
+  "python": "3.10+ standard library",
+  "network_required": false,
+  "lean_required": false,
+  "timeout_seconds": 120,
+  "expected": "All integrity, exact NTT, supported-ISA, complete-program and rational recovery checks pass",
+  "scope": "Paper universal argument plus finite replay; no full Lean machine verification or asymptotic kappa"
+}
diff --git a/research/wordram-ntt-kernel/lean/IntegerKernelRecovery20261024.lean b/research/wordram-ntt-kernel/lean/IntegerKernelRecovery20261024.lean
new file mode 100644
index 0000000000..1eac839250
--- /dev/null
+++ b/research/wordram-ntt-kernel/lean/IntegerKernelRecovery20261024.lean
@@ -0,0 +1,39 @@
+import Mathlib.Algebra.Order.Archimedean.Real.Basic
+import Mathlib.Algebra.Order.Floor.Ring
+import Mathlib.Data.Real.Basic
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Ring
+
+/-!
+Strict half-unit recovery and a shared butterfly endpoint.
+This module proves local algebra/recovery only; the fixed-point FFT propagation
+and the executable certificate are separate artifacts, not kernel-checked here.
+-/
+namespace Mathproof.IntegerKernelRecovery20261024
+
+/-- A strict half-unit error recovers the intended integer under floor(x+1/2).
+The strict inequality rules out tie dependence. -/
+theorem recover_integer_of_strict_half (x : ℝ) (z : ℤ)
+    (h : |x - (z : ℝ)| < 1 / 2) :
+    Int.floor (x + 1 / 2) = z := by
+  apply Int.floor_eq_iff.mpr
+  rcases abs_lt.mp h with ⟨hl, hu⟩
+  constructor <;> linarith
+
+/-- A shared product computes both outputs, for every commutative ring. -/
+theorem shared_butterfly {R : Type*} [CommRing R] (u v w : R) :
+    let t := w * v
+    (u + t, u - t) = (u + w * v, u - w * v) := by
+  rfl
+
+/-- No division or characteristic assumption is hidden in the sum law. -/
+theorem butterfly_sum {R : Type*} [CommRing R] (u v w : R) :
+    (u + w * v) + (u - w * v) = 2 * u := by
+  ring
+
+/-- The corresponding difference law preserves the one shared product. -/
+theorem butterfly_difference {R : Type*} [CommRing R] (u v w : R) :
+    (u + w * v) - (u - w * v) = 2 * (w * v) := by
+  ring
+
+end Mathproof.IntegerKernelRecovery20261024
diff --git a/research/wordram-ntt-kernel/lean/STATUS.json b/research/wordram-ntt-kernel/lean/STATUS.json
new file mode 100644
index 0000000000..c8490e586e
--- /dev/null
+++ b/research/wordram-ntt-kernel/lean/STATUS.json
@@ -0,0 +1,39 @@
+{
+  "status": "VERIFIED",
+  "sha256": "1cfed8b805c3236ae205d5774badd79118e5743fa9343ee70313083efc308e9a",
+  "theorems": [
+    {
+      "axioms": [
+        "propext",
+        "Classical.choice",
+        "Quot.sound"
+      ],
+      "theorem": "Mathproof.IntegerKernelRecovery20261024.recover_integer_of_strict_half"
+    },
+    {
+      "axioms": [],
+      "theorem": "Mathproof.IntegerKernelRecovery20261024.shared_butterfly"
+    },
+    {
+      "axioms": [
+        "propext"
+      ],
+      "theorem": "Mathproof.IntegerKernelRecovery20261024.butterfly_sum"
+    },
+    {
+      "axioms": [
+        "propext"
+      ],
+      "theorem": "Mathproof.IntegerKernelRecovery20261024.butterfly_difference"
+    }
+  ],
+  "allowed_axioms": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "error": null,
+  "seconds": 15.125,
+  "lean_version": "4.33.0",
+  "scope": "Only these four local helper theorems; full NTT/RAM correctness and floating error propagation remain informal"
+}
diff --git a/research/wordram-ntt-kernel/ntt/CATCRYPT-LICENSE.txt b/research/wordram-ntt-kernel/ntt/CATCRYPT-LICENSE.txt
new file mode 100644
index 0000000000..b724ce4a1c
--- /dev/null
+++ b/research/wordram-ntt-kernel/ntt/CATCRYPT-LICENSE.txt
@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2026 CatCrypt Contributors
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/research/wordram-ntt-kernel/ntt/MANIFEST.json b/research/wordram-ntt-kernel/ntt/MANIFEST.json
new file mode 100644
index 0000000000..6e80e0fca8
--- /dev/null
+++ b/research/wordram-ntt-kernel/ntt/MANIFEST.json
@@ -0,0 +1,34 @@
+{
+  "files": [
+    {
+      "path": "CATCRYPT-LICENSE.txt",
+      "bytes": 1078,
+      "sha256": "1ae0577444a82462c225f35a8cbd770e449ef4507e58f8638e5f121b6238712a"
+    },
+    {
+      "path": "exact_ntt.py",
+      "bytes": 5471,
+      "sha256": "b512200d63c736c5d347247028eb1b1f3431cea44aba01c86f2772910d6b41bf"
+    },
+    {
+      "path": "NTT-APPLICATION.txt",
+      "bytes": 7986,
+      "sha256": "09ed4367c0808d786c6a9ca9e552bc4592da1da16b66ffa60812c6a2dd65753a"
+    },
+    {
+      "path": "sources.json",
+      "bytes": 2940,
+      "sha256": "b7ddef8bb58bdcf2c6a5029826291c83dc7492e2b06cbfb66cf0828e7ad017e4"
+    },
+    {
+      "path": "TEST-RESULT.json",
+      "bytes": 1574,
+      "sha256": "16e4463688fd7b08a8056e842e78baeb24091a11136ac2899984d2cd938f6a92"
+    },
+    {
+      "path": "test_exact_ntt.py",
+      "bytes": 4309,
+      "sha256": "e2fcd058685ab49f2cec71f806563888452ee5dce6b696e04b0ef0ea84687123"
+    }
+  ]
+}
diff --git a/research/wordram-ntt-kernel/ntt/NTT-APPLICATION.txt b/research/wordram-ntt-kernel/ntt/NTT-APPLICATION.txt
new file mode 100644
index 0000000000..68a7dd7fb5
--- /dev/null
+++ b/research/wordram-ntt-kernel/ntt/NTT-APPLICATION.txt
@@ -0,0 +1,131 @@
+Exact NTT-to-integer multiplication application
+
+Result and scope
+For any base B >= 2, nonempty digit vectors a[0..s-1], b[0..t-1]
+with integer digits in [0,B), let N be a power of two with N >= s+t-1.
+Let p be prime, N < p, and omega in F_p have exact multiplicative order N.
+If min(s,t)*(B-1)^2 < p, then the following explicit algorithm returns
+(sum_i a_i B^i)*(sum_j b_j B^j): zero-pad both vectors to N; take their
+positive-exponent NTTs; multiply corresponding entries; take the normalized
+negative-exponent inverse NTT; lift each residue to [0,p); carry in base B.
+Signed inputs follow by applying this to absolute values and restoring the
+product of signs. This is a universal sufficient correctness theorem, with
+an informal proof below. It is not a kernel-checked new theorem or a kappa
+certificate, and does not assert a faster all-size multiplication bound.
+
+1. Zero-padding removes cyclic aliasing
+Define c_k=sum_{0<=i<s,0<=j<t,i+j=k} a_i*b_j for 0<=k<s+t-1,
+and c_k=0 through k=N-1. In cyclic convolution, every potentially nonzero
+pair has 0<=i+j<=s+t-2<N. Thus (i+j) mod N=i+j, and its residue k is
+exactly its ordinary index. Reindex the cyclic sum by these pairs; every
+ordinary pair occurs once, and all padded terms vanish. Consequently the
+length-N cyclic convolution of the padded inputs is c reduced modulo p.
+This argument includes s=t=N=1; no nonexistent negative index is used.
+
+2. Exact transform and inverse
+CatCrypt's dft_cyclicConv identifies the DFT of that cyclic convolution with
+the pointwise product of the input DFTs. Its idft_dft, over a field with
+(N:F_p)!=0, then gives the cyclic convolution exactly. Here prime p gives
+the field, and 1<=N<p discharges nonzero length. The source conventions are
+DFT(x)_k=sum_j x_j*omega^(j*k) and
+IDFT(X)_k=N^(-1)*sum_j X_j*(omega^(-1))^(j*k).
+These are exactly the signs and normalization in exact_ntt.py.
+
+3. The executable radix-2 transform computes those formulas
+Let N=2^L. First permute x into bit-reversed order. After stage h, with
+m=2^h and q=N/m, block b (0<=b<q) at offset b*m satisfies, for 0<=k<m,
+ A[b*m+k]=sum_{r=0}^{m-1} x[rev_{L-h}(b)+q*r]*omega^((N/m)*r*k).
+At h=0 this is precisely bit reversal. To pass from h to h+1, split the
+sum into even and odd r. The two previous adjacent blocks supply these two
+sums; multiplication of the odd sum by omega^((N/(2*m))*k) gives the first
+butterfly output. The second output subtracts that same term because a
+primitive even-order root in a field has omega^(N/2)=-1. This proves the
+invariant by induction, with all intermediate indices in [0,N). At h=L
+there is one block and the invariant is the DFT formula. Replacing omega by
+its inverse proves the inverse-transform formula before scaling; multiplying
+by N^(-1) supplies the specified IDFT. N=1 has no butterflies and is immediate.
+The direct quadratic DFT oracle tests this implementation independently;
+the finite tests support the code, while the induction is its informal
+universal correctness argument. This implementation has not been extracted
+from Lean or compiler-refined to Word RAM.
+
+4. Least-residue lifting recovers the integer coefficients
+For fixed k, at most min(s,t) pairs satisfy i+j=k, because either index
+uniquely determines the other. Each product is between 0 and (B-1)^2.
+Therefore 0<=c_k<=min(s,t)*(B-1)^2<p. Reduction modulo p is injective on
+[0,p), so the least nonnegative residue returned by the inverse transform
+is c_k itself. Strict inequality is essential. This asymmetric length bound
+can permit an unbalanced multiplication that a bound N*(B-1)^2 would reject.
+It does not imply the fixed modulus supports arbitrary input lengths.
+
+5. Carrying preserves value and terminates
+Set q_0=0. At position k write c_k+q_k=d_k+B*q_{k+1} by Euclidean division,
+with 0<=d_k<B. After r coefficient positions, the loop invariant is
+ sum_{k<r} c_k B^k = sum_{k<r} d_k B^k + q_r B^r.
+The induction step multiplies the Euclidean identity at r by B^r and adds
+it. After the coefficient list ends, repeatedly divide the remaining carry
+by B. Since B>=2 and q>=1 implies q div B<q, this terminates and preserves
+the same invariant. Removing leading zero digits preserves value. Finally,
+distributing the product of the two digit sums groups each pair (i,j) by
+k=i+j and gives sum_k c_k B^k. The returned digit value is therefore the
+actual integer product. Multiplying by signs proves the signed endpoint.
+
+Concrete fully explicit family used here
+p=65537, generator g=3, N a power of two with 1<=N<=65536,
+omega=3^(65536/N) modulo 65537. Trial division through 256 verifies p is
+prime; pow(3,65536,p)=1 and pow(3,32768,p)=65536. Since every proper divisor
+of 65536 divides 32768, g has exact order 65536, and omega has order N.
+The tests recompute primality and the required exact-order checks; they do
+not rely on a lookup table or a prime-selection oracle.
+
+For base 16, s,t<=256 imply coefficient bound 256*225=57600<65537 and
+N<=512. Thus all signed operands with |x|,|y|<16^256=2^1024 are handled.
+More generally min(s,t)<=291 is sufficient for coefficient lifting, provided
+the needed transform length remains <=65536. At min(s,t)=292 the generic
+bound fails (292*225=65700); the API rejects that contract rather than
+silently computing a modular product.
+
+For base 2, s,t<=32768 imply coefficients <=32768<65537 and N<=65536.
+Thus all signed operands with |x|,|y|<2^32768 are handled using this fixed
+modulus. The maximum dense all-one pair is checked independently against
+its triangular coefficient formula and Python's integer product.
+
+Paid arithmetic ledger, with explicit limits
+An N-point forward or inverse radix-2 transform has (N/2)*log2(N)
+butterflies. This implementation uses two modular products in each butterfly:
+one data-times-twiddle product and one twiddle update, including updates
+whose results are not subsequently needed. Three transforms therefore use
+3*N*log2(N) modular products; pointwise multiplication and inverse scaling
+add 2*N. For N=512 the exact instrumented total is 14848 modular products
+and 13824 butterfly additions/subtractions. There are also pow calls,
+primality checks, division/modulo, allocations, bit reversal, address/control
+operations, digit conversion and carries. These are intentionally excluded
+from Counts and MUST be included before claiming a Word RAM bound. Python
+integers and Python's pow are not bounded-word RAM instructions.
+
+A practical bounded-word interface follows from the proved ranges: residues
+are below 65537, butterfly products below 65537^2=4295098369, and a base-16
+carry is at most min(s,t)*(B-1), hence at most 3840 for s,t<=256. A 33-bit
+unsigned intermediate suffices for modular products; a 64-bit host word
+suffices for every arithmetic intermediate in that fixed kernel. Unsigned
+subtraction must be implemented as u+p-v before reduction to avoid underflow.
+Word address, instruction and compiler contracts are separate obligations.
+
+Reproduction
+Run from this directory using Python 3.10 or later:
+  python -B -m unittest -v test_exact_ntt.py
+Only the standard library is used. No native binary, OS-specific dependency,
+external package, network access or absolute source path is required.
+
+Evidence and predecessor credit
+CatCrypt Contributors, spitters/CatCrypt-core, commit
+ dc39071735465240b54b43db9b98335d66660d48, MIT, Lean 4.33.1.
+Reused mathematical interfaces: dft_cyclicConv, idft_dft and the even/odd
+radix decomposition dft_even_odd_split. sources.json records exact public
+paths, line numbers, whole-file hashes and declaration-region hashes.
+All three frozen source hashes were independently rechecked. These source
+files have not been rebuilt here and no transitive axiom audit is claimed.
+The zero-padding/lifting/carry bridge and Python implementation are original
+application work in this deliverable. The underlying transform, coefficient
+bound, radix-2 algorithm and carry arguments are standard mathematics; no
+new general NTT algorithm or literature novelty is claimed.
diff --git a/research/wordram-ntt-kernel/ntt/TEST-RESULT.json b/research/wordram-ntt-kernel/ntt/TEST-RESULT.json
new file mode 100644
index 0000000000..1771314511
--- /dev/null
+++ b/research/wordram-ntt-kernel/ntt/TEST-RESULT.json
@@ -0,0 +1,30 @@
+{
+  "command": "python -B -m unittest -v test_exact_ntt.py",
+  "exit_code": 0,
+  "test_groups": 8,
+  "finite_evidence_only": true,
+  "stdout": "",
+  "stderr": "test_all_binary_vectors_up_to_four_digits (test_exact_ntt.ExactNTTTests.test_all_binary_vectors_up_to_four_digits) ... ok\ntest_cost_instrumentation (test_exact_ntt.ExactNTTTests.test_cost_instrumentation) ... ok\ntest_dense_maximum_binary_operands (test_exact_ntt.ExactNTTTests.test_dense_maximum_binary_operands) ... ok\ntest_invalid_contracts (test_exact_ntt.ExactNTTTests.test_invalid_contracts) ... ok\ntest_random_asymmetric_and_maximal_digits (test_exact_ntt.ExactNTTTests.test_random_asymmetric_and_maximal_digits) ... ok\ntest_signed_endpoint (test_exact_ntt.ExactNTTTests.test_signed_endpoint) ... ok\ntest_transform_against_direct_dft (test_exact_ntt.ExactNTTTests.test_transform_against_direct_dft) ... ok\ntest_upper_binary_transform_length (test_exact_ntt.ExactNTTTests.test_upper_binary_transform_length) ... ok\n\n----------------------------------------------------------------------\nRan 8 tests in 1.729s\n\nOK\n",
+  "source_hash_checks": 3,
+  "source_hash_mismatches": 0,
+  "lean_checks_run": false,
+  "max_dense_binary_length_each": 32768,
+  "max_transform_length_tested": 65536,
+  "base16_maximal_cases": [
+    [
+      256,
+      256
+    ],
+    [
+      291,
+      310
+    ]
+  ],
+  "base16_256_costs": {
+    "N": 512,
+    "butterflies": 6912,
+    "butterfly_additions_subtractions": 13824,
+    "modular_products_including_twiddle_updates": 14848,
+    "includes_all_runtime_costs": false
+  }
+}
diff --git a/research/wordram-ntt-kernel/ntt/exact_ntt.py b/research/wordram-ntt-kernel/ntt/exact_ntt.py
new file mode 100644
index 0000000000..5982128975
--- /dev/null
+++ b/research/wordram-ntt-kernel/ntt/exact_ntt.py
@@ -0,0 +1,155 @@
+"""Exact zero-padded NTT multiplication; Python 3 standard library only.
+
+Original reference implementation. CatCrypt supplies the cited mathematical
+transform identities; this module is not claimed to be compiled from Lean.
+No timing here is a Word RAM or integer-mult-bounds kappa certificate.
+"""
+from dataclasses import dataclass
+from math import isqrt
+
+
+@dataclass
+class Counts:
+    butterflies: int = 0
+    twiddle_products: int = 0
+    butterfly_products: int = 0
+    pointwise_products: int = 0
+    inverse_scales: int = 0
+    # pow(), indexing, permutations and all other overhead are NOT counted.
+
+
+def is_prime(p):
+    return p >= 2 and all(p % d for d in range(2, isqrt(p) + 1))
+
+
+def validate_root(p, n, omega):
+    if not is_prime(p):
+        raise ValueError("modulus must be prime")
+    if n < 1 or n & (n - 1) or n >= p:
+        raise ValueError("length must be a positive power of two less than p")
+    if pow(omega, n, p) != 1 or (n > 1 and pow(omega, n // 2, p) == 1):
+        raise ValueError("omega must have exact order n")
+
+
+def ntt(values, p, omega, inverse=False, counts=None):
+    """Positive-exponent forward DFT; normalized inverse for inverse=True."""
+    n = len(values)
+    validate_root(p, n, omega)
+    a = [x % p for x in values]
+    j = 0
+    for i in range(1, n):
+        bit = n >> 1
+        while j & bit:
+            j ^= bit
+            bit >>= 1
+        j ^= bit
+        if i < j:
+            a[i], a[j] = a[j], a[i]
+    root = pow(omega, p - 2, p) if inverse else omega
+    width = 2
+    while width <= n:
+        wlen = pow(root, n // width, p)
+        for lo in range(0, n, width):
+            w = 1
+            for j in range(lo, lo + width // 2):
+                u = a[j]
+                v = a[j + width // 2] * w % p
+                a[j] = (u + v) % p
+                a[j + width // 2] = (u - v) % p
+                w = w * wlen % p
+                if counts is not None:
+                    counts.butterflies += 1
+                    counts.butterfly_products += 1
+                    counts.twiddle_products += 1
+        width *= 2
+    if inverse:
+        invn = pow(n, p - 2, p)
+        a = [v * invn % p for v in a]
+        if counts is not None:
+            counts.inverse_scales += n
+    return a
+
+
+def direct_dft(values, p, omega, inverse=False):
+    """Independent quadratic transform oracle."""
+    n = len(values)
+    validate_root(p, n, omega)
+    root = pow(omega, p - 2, p) if inverse else omega
+    scale = pow(n, p - 2, p) if inverse else 1
+    return [scale * sum(v * pow(root, j * k, p)
+                        for j, v in enumerate(values)) % p
+            for k in range(n)]
+
+
+def schoolbook(a, b):
+    c = [0] * (len(a) + len(b) - 1)
+    for i, x in enumerate(a):
+        for j, y in enumerate(b):
+            c[i + j] += x * y
+    return c
+
+
+def exact_convolution(a, b, base=16, p=65537, generator=3, counts=None):
+    """Recover all nonnegative coefficients, under an explicit sufficient bound."""
+    if not a or not b or base < 2:
+        raise ValueError("nonempty digit vectors and base >= 2 required")
+    if any(type(x) is not int or not 0 <= x < base for x in list(a) + list(b)):
+        raise ValueError("digits must be integers in [0,base)")
+    if min(len(a), len(b)) * (base - 1) ** 2 >= p:
+        raise ValueError("coefficient bound must be strictly below modulus")
+    length = len(a) + len(b) - 1
+    n = 1 << (length - 1).bit_length()
+    if not is_prime(p) or (p - 1) % n:
+        raise ValueError("prime modulus must admit the required power-of-two root")
+    omega = pow(generator, (p - 1) // n, p)
+    aa = ntt(list(a) + [0] * (n - len(a)), p, omega, counts=counts)
+    bb = ntt(list(b) + [0] * (n - len(b)), p, omega, counts=counts)
+    cc = [(x * y) % p for x, y in zip(aa, bb)]
+    if counts is not None:
+        counts.pointwise_products += n
+    c = ntt(cc, p, omega, inverse=True, counts=counts)
+    if any(c[length:]):
+        raise ArithmeticError("zero-padding invariant failed")
+    return c[:length]
+
+
+def carry_normalize(coefficients, base):
+    """Euclidean carrying, including a possibly multi-digit terminal carry."""
+    if base < 2 or any(type(c) is not int or c < 0 for c in coefficients):
+        raise ValueError("base >= 2 and nonnegative integer coefficients required")
+    out, carry = [], 0
+    for c in coefficients:
+        carry, digit = divmod(c + carry, base)
+        out.append(digit)
+    while carry:
+        carry, digit = divmod(carry, base)
+        out.append(digit)
+    while len(out) > 1 and out[-1] == 0:
+        out.pop()
+    return out or [0]
+
+
+def evaluate(digits, base):
+    result = 0
+    for digit in reversed(digits):
+        result = result * base + digit
+    return result
+
+
+def multiply_digits(a, b, base=16, p=65537, generator=3, counts=None):
+    return carry_normalize(exact_convolution(a, b, base, p, generator, counts), base)
+
+
+def multiply_integers(x, y, base=16, p=65537, generator=3, counts=None):
+    """Signed integer endpoint, under the same explicit digit-length contract."""
+    if type(x) is not int or type(y) is not int or base < 2:
+        raise ValueError("integer operands and base >= 2 required")
+    def digits(v):
+        out = []
+        while v:
+            v, d = divmod(v, base)
+            out.append(d)
+        return out or [0]
+    z = evaluate(multiply_digits(digits(abs(x)), digits(abs(y)), base,
+                                 p, generator, counts), base)
+    return -z if (x < 0) != (y < 0) else z
diff --git a/research/wordram-ntt-kernel/ntt/sources.json b/research/wordram-ntt-kernel/ntt/sources.json
new file mode 100644
index 0000000000..7c8a205220
--- /dev/null
+++ b/research/wordram-ntt-kernel/ntt/sources.json
@@ -0,0 +1,47 @@
+{
+  "sources": [
+    {
+      "repository": "spitters/CatCrypt-core",
+      "revision": "dc39071735465240b54b43db9b98335d66660d48",
+      "path": "CatCryptCore/Crypto/Lattice/CyclicConvolutionGeneric.lean",
+      "declaration": "dft_cyclicConv",
+      "line": 59,
+      "file_sha256": "c306d2780c3dbd1a46f8a4fb588ec142c4b943b548f488d185fc7cc485e09ee0",
+      "declaration_region_sha256": "d2cde7839db41588cb12883cf28ac8f47d2f0f1840316f59018f3116630846bf",
+      "declaration_hash_rule": "UTF-8 source from theorem header until next theorem or namespace end, trailing whitespace removed then LF appended; includes intervening comments",
+      "url": "https://github.com/spitters/CatCrypt-core/blob/dc39071735465240b54b43db9b98335d66660d48/CatCryptCore/Crypto/Lattice/CyclicConvolutionGeneric.lean#L59",
+      "evidence": "SOURCE_ONLY_NOT_BUILT",
+      "toolchain": "leanprover/lean4:v4.33.1",
+      "license": "MIT; CatCrypt Contributors"
+    },
+    {
+      "repository": "spitters/CatCrypt-core",
+      "revision": "dc39071735465240b54b43db9b98335d66660d48",
+      "path": "CatCryptCore/Crypto/Lattice/NTTFullInversionGeneric.lean",
+      "declaration": "idft_dft",
+      "line": 63,
+      "file_sha256": "4a9cd2b4f7e632410782aae854b63b2d9b1658b9370018f48855cc7cc9938eb5",
+      "declaration_region_sha256": "d36e213c5e7641d84aaa94aef8aa0eb8974e8c483ba93bccb49f2527833789b3",
+      "declaration_hash_rule": "UTF-8 source from theorem header until next theorem or namespace end, trailing whitespace removed then LF appended; includes intervening comments",
+      "url": "https://github.com/spitters/CatCrypt-core/blob/dc39071735465240b54b43db9b98335d66660d48/CatCryptCore/Crypto/Lattice/NTTFullInversionGeneric.lean#L63",
+      "evidence": "SOURCE_ONLY_NOT_BUILT",
+      "toolchain": "leanprover/lean4:v4.33.1",
+      "license": "MIT; CatCrypt Contributors"
+    },
+    {
+      "repository": "spitters/CatCrypt-core",
+      "revision": "dc39071735465240b54b43db9b98335d66660d48",
+      "path": "CatCryptCore/Crypto/Lattice/NTTRecursionPass.lean",
+      "declaration": "dft_even_odd_split",
+      "line": 104,
+      "file_sha256": "4404b4df84677caea3623c3dfc071af3dade3acc62eb5688bb20801844698b11",
+      "declaration_region_sha256": "635c8097025f611f0f9138067478c0a5a199a756c077933b9dcb60d2a016f190",
+      "declaration_hash_rule": "UTF-8 source from theorem header until next theorem or namespace end, trailing whitespace removed then LF appended; includes intervening comments",
+      "url": "https://github.com/spitters/CatCrypt-core/blob/dc39071735465240b54b43db9b98335d66660d48/CatCryptCore/Crypto/Lattice/NTTRecursionPass.lean#L104",
+      "evidence": "SOURCE_ONLY_NOT_BUILT",
+      "toolchain": "leanprover/lean4:v4.33.1",
+      "license": "MIT; CatCrypt Contributors"
+    }
+  ],
+  "use": "Mathematical identities and convention cross-check. Original Python implementation and informal sufficient bridge; no Lean import/build claim."
+}
diff --git a/research/wordram-ntt-kernel/ntt/test_exact_ntt.py b/research/wordram-ntt-kernel/ntt/test_exact_ntt.py
new file mode 100644
index 0000000000..20e78e7805
--- /dev/null
+++ b/research/wordram-ntt-kernel/ntt/test_exact_ntt.py
@@ -0,0 +1,93 @@
+"""Independent finite checks, not universal proof or a runtime benchmark."""
+import itertools
+import random
+import unittest
+from exact_ntt import (Counts, carry_normalize, direct_dft, evaluate,
+                       exact_convolution, multiply_digits, multiply_integers, ntt, schoolbook,
+                       validate_root)
+
+
+class ExactNTTTests(unittest.TestCase):
+    def test_transform_against_direct_dft(self):
+        rng = random.Random(20261024)
+        for n in [1, 2, 4, 8, 16, 32]:
+            omega = pow(3, 65536 // n, 65537)
+            for _ in range(12):
+                a = [rng.randrange(65537) for _ in range(n)]
+                self.assertEqual(ntt(a, 65537, omega), direct_dft(a, 65537, omega))
+                self.assertEqual(ntt(a, 65537, omega, True),
+                                 direct_dft(a, 65537, omega, True))
+                self.assertEqual(ntt(ntt(a, 65537, omega), 65537, omega, True), a)
+
+    def test_all_binary_vectors_up_to_four_digits(self):
+        vectors = [list(v) for length in range(1, 5)
+                   for v in itertools.product(range(2), repeat=length)]
+        for a in vectors:
+            for b in vectors:
+                c = exact_convolution(a, b, 2)
+                self.assertEqual(c, schoolbook(a, b))
+                self.assertEqual(evaluate(carry_normalize(c, 2), 2),
+                                 evaluate(a, 2) * evaluate(b, 2))
+
+    def test_random_asymmetric_and_maximal_digits(self):
+        rng = random.Random(5413)
+        for s, t in [(1, 1), (1, 4096), (3, 137), (16, 17),
+                     (127, 129), (256, 256), (291, 310)]:
+            for maximal in [False, True]:
+                a = [15 if maximal else rng.randrange(16) for _ in range(s)]
+                b = [15 if maximal else rng.randrange(16) for _ in range(t)]
+                c = exact_convolution(a, b)
+                self.assertEqual(c, schoolbook(a, b))
+                self.assertEqual(evaluate(multiply_digits(a, b), 16),
+                                 evaluate(a, 16) * evaluate(b, 16))
+
+    def test_upper_binary_transform_length(self):
+        # Boundary N=65536, asymmetric operands; coefficient bound is 2.
+        a = [1, 1]
+        b = [1] * 65535
+        c = exact_convolution(a, b, 2)
+        self.assertEqual(c, [1] + [2] * 65534 + [1])
+        self.assertEqual(evaluate(carry_normalize(c, 2), 2),
+                         evaluate(a, 2) * evaluate(b, 2))
+
+    def test_dense_maximum_binary_operands(self):
+        length = 32768
+        c = exact_convolution([1] * length, [1] * length, 2)
+        self.assertEqual(c, list(range(1, length + 1)) +
+                         list(range(length - 1, 0, -1)))
+        self.assertEqual(evaluate(carry_normalize(c, 2), 2), ((1 << length) - 1) ** 2)
+
+    def test_signed_endpoint(self):
+        values = [-2**1024 + 1, -2**127, -256, -1, 0, 1, 255, 2**127, 2**1024 - 1]
+        for x in values:
+            for y in values:
+                self.assertEqual(multiply_integers(x, y), x * y)
+
+    def test_cost_instrumentation(self):
+        counts = Counts()
+        exact_convolution([15] * 256, [15] * 256, counts=counts)
+        self.assertEqual(counts.butterflies, 3 * (512 // 2) * 9)
+        self.assertEqual(counts.butterfly_products, counts.butterflies)
+        self.assertEqual(counts.twiddle_products, counts.butterflies)
+        self.assertEqual(counts.pointwise_products, 512)
+        self.assertEqual(counts.inverse_scales, 512)
+
+    def test_invalid_contracts(self):
+        for a, b, base in [([], [1], 16), ([16], [1], 16),
+                            ([-1], [1], 16), ([1.0], [1], 16),
+                            ([15] * 292, [15] * 292, 16)]:
+            with self.assertRaises(ValueError):
+                exact_convolution(a, b, base)
+        for p, n, omega in [(15, 2, 14), (65537, 3, 3),
+                             (65537, 8, 1), (65537, 65536, 1)]:
+            with self.assertRaises(ValueError):
+                validate_root(p, n, omega)
+        with self.assertRaises(ValueError):
+            exact_convolution([1] * 65536, [1, 1], 2)
+        # Strictness: bound == p must fail even though this input is all zero.
+        with self.assertRaises(ValueError):
+            exact_convolution([0] * 17, [0] * 17, base=2, p=17)
+
+
+if __name__ == "__main__":
+    unittest.main()
diff --git a/research/wordram-ntt-kernel/ram/PROOFS.txt b/research/wordram-ntt-kernel/ram/PROOFS.txt
new file mode 100644
index 0000000000..21907aa9c4
--- /dev/null
+++ b/research/wordram-ntt-kernel/ram/PROOFS.txt
@@ -0,0 +1,141 @@
+Counted exact modular multiplication and shared NTT butterflies
+
+Scope
+This contribution supplies literal programs for the nine-instruction WordRAM model
+in tcslib, an independent Python interpreter, executable evidence and informal
+universal proofs. It does not instantiate the Lean compiler theorem and is not
+Lean-checked. Its fixed modulus does not establish an asymptotic multiplication
+bound or a new kappa. The sharing optimization is standard; no novelty claim.
+
+1. Exact machine, ABI and charged constants
+Fix W=64 and p=65537. Words have arithmetic modulo 2^64. Conditional branches
+interpret their operand as a signed two's-complement integer. Only the actual
+one/add/sub/mul/load/store/bltz/accept/reject instructions are accepted. The
+programs use direct-address arithmetic and branches, so need no implicit address
+loads. Interpreter masking and sign conversion implement word semantics; they
+are not extra target instructions. There is no target div, shift or remainder.
+
+Scratch S={8,9,10,11,20,...,35}; constants cell 20+i hold p*2^i, zero is cell 10,
+one is cell 11, temporary subtraction is cell 9, retained product is cell 8.
+Setup is one(11), zero=one-one, one(20), 16 doublings of cell 20, add one,
+then 15 doublings into the remaining cells: exactly 35 instructions. The caller
+may supply arbitrarily dirty scratch. Cleanup clears every scratch cell except
+cell 10, which has remained zero: exactly 19 instructions. No initial zero memory
+assumption is needed. A final accept is one charged instruction.
+
+The modular multiply ABI is inputs cells 0,1; output cell 3. The butterfly ABI is
+inputs u,b,w at 0,1,2; outputs plus,minus at 3,4. Inputs are in [0,p). Outputs
+start arbitrarily dirty. Inputs and every cell outside S union outputs are
+unchanged, including negative addresses and arbitrary dirty far memory. All
+scratch ends zero. A finite Python dictionary tests sample far addresses; the
+universal frame claim follows separately because every write target in the
+literal text is an explicitly listed cell and branches make no memory writes.
+
+For composition Builder permits caller-selected nonreserved cells. Butterfly
+outputs must be fresh/disjoint from inputs; mul may overwrite one operand since
+the initial multiplication reads both before writing. Constants remain live
+between setup and cleanup. Fresh twiddles must be supplied as input ABI or built
+with Builder.literal: 1 instruction for zero and bit_length(n)+popcount(n)-1
+for positive n<2^63. No twiddle construction or caller-side routing is free.
+A direct copy is a charged add(dst,src,zero), one instruction. Python generation,
+looping and allocation are not charged target work unless translated to emitted
+instructions. A fully unrolled fixed-size program has literal immediate cell
+addresses; a variable-size runtime implementation requires further work.
+
+2. Universal modular multiplication invariant
+For 0<=a,b<p, x=a*b <=65536^2=2^32 <p*2^16. Emit mul(output,a,b). Then for
+i=15,14,...,0 perform:
+  tmp := x - p*2^i
+  if tmp<0 branch past the next instruction
+  x := tmp + zero
+This is three literal instructions; the third executes precisely when the
+subtraction is nonnegative. At stage entry 0<=x<p*2^(i+1). If x<p*2^i the branch
+keeps x in [0,p*2^i). Otherwise subtracting p*2^i gives the same interval. The
+residue modulo p is invariant. Induction leaves 0<=x<p and x congruent to ab,
+hence x=ab mod p. All products, thresholds and signed differences have absolute
+value at most 2^32; W=64 therefore makes every signed comparison faithful and
+there is no product truncation. This proof covers all p^2 input pairs.
+
+The chosen subtractions are exactly the binary expansion of q=floor(ab/p),
+where 0<=q<=65535. Thus the modular-multiply body has 49 static instructions and
+33+popcount(q) dynamic instructions: one product, 32 subtract/branch instructions,
+and popcount(q) copies. The complete generic-cleanup program has 104 static
+instructions and 88+popcount(q)<=104 dynamic instructions, including halt. The
+extra clearing of unused retained cell 8 is deliberately counted.
+
+3. Sharing gives a paid machine saving
+For u,b,w in [0,p), let v=bw mod p. The fused butterfly computes v once and
+returns ((u+v) mod p,(u-v) mod p). The reference unfused program computes the
+same v twice, once for each output, with identical setup/cleanup/output ABI.
+The latter is a deliberately explicit recomputation baseline, not an assertion
+about the existing project's best implementation.
+
+Sum uses x=u+v in [0,2p-2], followed by one threshold-p reduction. Difference
+uses x=u+p-v in [1,2p-1], followed by one threshold-p reduction. Each therefore
+needs at most one subtraction. The difference is congruent to u-v modulo p.
+No signed overflow occurs. The output blocks cost 7+c_plus+c_minus dynamic
+instructions, where c_plus=1[u+v>=p] and c_minus=1[u>=v]. Their static cost is 9.
+
+Write h=popcount(floor(bw/p)), c=c_plus+c_minus. The fused body costs 40+h+c;
+the duplicated body costs 73+2h+c. With setup, cleanup and accept:
+  fused:     95+h+c <=113; static length 113;
+  duplicated:128+2h+c<=162; static length 162;
+  exact saving: 33+h instructions, between 33 and 49.
+All upper bounds are attained by u=b=w=65536. The improvement pays the retained
+v's initialization, use and erasure. It removes a complete reduction as well as
+a multiplication. A repeated-butterfly program pays setup/cleanup only once;
+the caller must also pay its literal constants, routing, array loads/stores,
+normalization, output delivery and any other kernel work. This local saving is
+not a whole-job complexity or kappa comparison.
+
+4. FastPoly syntax application
+The independent circuit_sharing.py mirrors the wire/mul/add/sub/fork/bind
+fragment of FastPoly.Cost.Circuit; it does not import Lean or claim to be a
+checked port. The duplicated syntax is fork(add(u,mul(b,w)),sub(u,mul(b,w))).
+The shared syntax is bind(mul(b,w),fork(add(inl(u),inr(0)),sub(inl(u),inr(0)))).
+Evaluating bind extends the original environment by the producer's output.
+Both expressions therefore evaluate to (u+bw,u-bw) in every ring, directly by
+the defining equations. The gates recurrence gives two multiplications and two
+additions for the duplicated syntax, one multiplication and two additions for
+the shared syntax. This is a fixed syntax for every input, respecting the
+RealizesFamily quantifier order. RAM reduction/framing costs are then charged
+separately as above; FastPoly gate counts are never called RAM instruction costs.
+
+5. Evidence and exact remaining formalization boundary
+verify_wordram.py checks all 65,537 b at a=65,536, crossing every quotient q from
+0 to 65,535, plus 5,096 edge/random butterfly triples with dirty scratch and far
+memory. It checks exact outputs, dynamic formulas, accepted halt, failure to halt
+with one step less, write frames, scratch cleanup and signed indirect addressing.
+circuit_sharing.py checks 2,197 signed integer triples and modular evaluations.
+These are finite regression tests; the invariant arguments above provide the
+separate informal universal claims.
+
+A direct Lean proof should encode these exact emitted instruction lists as
+List WordRAM.Instr, instantiate InRange 64 for each signed intermediate, compose
+steps_straight/effect_mul/steps_bltz/Steps.trans for each block, and finish with
+exec_of_steps, accept and the write-set frame theorem. This direct route avoids
+inventing a Light compilation correspondence. compileProgram_correct has distinct
+Light.Exec, Fits and Input hypotheses; it is not applied here, and its constant
+compiler overhead cannot be identified with these hand-assembled exact counts.
+The Python-to-Lean interpreter refinement and exact literal-program proofs remain
+unformalized. No success of a Lean build or axiom audit is asserted.
+
+6. Attribution
+Shilun-Allan-Li/tcslib revision 3a211c0cd7725e077637fff97931909731a3f1f4,
+TCSlib/Programs/WordRAM/Basic.lean (Instr, exec, loadWords);
+TCSlib/Programs/WordRAM/Steps.lean (steps_straight, effect_mul, steps_bltz,
+agreeOutside_effects); TCSlib/Programs/Light/Compiler/WholeProgram.lean
+(compileProgram_correct). These files credit Anthropic, PBC, Apache-2.0,
+vendored from anthropics/formal-math 3sum-apsp revision
+e1a4e6508154ea59f030480661590a9fe3018011 with listed local changes.
+
+Thomas Ahle's thomasahle/fast-polynomials revision
+09a36b0e7a6c153462bd43b91d4a3bb7ac886bef,
+FastPoly/Cost/Circuit.lean (Circuit.bind, Circuit.eval, Circuit.gates, let1),
+FastPoly/Cost/MultiplicationProgram.lean (RealizesFamily). The source files are
+references, not copied upstream proof code. Refer to upstream LICENSE for terms.
+
+This package's Python code and proofs are original independent descriptions.
+Neither shared butterfly computation nor binary modular reduction is claimed
+new. The useful contribution is a concrete, fully counted executable integration
+with exact contracts, overflow ranges, dirty-memory frames and regression evidence.
diff --git a/research/wordram-ntt-kernel/ram/circuit-verification.json b/research/wordram-ntt-kernel/ram/circuit-verification.json
new file mode 100644
index 0000000000..106316349b
--- /dev/null
+++ b/research/wordram-ntt-kernel/ram/circuit-verification.json
@@ -0,0 +1,13 @@
+{
+  "status": "PASS",
+  "triples": 2197,
+  "duplicated_gates_mul_add": [
+    2,
+    2
+  ],
+  "shared_gates_mul_add": [
+    1,
+    2
+  ],
+  "formalization": "not Lean checked"
+}
diff --git a/research/wordram-ntt-kernel/ram/circuit_sharing.py b/research/wordram-ntt-kernel/ram/circuit_sharing.py
new file mode 100644
index 0000000000..21ee1529a5
--- /dev/null
+++ b/research/wordram-ntt-kernel/ram/circuit_sharing.py
@@ -0,0 +1,68 @@
+"""Small executable mirror of the used FastPoly Circuit fragment (not a Lean port).
+Constructors preserve the exact `fork`/`bind` cost recurrence in the pinned source.
+"""
+from dataclasses import dataclass
+
+@dataclass(frozen=True)
+class Circuit:
+    op: str
+    args: tuple
+
+
+def wire(label): return Circuit('wire', (label,))
+def mul(a, b): return Circuit('mul', (a, b))
+def add(a, b): return Circuit('add', (a, b))
+def sub(a, b): return Circuit('sub', (a, b))
+def fork(a, b): return Circuit('fork', (a, b))
+def bind(a, b): return Circuit('bind', (a, b))
+
+
+def evaluate(c, environment, modulus=None):
+    def normalize(v): return v if modulus is None else v % modulus
+    if c.op == 'wire': return (environment[c.args[0]],)
+    a, b = c.args
+    if c.op == 'bind':
+        producer = evaluate(a, environment, modulus)
+        body_environment = {('inl', k): v for k, v in environment.items()}
+        body_environment.update({('inr', i): v for i, v in enumerate(producer)})
+        return evaluate(b, body_environment, modulus)
+    x, y = evaluate(a, environment, modulus), evaluate(b, environment, modulus)
+    if c.op == 'fork': return x + y
+    if c.op == 'add': return (normalize(x[0] + y[0]),)
+    if c.op == 'sub': return (normalize(x[0] - y[0]),)
+    if c.op == 'mul': return (normalize(x[0] * y[0]),)
+    raise ValueError(c.op)
+
+
+def gates(c):
+    if c.op == 'wire': return (0, 0)
+    x, y = (gates(a) for a in c.args)
+    return (x[0] + y[0] + int(c.op == 'mul'),
+            x[1] + y[1] + int(c.op in ('add', 'sub')))
+
+
+def butterfly_circuits():
+    u, b, w = (wire(s) for s in ('u', 'b', 'w'))
+    duplicated = fork(add(u, mul(b, w)), sub(u, mul(b, w)))
+    v = wire(('inr', 0)); u_body = wire(('inl', 'u'))
+    shared = bind(mul(b, w), fork(add(u_body, v), sub(u_body, v)))
+    return duplicated, shared
+
+
+def check():
+    duplicated, shared = butterfly_circuits()
+    assert gates(duplicated) == (2, 2)
+    assert gates(shared) == (1, 2)
+    for u in range(-6, 7):
+        for b in range(-6, 7):
+            for w in range(-6, 7):
+                environment = {'u': u, 'b': b, 'w': w}
+                assert evaluate(duplicated, environment) == (u + b*w, u - b*w)
+                assert evaluate(shared, environment) == (u + b*w, u - b*w)
+                assert evaluate(shared, environment, 65537) == ((u + b*w) % 65537, (u - b*w) % 65537)
+    return {'status': 'PASS', 'triples': 2197, 'duplicated_gates_mul_add': gates(duplicated),
+            'shared_gates_mul_add': gates(shared), 'formalization': 'not Lean checked'}
+
+if __name__ == '__main__':
+    import json
+    print(json.dumps(check(), indent=2))
diff --git a/research/wordram-ntt-kernel/ram/sources.json b/research/wordram-ntt-kernel/ram/sources.json
new file mode 100644
index 0000000000..73b132f847
--- /dev/null
+++ b/research/wordram-ntt-kernel/ram/sources.json
@@ -0,0 +1,42 @@
+[
+  {
+    "repository": "Shilun-Allan-Li/tcslib",
+    "revision": "3a211c0cd7725e077637fff97931909731a3f1f4",
+    "path": "TCSlib/Programs/WordRAM/Basic.lean",
+    "sha256": "f4f498c800d0231ee7c8ac222ae162cc9de149694b07c8c5e094c93530acf1f3",
+    "url": "https://github.com/Shilun-Allan-Li/tcslib/blob/3a211c0cd7725e077637fff97931909731a3f1f4/TCSlib/Programs/WordRAM/Basic.lean",
+    "evidence": "SOURCE_ONLY_NOT_BUILT"
+  },
+  {
+    "repository": "Shilun-Allan-Li/tcslib",
+    "revision": "3a211c0cd7725e077637fff97931909731a3f1f4",
+    "path": "TCSlib/Programs/WordRAM/Steps.lean",
+    "sha256": "7bc4819544c0f0c50270c15b53746c0abf83185ed71063294a94db85a91918fa",
+    "url": "https://github.com/Shilun-Allan-Li/tcslib/blob/3a211c0cd7725e077637fff97931909731a3f1f4/TCSlib/Programs/WordRAM/Steps.lean",
+    "evidence": "SOURCE_ONLY_NOT_BUILT"
+  },
+  {
+    "repository": "Shilun-Allan-Li/tcslib",
+    "revision": "3a211c0cd7725e077637fff97931909731a3f1f4",
+    "path": "TCSlib/Programs/Light/Compiler/WholeProgram.lean",
+    "sha256": "3d2b93e17218377cf46d7447156e6423a1daec7e00be90936896ad56e3409120",
+    "url": "https://github.com/Shilun-Allan-Li/tcslib/blob/3a211c0cd7725e077637fff97931909731a3f1f4/TCSlib/Programs/Light/Compiler/WholeProgram.lean",
+    "evidence": "SOURCE_ONLY_NOT_BUILT"
+  },
+  {
+    "repository": "thomasahle/fast-polynomials",
+    "revision": "09a36b0e7a6c153462bd43b91d4a3bb7ac886bef",
+    "path": "FastPoly/Cost/Circuit.lean",
+    "sha256": "1ed86f02b9321ca5d2ef17eb860db31801fed135e4a62b7d7035acb43372db0a",
+    "url": "https://github.com/thomasahle/fast-polynomials/blob/09a36b0e7a6c153462bd43b91d4a3bb7ac886bef/FastPoly/Cost/Circuit.lean",
+    "evidence": "SOURCE_ONLY_NOT_BUILT"
+  },
+  {
+    "repository": "thomasahle/fast-polynomials",
+    "revision": "09a36b0e7a6c153462bd43b91d4a3bb7ac886bef",
+    "path": "FastPoly/Cost/MultiplicationProgram.lean",
+    "sha256": "dcd92f8086d09d4be671e295db44dbcee16761b953ed43b5b8be2b6f77adf477",
+    "url": "https://github.com/thomasahle/fast-polynomials/blob/09a36b0e7a6c153462bd43b91d4a3bb7ac886bef/FastPoly/Cost/MultiplicationProgram.lean",
+    "evidence": "SOURCE_ONLY_NOT_BUILT"
+  }
+]
diff --git a/research/wordram-ntt-kernel/ram/verification.json b/research/wordram-ntt-kernel/ram/verification.json
new file mode 100644
index 0000000000..d761d6cd06
--- /dev/null
+++ b/research/wordram-ntt-kernel/ram/verification.json
@@ -0,0 +1,25 @@
+{
+  "status": "PASS",
+  "word_bits": 64,
+  "modulus": 65537,
+  "exhaustive_multiply_inputs": 65537,
+  "exhaustive_slice": "a=65536, all 0<=b<=65536",
+  "butterfly_input_triples": 5096,
+  "random_seed": 20261024,
+  "static_lengths": {
+    "multiply": 104,
+    "fused_butterfly": 113,
+    "duplicate_butterfly": 162
+  },
+  "observed_max_dynamic": {
+    "multiply": 104,
+    "fused_butterfly": 113,
+    "duplicate_butterfly": 162
+  },
+  "scope": "Executable replays plus informal universal invariant proof; no Lean kernel check",
+  "files_sha256": {
+    "circuit_sharing.py": "0eadf9ef954c5d97aa5e5f0949b6bf90ecb90fbb9d0321f472b2c6e97140c24f",
+    "verify_wordram.py": "02b2c09ff1542e6f947aedaad67c9a1872ed0098a447b71076cfbfe14373efbb",
+    "wordram_kernel.py": "b1a6133e505e5faf5832a5274eea23f96b033257c3d16cc24479c4a4c7059a2e"
+  }
+}
diff --git a/research/wordram-ntt-kernel/ram/verify_wordram.py b/research/wordram-ntt-kernel/ram/verify_wordram.py
new file mode 100644
index 0000000000..d55923ac76
--- /dev/null
+++ b/research/wordram-ntt-kernel/ram/verify_wordram.py
@@ -0,0 +1,79 @@
+"""Portable adversarial replay and source-independent arithmetic oracles."""
+import hashlib
+import json
+from pathlib import Path
+import random
+from wordram_kernel import (
+    Builder, MODULUS as P, MASK, SCRATCH, butterfly_program, multiply_program, run,
+)
+
+
+def check_frame(result, initial, outputs):
+    assert result is not None and result.accepted
+    assert result.writes <= SCRATCH | set(outputs)
+    for cell, value in initial.items():
+        if cell not in SCRATCH | set(outputs):
+            assert result.memory.get(cell, 0) == (value & MASK)
+    assert all(result.memory.get(cell, 0) == 0 for cell in SCRATCH)
+
+
+def run_checks():
+    rng = random.Random(20261024)
+    mul = multiply_program()
+    fused, duplicate = butterfly_program(), butterfly_program(fused=False)
+    assert (len(mul), len(fused), len(duplicate)) == (104, 113, 162)
+    maximum_mul = maximum_fused = maximum_duplicate = 0
+    # This complete finite sweep crosses every attainable product quotient:
+    # floor(65536*b/65537)=b-1 for 1<=b<=65536.
+    for b in range(P):
+        initial = {0: P - 1, 1: b, -97: MASK - b, 1000007: b + 31}
+        result = run(mul, initial)
+        check_frame(result, initial, {3})
+        assert result.memory[3] == ((P - 1) * b) % P
+        assert result.steps == 88 + (((P - 1) * b) // P).bit_count()
+        maximum_mul = max(maximum_mul, result.steps)
+    edge = [0, 1, 2, 255, 256, 32767, 32768, P - 3, P - 2, P - 1]
+    triples = [(u, b, w) for u in edge for b in edge for w in edge]
+    triples += [(rng.randrange(P), rng.randrange(P), rng.randrange(P)) for _ in range(4096)]
+    for u, b, w in triples:
+        initial = {0: u, 1: b, 2: w, -97: rng.getrandbits(64), 1000007: rng.getrandbits(64)}
+        initial.update({a: rng.getrandbits(64) for a in SCRATCH | {3, 4}})
+        f, d = run(fused, initial), run(duplicate, initial)
+        check_frame(f, initial, {3, 4}); check_frame(d, initial, {3, 4})
+        v = b * w % P
+        expected = ((u + v) % P, (u - v) % P)
+        assert (f.memory[3], f.memory[4]) == expected
+        assert (d.memory[3], d.memory[4]) == expected
+        bits = ((b * w) // P).bit_count()
+        corrections = int(u + v >= P) + int(u >= v)
+        assert f.steps == 95 + bits + corrections
+        assert d.steps == 128 + 2 * bits + corrections
+        assert d.steps - f.steps == 33 + bits
+        maximum_fused = max(maximum_fused, f.steps)
+        maximum_duplicate = max(maximum_duplicate, d.steps)
+        # One fewer than the exact halt count must not return a verdict.
+        assert run(fused, initial, budget=f.steps - 1) is None
+    # Exercise the otherwise unused indirect/signed-address interpreter semantics.
+    e = run([('load', 0, 1), ('store', 2, 0), ('accept',)], {1: -4, -4: 123, 2: -5})
+    assert e.accepted and e.memory[0] == 123 and e.memory[-5] == 123 and e.steps == 3
+    # Prove literal-synthesis count against its syntax, including zero and sign boundary.
+    for n in [0, 1, 2, 3, 65537, (1 << 62) - 1, (1 << 63) - 1]:
+        builder = Builder(); builder.setup(); start = len(builder.code)
+        builder.literal(100, n)
+        literal_ops = len(builder.code) - start
+        assert literal_ops == (1 if n == 0 else n.bit_length() + n.bit_count() - 1)
+        builder.cleanup(); builder.accept()
+        e = run(builder.program(), {})
+        assert e.accepted and e.memory[100] == n
+    return {
+        'status': 'PASS', 'word_bits': 64, 'modulus': P,
+        'exhaustive_multiply_inputs': P, 'exhaustive_slice': 'a=65536, all 0<=b<=65536',
+        'butterfly_input_triples': len(triples), 'random_seed': 20261024,
+        'static_lengths': {'multiply': len(mul), 'fused_butterfly': len(fused), 'duplicate_butterfly': len(duplicate)},
+        'observed_max_dynamic': {'multiply': maximum_mul, 'fused_butterfly': maximum_fused, 'duplicate_butterfly': maximum_duplicate},
+        'scope': 'Executable replays plus informal universal invariant proof; no Lean kernel check',
+        'files_sha256': {p.name: hashlib.sha256(p.read_bytes()).hexdigest() for p in Path(__file__).parent.glob('*.py')},
+    }
+
+if __name__ == '__main__':
+    print(json.dumps(run_checks(), indent=2))
diff --git a/research/wordram-ntt-kernel/ram/wordram_kernel.py b/research/wordram-ntt-kernel/ram/wordram_kernel.py
new file mode 100644
index 0000000000..f5c6e00699
--- /dev/null
+++ b/research/wordram-ntt-kernel/ram/wordram_kernel.py
@@ -0,0 +1,157 @@
+"""Literal tcslib WordRAM.Basic ISA programs; Python is only the assembler/interpreter.
+Original implementation, 2026. See PROOFS.txt for contracts and source attribution.
+"""
+from collections import Counter
+from dataclasses import dataclass
+
+W = 64
+MODULUS = 65537
+MASK = (1 << W) - 1
+ZERO, ONE, VALUE, TEMP = 10, 11, 8, 9
+CONSTANTS = tuple(range(20, 36))
+SCRATCH = frozenset((ZERO, ONE, VALUE, TEMP, *CONSTANTS))
+
+@dataclass
+class Execution:
+    accepted: bool
+    memory: dict
+    steps: int
+    counts: dict
+    writes: frozenset
+
+def signed(x):
+    x &= MASK
+    return x if x < (1 << (W - 1)) else x - (1 << W)
+
+def run(program, memory, budget=None):
+    """Match WordRAM.exec at W=64, including signed indirect addresses and halt step.
+    Memory is a finite support dict; unspecified cells contain zero. No native %
+    reduction/division/shift is an interpreted instruction.
+    """
+    m = {a: v & MASK for a, v in memory.items()}
+    pc = steps = 0
+    counts, writes = Counter(), set()
+    budget = len(program) + 1 if budget is None else budget
+    def read(a):
+        return m.get(a, 0)
+    while steps < budget:
+        ins = program[pc] if 0 <= pc < len(program) else ('reject',)
+        op, *args = ins
+        steps += 1
+        counts[op] += 1
+        if op in ('accept', 'reject'):
+            return Execution(op == 'accept', m, steps, dict(counts), frozenset(writes))
+        next_pc = pc + 1
+        if op == 'bltz':
+            a, label = args
+            if signed(read(a)) < 0:
+                next_pc = label
+        else:
+            i = args[0]
+            if op == 'one':
+                value = 1
+            elif op == 'add':
+                value = read(args[1]) + read(args[2])
+            elif op == 'sub':
+                value = read(args[1]) - read(args[2])
+            elif op == 'mul':
+                value = read(args[1]) * read(args[2])
+            elif op == 'load':
+                value = read(signed(read(args[1])))
+            elif op == 'store':
+                i = signed(read(args[0]))
+                value = read(args[1])
+            else:
+                raise ValueError('Unknown tcslib instruction: ' + str(op))
+            m[i] = value & MASK
+            writes.add(i)
+        pc = next_pc
+    return None
+
+class Builder:
+    """Forward-only literal assembler. Branch targets are absolute program indices.
+    All cells except reserved SCRATCH may be chosen by the caller; fresh/disjoint
+    input/output cells are required for butterfly. `setup` is exactly 35 instructions.
+    Constants remain valid until cleanup. `literal` charges every construction op.
+    """
+    def __init__(self):
+        self.code = []
+        self.ready = False
+    def emit(self, *ins):
+        self.code.append(tuple(ins))
+    def setup(self):
+        if self.ready:
+            raise ValueError('Setup already live')
+        self.emit('one', ONE)
+        self.emit('sub', ZERO, ONE, ONE)
+        self.emit('one', CONSTANTS[0])
+        for _ in range(16):
+            self.emit('add', CONSTANTS[0], CONSTANTS[0], CONSTANTS[0])
+        self.emit('add', CONSTANTS[0], CONSTANTS[0], ONE)
+        for src, dst in zip(CONSTANTS, CONSTANTS[1:]):
+            self.emit('add', dst, src, src)
+        self.ready = True
+    def literal(self, dst, value):
+        if not self.ready or dst in SCRATCH or not 0 <= value < (1 << 63):
+            raise ValueError('Bad literal contract')
+        if value == 0:
+            self.emit('sub', dst, ZERO, ZERO)
+        else:
+            self.emit('one', dst)
+            for bit in bin(value)[3:]:
+                self.emit('add', dst, dst, dst)
+                if bit == '1':
+                    self.emit('add', dst, dst, ONE)
+    def copy(self, dst, src):
+        if not self.ready or dst in SCRATCH:
+            raise ValueError('Bad copy contract')
+        self.emit('add', dst, src, ZERO)
+    def _reduce_once(self, value, constant):
+        self.emit('sub', TEMP, value, constant)
+        self.emit('bltz', TEMP, len(self.code) + 2)
+        self.emit('add', value, TEMP, ZERO)
+    def _mul(self, a, b, out):
+        self.emit('mul', out, a, b)
+        for constant in reversed(CONSTANTS):
+            self._reduce_once(out, constant)
+    def mul(self, a, b, out):
+        if not self.ready or {a, b, out} & SCRATCH:
+            raise ValueError('Bad multiplication ABI')
+        self._mul(a, b, out)
+    def butterfly(self, u, b, twiddle, plus, minus, fused=True):
+        cells = {u, b, twiddle, plus, minus}
+        if not self.ready or cells & SCRATCH or plus == minus or {plus, minus} & {u, b, twiddle}:
+            raise ValueError('Butterfly requires fresh output cells')
+        self._mul(b, twiddle, VALUE)
+        self.emit('add', plus, u, VALUE)
+        self._reduce_once(plus, CONSTANTS[0])
+        if not fused:
+            self._mul(b, twiddle, VALUE)
+        self.emit('add', minus, u, CONSTANTS[0])
+        self.emit('sub', minus, minus, VALUE)
+        self._reduce_once(minus, CONSTANTS[0])
+    def cleanup(self):
+        if not self.ready:
+            raise ValueError('Setup not live')
+        # ZERO was set to zero and never subsequently changed.
+        for cell in sorted(SCRATCH - {ZERO}):
+            self.emit('sub', cell, cell, cell)
+        self.ready = False
+    def accept(self):
+        self.emit('accept')
+    def program(self):
+        return list(self.code)
+
+def multiply_program():
+    b = Builder(); b.setup(); b.mul(0, 1, 3); b.cleanup(); b.accept()
+    return b.program()
+
+def butterfly_program(fused=True):
+    b = Builder(); b.setup(); b.butterfly(0, 1, 2, 3, 4, fused=fused); b.cleanup(); b.accept()
+    return b.program()
+
+if __name__ == '__main__':
+    p = butterfly_program()
+    result = run(p, {0: 65536, 1: 65536, 2: 65536})
+    print({'static_instructions': len(p), 'dynamic_instructions': result.steps,
+           'outputs': [result.memory[3], result.memory[4]]})
diff --git a/research/wordram-ntt-kernel/ram_multiplier.py b/research/wordram-ntt-kernel/ram_multiplier.py
new file mode 100644
index 0000000000..09ca74343b
--- /dev/null
+++ b/research/wordram-ntt-kernel/ram_multiplier.py
@@ -0,0 +1,109 @@
+"""Assemble and execute one fixed-size tcslib-ISA multiplication program.
+Program generation depends only on public lengths and fixed field constants.
+Every runtime instruction, including table synthesis and clearing, is interpreted.
+"""
+from dataclasses import dataclass
+from ram.wordram_kernel import Builder, run, SCRATCH, ZERO, TEMP
+from ntt.exact_ntt import validate_root, evaluate
+
+P, BASE, GENERATOR = 65537, 16, 3
+
+@dataclass
+class Plan:
+    program: list
+    left: list
+    right: list
+    output: list
+    temporaries: set
+    butterflies: int
+    modular_products: int
+    n: int
+    fused: bool
+
+
+def build_multiplier(s, t, fused=True):
+    if not (1 <= s <= 256 and 1 <= t <= 256):
+        raise ValueError('each operand must have 1..256 hexadecimal digits')
+    n = 1 << (s+t-2).bit_length()
+    omega = pow(GENERATOR, (P-1)//n, P)
+    validate_root(P, n, omega)
+    b = Builder(); b.setup()
+    left, right = list(range(1000,1000+s)), list(range(2000,2000+t))
+    outputs = list(range(3000,3000+n+1))
+    fresh_id, temporaries, constants = 10000, set(), {}
+    butterflies = modular_products = 0
+    def fresh():
+        nonlocal fresh_id
+        x = fresh_id; fresh_id += 1; temporaries.add(x)
+        return x
+    def const(value):
+        if value not in constants:
+            addr=fresh(); b.literal(addr,value); constants[value]=addr
+        return constants[value]
+    def transform(cells, inverse=False):
+        nonlocal butterflies,modular_products
+        widthbits = n.bit_length()-1
+        perm = [int(format(i,'0'+str(widthbits)+'b')[::-1],2) if widthbits else 0 for i in range(n)]
+        a=[]
+        for i in perm:
+            dst=fresh(); b.copy(dst,cells[i] if i<len(cells) else const(0));a.append(dst)
+        root=pow(omega,P-2,P) if inverse else omega
+        width=2
+        while width<=n:
+            rootstep=pow(root,n//width,P)
+            for lo in range(0,n,width):
+                w=1
+                for j in range(lo,lo+width//2):
+                    plus,minus=fresh(),fresh()
+                    b.butterfly(a[j],a[j+width//2],const(w),plus,minus,fused=fused)
+                    a[j],a[j+width//2]=plus,minus
+                    w=w*rootstep%P
+                    butterflies+=1;modular_products+=1 if fused else 2
+            width*=2
+        if inverse:
+            invn=const(pow(n,P-2,P));scaled=[]
+            for src in a:
+                dst=fresh();b.mul(src,invn,dst);scaled.append(dst);modular_products+=1
+            a=scaled
+        return a
+    aa,bb=transform(left),transform(right)
+    products=[]
+    for x,y in zip(aa,bb):
+        dst=fresh();b.mul(x,y,dst);products.append(dst);modular_products+=1
+    coeff=transform(products,True)
+    # Restore quotient/remainder division by 16 using only allowed instructions.
+    # Bounds: coefficient <= 57600, incoming carry <=3840, total <=61440.
+    carry=const(0)
+    for i,c in enumerate(coeff):
+        total,quotient=fresh(),fresh()
+        b.emit('add',total,c,carry);b.copy(quotient,const(0))
+        for bit in reversed(range(12)):
+            threshold,weight=const(BASE*(1<<bit)),const(1<<bit)
+            b.emit('sub',TEMP,total,threshold)
+            b.emit('bltz',TEMP,len(b.code)+3)
+            b.emit('add',total,TEMP,ZERO)
+            b.emit('add',quotient,quotient,weight)
+        b.copy(outputs[i],total);carry=quotient
+    b.copy(outputs[n],carry)
+    # Clear every owned intermediate, table cell and constant; leave operands.
+    for addr in sorted(temporaries):b.emit('sub',addr,addr,addr)
+    b.cleanup();b.accept()
+    return Plan(b.program(),left,right,outputs,temporaries,butterflies,modular_products,n,fused)
+
+
+def execute(plan,a,b,dirty=False):
+    if len(a)!=len(plan.left) or len(b)!=len(plan.right) or any(type(x)is not int or not 0<=x<BASE for x in a+b):
+        raise ValueError('operand digits violate fixed program ABI')
+    memory={**dict(zip(plan.left,a)),**dict(zip(plan.right,b)),-7:123456,777777:987654}
+    if dirty:
+        memory.update({x:0xDEADBEEF for x in plan.temporaries|SCRATCH|set(plan.output)})
+    initial=memory.copy();result=run(plan.program,memory)
+    assert result is not None and result.accepted
+    digits=[result.memory[x] for x in plan.output]
+    assert all(0<=x<BASE for x in digits)
+    assert evaluate(digits,BASE)==evaluate(a,BASE)*evaluate(b,BASE)
+    assert all(result.memory.get(x,0)==0 for x in plan.temporaries|SCRATCH)
+    allowed=plan.temporaries|SCRATCH|set(plan.output)
+    assert result.writes<=allowed
+    assert all(result.memory.get(x,0)==v for x,v in initial.items() if x not in allowed)
+    return result,digits
diff --git a/research/wordram-ntt-kernel/recovery/REPORT.txt b/research/wordram-ntt-kernel/recovery/REPORT.txt
new file mode 100644
index 0000000000..ed6d5042a0
--- /dev/null
+++ b/research/wordram-ntt-kernel/recovery/REPORT.txt
@@ -0,0 +1,70 @@
+Certified shared-butterfly and strict-recovery application
+
+Scope. This contribution supplies a concrete integer-only fixed-point complex FFT backend for multiplying two base-16 digit vectors of length at most 256. The transform length is 512. It applies the fixed-syntax sharing discipline of FastPoly and the strict lattice-recovery endpoint of mpfx. Its universal correctness argument is the elementary proof below; its executable evidence uses Python integers and exact Fractions. It does not import, port or kernel-check the upstream libraries. It is an optional approximate backend alongside the release's exact NTT backend, not a claimed advantage over exact modular arithmetic or a new kappa.
+
+1. Fixed syntax and shared product.
+
+For every commutative ring, B_w(u,v)=(u+w v,u-w v). Evaluate t=w v once, then emit u+t and u-t. This is one multiplication and two add/subtract operations when w is an input; evaluating the two output expressions independently repeats the product. This is exactly the distinction between Circuit.bind and two independently expanded Circuit.mul expressions. The fixed circuit is chosen before its input environment, matching MultiplicationProgram.RealizesFamily's quantifier order.
+
+Important accounting qualification: FastPoly.Circuit.scale charges zero nonscalar multiplications when w is a scalar constant. Our transform counts every executed complex twiddle multiplication, including constant and identity twiddles. Therefore its literal counts are executable complex-arithmetic counts, not FastPoly nonscalar-rank counts, machine instructions, or project rank-moment savings. Identity and other special twiddles have deliberately not been optimized out.
+
+For N=2^L, each transform uses L N/2 shared complex products, and two forward transforms, a pointwise product and one inverse use 3 L N/2+N. For N=512, L=9 this is 7,424 complex products and 6,912 butterflies, versus 14,336 complex products when each butterfly output recomputes its product. Each complex product is concretely four integer products, two integer add/subtractions and two nearest-scaled divisions. All loop, address, permutation, division and storage costs still require a separate machine refinement.
+
+2. Exact transform semantics.
+
+Let zeta=exp(-2 pi i/N). The forward transform is A_j=sum_t a_t zeta^(jt); the inverse has positive sign and divides by N. For any integer k, sum_j zeta^(jk) is N when N divides k and zero otherwise: the latter follows by multiplying the finite geometric sum by 1-zeta^k, which is nonzero. Consequently inverse(DFT(a) DFT(b))_k=sum_{r+s congruent k mod N} a_r b_s.
+
+Zero-pad operands of lengths at most N/2. Their largest nonzero linear-convolution index is N-2, so no nonzero term wraps. The inverse output is exactly c_k=sum_{r+s=k} a_r b_s, an integer in [0,225 N/2]. For N=512 this is at most 57,600. Evaluation at 16 gives sum_k c_k 16^k=(sum_r a_r 16^r)(sum_s b_s 16^s), by finite distributivity. Ordinary base-16 carry normalization, if required, preserves this value using t=16 floor(t/16)+(t mod 16).
+
+The implementation's initial bit reversal and iterative blocks realize this transform. More explicitly, after stage s, each consecutive block b of length m=2^s is the length-m DFT of a[r+t N/m], where r is the bit reversal of b in L-s bits. At s=0 this is the initial permutation. The next stage combines the even and odd t subsequences and uses zeta_N^(j N/(2m)), giving the standard two butterfly outputs. This proves the invariant inductively, and the full block at s=L is the stated DFT. Conjugating every twiddle gives the unnormalized inverse.
+
+3. A complete sufficient rounding theorem.
+
+Use Q=2^b and store complex values as integer pairs divided by Q. Input digits are exactly represented. Addition/subtraction is exact integer arithmetic. A complex multiplication first computes its two integer component numerators exactly and rounds each divided-by-Q numerator to the nearest integer. Each component error is at most 1/(2Q), so its Euclidean error is at most 1/Q. Ties are rounded toward positive infinity, but the theorem below is independent of this choice at final recovery.
+
+Assume each stored twiddle differs from its exact unit complex root by at most W in Euclidean norm. Let delta=1/Q. Suppose all exact inputs to a butterfly stage have magnitude at most M, and their approximations have error at most E. Write the exact lower product w v and computed product round(w_tilde v_tilde). By the triangle inequality,
+
+|round(w_tilde v_tilde)-w v|
+ <= delta + |w_tilde| |v_tilde-v| + |w_tilde-w| |v|
+ <= delta + (1+W) E + W M.
+
+Adding either signed product to u_tilde contributes at most one further E and no new rounding. Thus every output error is at most
+
+E_next=(2+W) E + W M + delta,
+
+and every exact output magnitude is at most M_next=2 M. This recurrence includes errors in the twiddle and product, including their interaction W E; it does not treat approximate twiddles as exact.
+
+Initialize M=15, E=0 and iterate L stages for each forward transform. The exact pointwise products have magnitude at most M^2. Their computed errors satisfy
+
+E_product <= 2 M E + E^2 + delta,
+
+by expansion (A+e)(B+f)-AB=A f+B e+e f. Initialize the same L-stage inverse recurrence at M^2,E_product. Exact normalization by division by N leaves coefficient error at most E_inverse/N. The implementation keeps this normalization rational until the final integer rounding; it does not incur a hidden intermediate fixed-format rounding.
+
+If E_inverse/N<1/2, every recovered coefficient is exactly c_k. Indeed x-c_k in (-1/2,1/2) implies c_k<=x+1/2<c_k+1 and hence floor(x+1/2)=c_k. Integer lattice membership is essential. Equality at 1/2 is insufficient: x=1/2 and intended coefficient zero gives floor(x+1/2)=1. These controls are executable and the strict endpoint is separately formalized in IntegerKernelRecovery20261024.lean.
+
+4. Twiddle certificates are generated, not assumed.
+
+Machin's identity pi=16 atan(1/5)-4 atan(1/239), together with the alternating arctangent series, encloses pi between two rational endpoints after 100 terms. The verifier takes a 96-bit dyadic midpoint and includes its distance to both endpoints. Angles are reflected to [0,pi/2]. It evaluates the cosine degree-30 and sine degree-31 Taylor polynomials over rational arguments. Taylor's theorem, using derivative magnitude at most one, bounds their remainders by |x|^31/31! and |x|^32/32!, respectively. The angle perturbation is added using |sin x-sin y|<=|x-y| and |cos x-cos y|<=|x-y|. Reflection changes only the cosine sign; the forward sine has negative sign.
+
+For each coordinate the checker proves, with Fractions, that the distance between the chosen dyadic and the polynomial plus the remainder and angle bounds is STRICTLY below 1/(2Q). Exact roots 1 and -i are handled directly. Thus each complex twiddle error is below 1/Q, justifying W=delta. No binary floating point, empirical root-quality assumption, or trusted external transcendental evaluator enters these checks. Machin's formula, the alternating-series theorem, elementary trigonometric identities and Taylor's theorem are the ordinary mathematical premises of this paper proof; their proofs have not been replayed in Lean here.
+
+5. Instantiated all-input result and executable checks.
+
+For every pair of nonnegative base-16 digit vectors of length at most 256, the stated fixed-point FFT with N=512, Q=2^40, the certified twiddle table and exact unbounded integer intermediate arithmetic recovers their complete linear convolution and product exactly. The rational recurrence proves E_inverse/N<1/1000<1/2 (approximately 0.000731335, given only as a readable illustration). The smallest precision satisfying this particular conservative recurrence is 31 bits; its bound is approximately 0.374444<1/2. This is not a lower bound or an optimal precision claim.
+
+The 40-bit run checks all-zero, all-15, both endpoint placements, alternating digits and 12 deterministic random input pairs and three signed-digit input pairs: 20 pairs total. Every recovered coefficient is independently compared with schoolbook convolution, and the packed product is compared with Python's integer multiplication. These finite controls corroborate the implementation and do not replace the universal argument above.
+
+The implementation uses Python unbounded integer arithmetic. Its fixed-point product numerators can exceed 64 bits, so this backend is NOT a 64-bit unit-cost Word RAM certificate. A carry/split implementation or charged multiword multiplication refinement is needed before comparing its machine costs. The exact NTT backend avoids these approximate-arithmetic costs and has a separate residue reconstruction theorem.
+
+Reproduce:
+  python fixedpoint_fft.py --n 512 --bits 40 --cases 12 --output verification.json
+
+Predecessor credit.
+- bksaiki/mpfx-lean, revision 8bd80452927ae9234fc378c07a00f2962e1e5b6f, Mpfx/Rounding/Ulp.lean, nearest_eq_of_close (line 198 in this snapshot) and nearest_eq_of_close' (line 229): strict closeness plus lattice alignment implies exact nearest rounding. We specialize the endpoint to integer coefficients; we do not claim the idea is novel.
+- thomasahle/fast-polynomials, revision 09a36b0e7a6c153462bd43b91d4a3bb7ac886bef, FastPoly/Cost/Circuit.lean: Circuit.bind/let1 implements genuine sharing; Circuit.gates computes syntax costs. MultiplicationProgram.lean: RealizesFamily fixes syntax before the environment. We apply this discipline to a butterfly and explicitly retain its differing scalar-cost convention.
+- The DFT convolution identity, radix-2 Cooley-Tukey decomposition, Machin identity, Taylor bounds and strict-half integer recovery are classical. This contribution is a scoped combination and reproducible bounded kernel, with no broad novelty or project-best-kappa claim.
+
+Signed extension. The entire error proof only uses absolute digit bounds. Therefore it also proves exact coefficient and integer-product recovery for signed digits in [-15,15], with coefficient absolute value at most 57,600. The verifier includes all-negative, alternating-sign and random signed operands. Base-16 normalization of a negative overall integer requires an explicit sign representation; packed integer equality already holds without that choice.
+
+Lean evidence. The corrected local helper in ../lean/IntegerKernelRecovery20261024.lean passed a fresh independent Lean 4.33.0 kernel and transitive-axiom audit. The four helpers use only the standard approved axioms; exact names, source SHA-256 and dependencies are recorded in ../lean/STATUS.json. This verifies only the local recovery/algebra endpoints, not the complete FFT or RAM program.
+
diff --git a/research/wordram-ntt-kernel/recovery/SOURCES.json b/research/wordram-ntt-kernel/recovery/SOURCES.json
new file mode 100644
index 0000000000..dffae1f418
--- /dev/null
+++ b/research/wordram-ntt-kernel/recovery/SOURCES.json
@@ -0,0 +1,26 @@
+[
+  {
+    "repository": "bksaiki/mpfx-lean",
+    "revision": "8bd80452927ae9234fc378c07a00f2962e1e5b6f",
+    "source": "Mpfx/Rounding/Ulp.lean",
+    "sha256": "fae20b63b9d9cca472181f2f0c83d8b0146d7627a9d7835d9032a61b9e688d55",
+    "url": "https://github.com/bksaiki/mpfx-lean/blob/8bd80452927ae9234fc378c07a00f2962e1e5b6f/Mpfx/Rounding/Ulp.lean",
+    "evidence": "SOURCE_ONLY_NOT_BUILT; mathematical application, not upstream import"
+  },
+  {
+    "repository": "thomasahle/fast-polynomials",
+    "revision": "09a36b0e7a6c153462bd43b91d4a3bb7ac886bef",
+    "source": "FastPoly/Cost/Circuit.lean",
+    "sha256": "1ed86f02b9321ca5d2ef17eb860db31801fed135e4a62b7d7035acb43372db0a",
+    "url": "https://github.com/thomasahle/fast-polynomials/blob/09a36b0e7a6c153462bd43b91d4a3bb7ac886bef/FastPoly/Cost/Circuit.lean",
+    "evidence": "SOURCE_ONLY_NOT_BUILT; mathematical application, not upstream import"
+  },
+  {
+    "repository": "thomasahle/fast-polynomials",
+    "revision": "09a36b0e7a6c153462bd43b91d4a3bb7ac886bef",
+    "source": "FastPoly/Cost/MultiplicationProgram.lean",
+    "sha256": "dcd92f8086d09d4be671e295db44dbcee16761b953ed43b5b8be2b6f77adf477",
+    "url": "https://github.com/thomasahle/fast-polynomials/blob/09a36b0e7a6c153462bd43b91d4a3bb7ac886bef/FastPoly/Cost/MultiplicationProgram.lean",
+    "evidence": "SOURCE_ONLY_NOT_BUILT; mathematical application, not upstream import"
+  }
+]
diff --git a/research/wordram-ntt-kernel/recovery/fixedpoint_fft.py b/research/wordram-ntt-kernel/recovery/fixedpoint_fft.py
new file mode 100644
index 0000000000..7ae4b7016f
--- /dev/null
+++ b/research/wordram-ntt-kernel/recovery/fixedpoint_fft.py
@@ -0,0 +1,167 @@
+"""Certified fixed-point FFT application. Python standard library only.
+Not a Word RAM cost certificate: products below may require multiword arithmetic.
+"""
+from fractions import Fraction as F
+from math import factorial
+import argparse, hashlib, json, random
+from pathlib import Path
+
+
+def nearest(x):
+    """Nearest integer; exact ties go toward positive infinity."""
+    return (2*x.numerator + x.denominator)//(2*x.denominator)
+
+
+def atan_interval(q, terms=100):
+    z=F(1,q)
+    total=sum(((-1)**j*z**(2*j+1)/ (2*j+1) for j in range(terms)),F(0))
+    nxt=(-1)**terms*z**(2*terms+1)/(2*terms+1)
+    return min(total,total+nxt),max(total,total+nxt)
+
+
+def pi_interval():
+    a,b=atan_interval(5); c,d=atan_interval(239)
+    return 16*a-4*d,16*b-4*c
+
+
+def certified_twiddles(n,bits):
+    """Each coordinate is within 1/(2*Q) of its true root coordinate.
+    Machin's formula and Taylor's theorem give rational certificates.
+    True forward twiddle is exp(-2*pi*i*k/n).
+    """
+    q=1<<bits; lo,hi=pi_interval(); mid=F(nearest((lo+hi)/2*(1<<96)),1<<96)
+    result=[]; maxrad=F(0)
+    for k in range(n//2):
+        if k==0: result.append((q,0)); continue
+        if 4*k==n: result.append((0,-q)); continue
+        kk=min(k,n//2-k)
+        x=2*mid*kk/n
+        c=sum(((-1)**j*x**(2*j)/factorial(2*j) for j in range(16)),F(0))
+        s=sum(((-1)**j*x**(2*j+1)/factorial(2*j+1) for j in range(16)),F(0))
+        # Taylor polynomial degrees 30 and 31; derivative magnitude <= 1.
+        perturb=F(2*kk,n)*max(abs(mid-lo),abs(hi-mid))
+        ec=abs(x)**31/factorial(31)+perturb
+        es=abs(x)**32/factorial(32)+perturb
+        if k>n//4: c=-c
+        a=nearest(c*q); b=nearest(-s*q)
+        assert abs(F(a,q)-c)+ec < F(1,2*q)
+        assert abs(F(b,q)+s)+es < F(1,2*q)
+        result.append((a,b)); maxrad=max(maxrad,ec,es)
+    return result, {'pi_lower':str(lo),'pi_upper':str(hi),
+       'max_taylor_and_argument_radius':str(maxrad),
+       'component_error_upper':str(F(1,2*q)),
+       'euclidean_error_upper':str(F(1,q))}
+
+
+def cmul(a,b,q,counter):
+    counter['complex_products']+=1
+    return nearest(F(a[0]*b[0]-a[1]*b[1],q)),nearest(F(a[0]*b[1]+a[1]*b[0],q))
+
+
+def fft(data,twiddles,q,inverse,counter):
+    n=len(data); out=list(data); j=0
+    for i in range(1,n):
+        bit=n>>1
+        while j&bit: j^=bit; bit>>=1
+        j^=bit
+        if i<j: out[i],out[j]=out[j],out[i]
+    length=2
+    while length<=n:
+        for offset in range(0,n,length):
+            for j in range(length//2):
+                w=twiddles[j*n//length]
+                if inverse: w=(w[0],-w[1])
+                u=out[offset+j]; v=out[offset+j+length//2]
+                t=cmul(v,w,q,counter) # exactly one shared product
+                out[offset+j]=(u[0]+t[0],u[1]+t[1])
+                out[offset+j+length//2]=(u[0]-t[0],u[1]-t[1])
+                counter['butterflies']+=1
+        length*=2
+    return out
+
+
+def budget(n,d,bits):
+    """Uniform Euclidean norm error bound, all admissible input digits.
+    Additions are exact integer additions; only complex products round.
+    """
+    delta=F(1,1<<bits); werr=delta
+    def stages(m,e):
+        ledger=[]
+        for stage in range(n.bit_length()-1):
+            # E + |w|E + W(M+E) + delta; |w|=1.
+            e=(2+werr)*e+werr*m+delta
+            m*=2
+            ledger.append({'stage':stage+1,'magnitude_upper':str(m),'error_upper':str(e)})
+        return m,e,ledger
+    m,e,fwd=stages(F(d),F(0))
+    ep=2*m*e+e*e+delta
+    mi,ei,inv=stages(m*m,ep)
+    # No rounding in normalization: interpreted output is integer/(Q*N).
+    return {'forward':fwd,'product_error':str(ep),'inverse':inv,
+      'coefficient_error_upper':str(ei/n),'strict_half':ei/n<F(1,2)}
+
+
+def schoolbook(a,b,n):
+    out=[0]*n
+    for i,x in enumerate(a):
+        for j,y in enumerate(b): out[i+j]+=x*y
+    return out
+
+
+def run(n=512,bits=40,cases=12):
+    assert n>=2 and n&(n-1)==0
+    q=1<<bits; d=15; width=n//2
+    tw,tc=certified_twiddles(n,bits)
+    bound=budget(n,d,bits); assert bound['strict_half']
+    if n==512 and bits==40: assert F(bound['coefficient_error_upper'])<F(1,1000)
+    if n==512: assert not budget(n,d,30)['strict_half']
+    rng=random.Random(20261024)
+    tests=[([0]*width,[0]*width),([d]*width,[d]*width),
+      ([d]+[0]*(width-1),[0]*(width-1)+[d]),
+      ([0]*(width-1)+[d],[0]*(width-1)+[d]),
+      ([d if i%2 else 0 for i in range(width)],[d if i%2 else 0 for i in range(width)])]
+    tests += [([-d]*width,[d]*width),([(-1)**i*d for i in range(width)],[d]*width),
+      ([rng.randrange(-15,16) for _ in range(width)],[rng.randrange(-15,16) for _ in range(width)])]
+    tests += [([rng.randrange(16) for _ in range(width)],[rng.randrange(16) for _ in range(width)]) for _ in range(cases)]
+    max_observed=F(0); counts=None
+    for a,b in tests:
+        counter={'complex_products':0,'butterflies':0}
+        aa=fft([(x*q,0) for x in a]+[(0,0)]*width,tw,q,False,counter)
+        bb=fft([(x*q,0) for x in b]+[(0,0)]*width,tw,q,False,counter)
+        prod=[cmul(x,y,q,counter) for x,y in zip(aa,bb)]
+        out=fft(prod,tw,q,True,counter)
+        actual=schoolbook(a,b,n)
+        recovered=[nearest(F(x,n*q)) for x,y in out]
+        assert recovered==actual
+        # Stronger than only comparing packed product: each coefficient exact.
+        for (x,y),z in zip(out,actual):
+            err=abs(F(x,n*q)-z)+abs(F(y,n*q))
+            max_observed=max(max_observed,err)
+        av=sum(v*16**i for i,v in enumerate(a)); bv=sum(v*16**i for i,v in enumerate(b))
+        assert sum(v*16**i for i,v in enumerate(recovered))==av*bv
+        assert counter['complex_products']==3*(n//2)*(n.bit_length()-1)+n
+        counts=counter
+    # Essential controls: equality at a half-step does not force recovery.
+    assert nearest(F(1,2))!=0
+    assert nearest(F(0))!=F(1,4) # missing integer-lattice membership
+    # Minimal accepted bit count for THIS conservative sufficient bound.
+    minbits=next(b for b in range(1,bits+1) if budget(n,d,b)['strict_half'])
+    return {'status':'PASS','n':n,'digit_base':16,'max_operand_digits':width,
+      'bits':bits,'tested_pairs':len(tests),'certificate':tc,'budget':bound,
+      'smallest_bits_satisfying_this_bound':minbits,
+      'max_observed_l1_coefficient_error':str(max_observed),
+      'literal_counts':counts,'unshared_complex_products':6*(n//2)*(n.bit_length()-1)+n,
+      'controls':{'half_step_boundary_rejects_universal_recovery':True,'lattice_membership_required':True},
+      'evidence':'Exact rational executable checks plus paper all-input proof; not Lean kernel verification; not RAM64 or kappa certificate.'}
+
+if __name__=='__main__':
+    ap=argparse.ArgumentParser(); ap.add_argument('--n',type=int,default=512)
+    ap.add_argument('--bits',type=int,default=40); ap.add_argument('--cases',type=int,default=12)
+    ap.add_argument('--output'); args=ap.parse_args()
+    result=run(args.n,args.bits,args.cases)
+    output=json.dumps(result,indent=2)
+    if args.output: Path(args.output).write_text(output+'\n',encoding='utf-8')
+    print(json.dumps({k:v for k,v in result.items() if k not in ('certificate','budget')},indent=2))
+
+
+
diff --git a/research/wordram-ntt-kernel/recovery/verification-31bits.json b/research/wordram-ntt-kernel/recovery/verification-31bits.json
new file mode 100644
index 0000000000..f06d2c8f1b
--- /dev/null
+++ b/research/wordram-ntt-kernel/recovery/verification-31bits.json
@@ -0,0 +1,126 @@
+{
+  "status": "PASS",
+  "n": 512,
+  "digit_base": 16,
+  "max_operand_digits": 256,
+  "bits": 31,
+  "tested_pairs": 20,
+  "certificate": {
+    "pi_lower": "84864088515595226663583152976728260179413074880032130329988380583936176755167227026651389449357910430614450064620430832501346936695503444635550910777273903039519780970570811508180702258807211347625227531217706657372591374251190395132849846601873565403063864402305670533556844393647008357335142383010670201592796977797818470195163758847920849799147264943952248127768212391387678801698663045441643125290163162347319527121439654522323279455729428487217276711037207704556103761531199119009526585982354597558875306739003608286978922389765020970851996844885880276504413649179603452845526234209559698992142724103536519493160985724492506772822491747294983645230986162361392240167777177837197368039788205080908/27013078356490253639151105438942813146905934880912526447139939700530374037581023433817463557767530479844522381643841135194969213474785918174891364100053416715331668732091281389566002025317332963337837764228481707366893452872699110237365337674789367251656031217126331591549943865161259717286179968117897575919804241433838750970265111960900589653097617148247355117037743451894447251076263310526262790605730774117235902357727080106727415268723728256036062527638426207458441813195050757686691475854564060749240974976833214552824271149324868370594274609201569101904311307109634904780218785115328941647719121258385675157892602565935555959882253405642738023535674696772035385805565965711139142513275146484375",
+    "pi_upper": "37142245634528118670709175687018898557191345949839870769939418332984443880169826782904443833860537468975705110476195634049363166215360132278653131754651249400620598943545529998763347159845772810988264698609460103523906696336320883428280774705539295728761110807652992804912565018277799432322132953462290007544924657560719648376613729505863086194635667194802098556944962684762778968603652615897788950519625612745070723613452437832686717743583801784418404097404643507072183209709881150328702173055243930863159259751869519764391358691401419682197854112124228031492467575456820865001055787019103593456207934383482437324109936430380263910650930384628695561443059848121538750171463958830425271060719546048/11822743980537041385458546523582751154087785088195465086019125934652043047907522379605339348824219849024230310062779509810301471207955882326504859902686147264286194539701371382488927900998465084355069836062254559341964186933307850981847892051430020155308919319132338190661028284326806129657297652403624575865182788043731180726118726895931701849187521729419720906950921487672855539589758280897683334765555038478508736873359657615731261387547367980268229953799139636674096135044489223615960625625673596728541593711959355820461945321915262500041260923829051094126639636521434719621600980863136561705729557106136830219136833461395789621978892791461431882992102158913549914132090634666383266448974609375",
+    "max_taylor_and_argument_radius": "96032876096991249562927612843093185250496912238733531747160979957126389447398907464896572673630039391657909795060622526535576425519284945067637229208056157465828565613612271990270016166121794385974453112123595800349969939452732914521342259872276835777527676410933168737339378343900416534883775334533331655737620738925379815122835114890355950477749847107713219833240687357910056088600165900598552965901273797280651658781672831855101920097765535297830222067545909097214577667345735915046989902135178445317815505847934243156313717813576202677514098016697678967505767338965743406051430848668358099443880305633252859515662610274116125186520817139704089892060059303971469234726770050053125560262632658473519387431013771490348771977197745347123123873251622925152016160424332416533836683041010637472892452342186304032344335668319502054088261844310621522274362445588854724900315478372474451671712742608094568932974047108721041068630872246278025061710564074794919870715129288725271174242625764991709560086163685299761349694034866986146377683284759085049475066331538154080649413233110399593317745081227571409135279748193484629526161944617624392246488667535145318640802319539413653661786704167208048559694219463588489425850772660855254127599485582023403650451486199753229825503632002020742214132997390127414157544138054829113004565149629932084374529520453386549474794325686992802603916512981623319574744755071499082014866228156938138159395974072622578693420562304187040851616364196383441749355131997931893962565161327551556201572500846748307985699997817395187080895901281188600144444312423438175156773906242434346055172633839772242244580282527017446929337/837530224113930607170362585959285890618571712586416747915416228911972623265445518530011254921328893867448368166066976073543940313594193798418109434708771848082478031981726646987430287126791768639024723461279325541392747609319832536669291864511136980436142546154718203344443949038038605614586221021609219966660411009254897310066070810896617514075057333929821772684002211683327931170940414022065850359854963082564957404311693386191170944211333886725778245543179967789112063512570913761440496904501495632408744958329885738844784559782528683390531068975731949956084378852163312602030297331507662432746388881997528967502144512060160826003574499901017703229537360923717820151426848721778729952135490720280608199718538929236051000693397430868524759971985882784168503289089554610682774653627994611173839192080715046663748102019664156260309144485148871062689287411295212409959933538422004462451417238214107750834553270241195009844661554308949736829963552872413351148508990256720436974054727164007165082136373937816103152242809605685807765775275225393540867313397141232323580788552679696910395638467791104967627724001169102160368512511289156388904666740804046230945080324076856079375802127702614864866511434528495052838157212460290342807376999769270832435419384891323750361155096412238685038773096992645743054501117246480786782309482548106893656664433777460099226910872929927768176818074430515652230627114320276836544278453776373947133609079296770402057230903050488960492658229248000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "component_error_upper": "1/4294967296",
+    "euclidean_error_upper": "1/2147483648"
+  },
+  "budget": {
+    "forward": [
+      {
+        "stage": 1,
+        "magnitude_upper": "30",
+        "error_upper": "1/134217728"
+      },
+      {
+        "stage": 2,
+        "magnitude_upper": "60",
+        "error_upper": "8455716865/288230376151711744"
+      },
+      {
+        "stage": 3,
+        "magnitude_upper": "120",
+        "error_upper": "53899080353120780289/618970019642690137449562112"
+      },
+      {
+        "stage": 4,
+        "magnitude_upper": "240",
+        "error_upper": "306390159831794469863774224385/1329227995784915872903807060280344576"
+      },
+      {
+        "stage": 5,
+        "magnitude_upper": "480",
+        "error_upper": "1636279663584324994260179840252677980161/2854495385411919762116571938898990272765493248"
+      },
+      {
+        "stage": 6,
+        "magnitude_upper": "960",
+        "error_upper": "8400779924223971057745256225834350462663712047105/6129982163463555433433388108601236734474956488734408704"
+      },
+      {
+        "stage": 7,
+        "magnitude_upper": "1920",
+        "error_upper": "41971987902924570568019860019209970278207895936614665289729/13164036458569648337239753460458804039861886925068638906788872192"
+      },
+      {
+        "stage": 8,
+        "magnitude_upper": "3840",
+        "error_upper": "205556429470052935703251579226565976681819589597996027649928508473345/28269553036454149273332760011886696253239742350009903329945699220681916416"
+      },
+      {
+        "stage": 9,
+        "magnitude_upper": "7680",
+        "error_upper": "991441495474984787063180360547362223769973562143742354182672138987643412152321/60708402882054033466233184588234965832575213720379360039119137804340758912662765568"
+      }
+    ],
+    "product_error": "924500427525239915252144982604405398882472917861704600673548969013070792416983262168872919506062992383019426586389397209579691070654708428113700573466745892564369409/3685510180489786476798393145496356338786055879312930105836138965083617346086082863365358130056307390177215209990980317284932211552660930305235775636164742230126362624",
+    "inverse": [
+      {
+        "stage": 1,
+        "magnitude_upper": "117964800",
+        "error_upper": "4188079341638655040465914230051872509943632529786231276554736583569492335814223818377930243363045220573724503883222013779894931223440768686115088278808118453851989480042397697/7914572847139345089936080672628710081124203171238778877250017794972711203409019749450124833959777439667125485632516458859243681097816038718961476963260581373331416708758372352"
+      },
+      {
+        "stage": 2,
+        "magnitude_upper": "235929600",
+        "error_upper": "18921304820492110052669950120546318975427719512195993207418958233310891786754848703720631817254753708370920285820656219373687453551953631865496547692386005690245845774266888633670696961/16996415770136547158066822609678996074546979767265021542382212422412913915547271767653200072487337141404458543559888032491090538804886631661104639320530795262202600666732583009015300096"
+      },
+      {
+        "stage": 3,
+        "magnitude_upper": "471859200",
+        "error_upper": "85276343011660491409262772692006992055141037084416492874049203356196298495360388463443940078761956024566612257196736772399943462179959259180723159779340451974485969447046483114573015669236826113/36499524940977561749129372845602330599145828057988479444633540143194201337669419092047302490538971198229138476588755258485509637771003503986021290557777713506015957394882119600662993537972830208"
+      },
+      {
+        "stage": 4,
+        "magnitude_upper": "943718400",
+        "error_upper": "383481741118365544715605399908271696252420376710158890799424574373534785781048997974615388238501234382224142139220864594428610422468306481332597305394354813690171915510004936659909085619136759925066170369/78382132970517478991165606422426233672355708521949855379734648809861125861064803929830588940942115354940041435601982738271645192059633193360683542052684438972998018132574030730004068581526319939960438784"
+      },
+      {
+        "stage": 5,
+        "magnitude_upper": "1887436800",
+        "error_upper": "1721012198293906356061210257381801150976590862216109474578467163931614861951169873577630568233555414502106251966313282115327368669944585290181514495312051229718996039271560049557510236052617738041853253588380286977/168324348849547952231711676252164117297610873690341563503944988898199428937506586307637329160882830439263455003397702966816621832005881723620090072660860187198567157476110227142133240252298326952681384055545004032"
+      },
+      {
+        "stage": 6,
+        "magnitude_upper": "3774873600",
+        "error_upper": "7709392679933405810919658482675521097280608798148136485103593610200621821293278478084465083730248267143934730122377896960502604750702321437170728897371591351266047235834250836061737119886305943253093571329191500487380172801/361473786714651839609485931802192366508973300717001923159475447150424810286233407987951861887389439612274926783780351561999781998832434041296198795326329101623141899709787663433296905279066051548640942013290819886814068736"
+      },
+      {
+        "stage": 7,
+        "magnitude_upper": "7549747200",
+        "error_upper": "34476107294967809844977633270640986493512210262787165296613396591445645623804145054824690747857287507472679554448434159414886479922730876439693085473989216016490957032256820865389894715055596360335044542373557623170037639453429727233/776259046150354467574489744231251277628443008558348305569526019013025476343188443165439204414323238975243865348565536603085790022057407195722143637520590569602227488010424952775132642815799222412631499596858234375446423426908028928"
+      },
+      {
+        "stage": 8,
+        "magnitude_upper": "15099494400",
+        "error_upper": "153934312920674444418621923799375282447456657270710060185444464985290579779853646407720141043648226385484403288024309136878832077417477839477850107928900464154218685810747186568071451807939232842458985403658573832430189750104317352436960329729/1667003608219963568519962947680314449286189580578977040099064452941009309454408017880358050217888572685732477648358310111472200413529841270090839013082707511523789394878503639615769571477953506182241254033971650495422687009369115322790969344"
+      },
+      {
+        "stage": 9,
+        "magnitude_upper": "30198988800",
+        "error_upper": "686313751529225431440916500910769191106880681821213786620669108714005524248036580998113508377836867231018126704458923434282876600073883259683737121861982602530664121089748241226260984310248058283166766073431092364395986750828989758585173419575482515457/3579862989809370150552347991709354811340217396521331566180181212788883000669113019918160533228078546928669938652374965009299607594634172087555628255195572452564109288497401512783350157684872347030630001028968155934491319200842197951919848388309286912"
+      }
+    ],
+    "coefficient_error_upper": "686313751529225431440916500910769191106880681821213786620669108714005524248036580998113508377836867231018126704458923434282876600073883259683737121861982602530664121089748241226260984310248058283166766073431092364395986750828989758585173419575482515457/1832889850782397517082802171755189663406191307018921761884252780947908096342585866198098193012776216027479008590015982084761399088452696108828481666660133095712823955710669574545075280734654641679682560526831695838459555430831205351382962374814354898944",
+    "strict_half": true
+  },
+  "smallest_bits_satisfying_this_bound": 31,
+  "max_observed_l1_coefficient_error": "26190265/1099511627776",
+  "literal_counts": {
+    "complex_products": 7424,
+    "butterflies": 6912
+  },
+  "unshared_complex_products": 14336,
+  "controls": {
+    "half_step_boundary_rejects_universal_recovery": true,
+    "lattice_membership_required": true
+  },
+  "evidence": "Exact rational executable checks plus paper all-input proof; not Lean kernel verification; not RAM64 or kappa certificate."
+}
diff --git a/research/wordram-ntt-kernel/recovery/verification.json b/research/wordram-ntt-kernel/recovery/verification.json
new file mode 100644
index 0000000000..3939d4bb36
--- /dev/null
+++ b/research/wordram-ntt-kernel/recovery/verification.json
@@ -0,0 +1,126 @@
+{
+  "status": "PASS",
+  "n": 512,
+  "digit_base": 16,
+  "max_operand_digits": 256,
+  "bits": 40,
+  "tested_pairs": 20,
+  "certificate": {
+    "pi_lower": "84864088515595226663583152976728260179413074880032130329988380583936176755167227026651389449357910430614450064620430832501346936695503444635550910777273903039519780970570811508180702258807211347625227531217706657372591374251190395132849846601873565403063864402305670533556844393647008357335142383010670201592796977797818470195163758847920849799147264943952248127768212391387678801698663045441643125290163162347319527121439654522323279455729428487217276711037207704556103761531199119009526585982354597558875306739003608286978922389765020970851996844885880276504413649179603452845526234209559698992142724103536519493160985724492506772822491747294983645230986162361392240167777177837197368039788205080908/27013078356490253639151105438942813146905934880912526447139939700530374037581023433817463557767530479844522381643841135194969213474785918174891364100053416715331668732091281389566002025317332963337837764228481707366893452872699110237365337674789367251656031217126331591549943865161259717286179968117897575919804241433838750970265111960900589653097617148247355117037743451894447251076263310526262790605730774117235902357727080106727415268723728256036062527638426207458441813195050757686691475854564060749240974976833214552824271149324868370594274609201569101904311307109634904780218785115328941647719121258385675157892602565935555959882253405642738023535674696772035385805565965711139142513275146484375",
+    "pi_upper": "37142245634528118670709175687018898557191345949839870769939418332984443880169826782904443833860537468975705110476195634049363166215360132278653131754651249400620598943545529998763347159845772810988264698609460103523906696336320883428280774705539295728761110807652992804912565018277799432322132953462290007544924657560719648376613729505863086194635667194802098556944962684762778968603652615897788950519625612745070723613452437832686717743583801784418404097404643507072183209709881150328702173055243930863159259751869519764391358691401419682197854112124228031492467575456820865001055787019103593456207934383482437324109936430380263910650930384628695561443059848121538750171463958830425271060719546048/11822743980537041385458546523582751154087785088195465086019125934652043047907522379605339348824219849024230310062779509810301471207955882326504859902686147264286194539701371382488927900998465084355069836062254559341964186933307850981847892051430020155308919319132338190661028284326806129657297652403624575865182788043731180726118726895931701849187521729419720906950921487672855539589758280897683334765555038478508736873359657615731261387547367980268229953799139636674096135044489223615960625625673596728541593711959355820461945321915262500041260923829051094126639636521434719621600980863136561705729557106136830219136833461395789621978892791461431882992102158913549914132090634666383266448974609375",
+    "max_taylor_and_argument_radius": "96032876096991249562927612843093185250496912238733531747160979957126389447398907464896572673630039391657909795060622526535576425519284945067637229208056157465828565613612271990270016166121794385974453112123595800349969939452732914521342259872276835777527676410933168737339378343900416534883775334533331655737620738925379815122835114890355950477749847107713219833240687357910056088600165900598552965901273797280651658781672831855101920097765535297830222067545909097214577667345735915046989902135178445317815505847934243156313717813576202677514098016697678967505767338965743406051430848668358099443880305633252859515662610274116125186520817139704089892060059303971469234726770050053125560262632658473519387431013771490348771977197745347123123873251622925152016160424332416533836683041010637472892452342186304032344335668319502054088261844310621522274362445588854724900315478372474451671712742608094568932974047108721041068630872246278025061710564074794919870715129288725271174242625764991709560086163685299761349694034866986146377683284759085049475066331538154080649413233110399593317745081227571409135279748193484629526161944617624392246488667535145318640802319539413653661786704167208048559694219463588489425850772660855254127599485582023403650451486199753229825503632002020742214132997390127414157544138054829113004565149629932084374529520453386549474794325686992802603916512981623319574744755071499082014866228156938138159395974072622578693420562304187040851616364196383441749355131997931893962565161327551556201572500846748307985699997817395187080895901281188600144444312423438175156773906242434346055172633839772242244580282527017446929337/837530224113930607170362585959285890618571712586416747915416228911972623265445518530011254921328893867448368166066976073543940313594193798418109434708771848082478031981726646987430287126791768639024723461279325541392747609319832536669291864511136980436142546154718203344443949038038605614586221021609219966660411009254897310066070810896617514075057333929821772684002211683327931170940414022065850359854963082564957404311693386191170944211333886725778245543179967789112063512570913761440496904501495632408744958329885738844784559782528683390531068975731949956084378852163312602030297331507662432746388881997528967502144512060160826003574499901017703229537360923717820151426848721778729952135490720280608199718538929236051000693397430868524759971985882784168503289089554610682774653627994611173839192080715046663748102019664156260309144485148871062689287411295212409959933538422004462451417238214107750834553270241195009844661554308949736829963552872413351148508990256720436974054727164007165082136373937816103152242809605685807765775275225393540867313397141232323580788552679696910395638467791104967627724001169102160368512511289156388904666740804046230945080324076856079375802127702614864866511434528495052838157212460290342807376999769270832435419384891323750361155096412238685038773096992645743054501117246480786782309482548106893656664433777460099226910872929927768176818074430515652230627114320276836544278453776373947133609079296770402057230903050488960492658229248000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "component_error_upper": "1/2199023255552",
+    "euclidean_error_upper": "1/1099511627776"
+  },
+  "budget": {
+    "forward": [
+      {
+        "stage": 1,
+        "magnitude_upper": "30",
+        "error_upper": "1/68719476736"
+      },
+      {
+        "stage": 2,
+        "magnitude_upper": "60",
+        "error_upper": "4329327034369/75557863725914323419136"
+      },
+      {
+        "stage": 3,
+        "magnitude_upper": "120",
+        "error_upper": "14129320516752506829668353/83076749736557242056487941267521536"
+      },
+      {
+        "stage": 4,
+        "magnitude_upper": "240",
+        "error_upper": "41122991119624320132586209354725720065/91343852333181432387730302044767688728495783936"
+      },
+      {
+        "stage": 5,
+        "magnitude_upper": "480",
+        "error_upper": "112444282222250106129717009489449589326285918699521/100433627766186892221372630771322662657637687111424552206336"
+      },
+      {
+        "stage": 6,
+        "magnitude_upper": "960",
+        "error_upper": "295576166516228645032850294527095031064691868397317359012937729/110427941548649020598956093796432407239217743554726184882600387580788736"
+      },
+      {
+        "stage": 7,
+        "magnitude_upper": "1920",
+        "error_upper": "756100115784644454203449283440218957136576631749966918980529383937180434433/121416805764108066932466369176469931665150427440758720078238275608681517825325531136"
+      },
+      {
+        "stage": 8,
+        "magnitude_upper": "3840",
+        "error_upper": "1895923422009600687306343753860634081506375278717972978946912441129193179508880864968705/133499189745056880149688856635597007162669032647290798121690100488888732861290034376435130433536"
+      },
+      {
+        "stage": 9,
+        "magnitude_upper": "7680",
+        "error_upper": "4681950083557499873676897302181266574674827070129198651882336601827378463992077351398995596557680641/146783911423364576743092537299333564210980159306769991919205685720763064069663027716481187399048043939495936"
+      }
+    ],
+    "product_error": "10555928795607497142190170063591154739502411132600801416823863671562017777617821004072840907263655744867570300294384475683064908519095170174181248492424857878683637712503655996894888784287084160075185164895911937/21545516652742137885659094560277007014094191832363720128504958578969526904000843047377578132593002296225722240434905979752527594496752860623371529300590103961416596156942109074193054752294185849943217159109760516096",
+    "inverse": [
+      {
+        "stage": 1,
+        "magnitude_upper": "117964800",
+        "error_upper": "24483539208466671218362408386524119228420294054532286022032118633611326680710868950364768196065790052224841948306401222895897821902845655605451404639288839280090196727286413875906383500383621501628108928267390097856875462657/23689546086131422960647270026588478931532074235789438036179382904450240366918592625898413220651954314430049601701829119967217713075482397330387684250506304003974227539380644310764545984368872754291732775783027172102246808682496"
+      },
+      {
+        "stage": 2,
+        "magnitude_upper": "235929600",
+        "error_upper": "56634404687492722253299774283407753265487595235513285858756157107040168225957943169856850287174765528177306061590507285394895594776261821844464505549487481305476852183529353318233330218569538363964720738173884340210495824575594932207617/26046931378436930758124421057504913270096712196546516251547882077203270460225125279380594534654508948214569963255598595491753131461403769845169359579417304867559209294976619368996399554343023534097519594280807038990979484521392426918608896"
+      },
+      {
+        "stage": 3,
+        "magnitude_upper": "471859200",
+        "error_upper": "130685615099585334747874601709992517500187420932678610787273989383576627823762824888777648571185394823445092283589516097540377515129623070435383866988385848840886536070546600291454433369004406667375267311065981152680503185840855743622331324952477697/28638903918474961204418783933674838490721739172170652529441449702311064005352904159345284265824628375429359509218999720074396860757073376700445026041564579620512874307979212102266801261478978776245040008231745247475930553606737583615358787106474295296"
+      },
+      {
+        "stage": 4,
+        "magnitude_upper": "943718400",
+        "error_upper": "300894237090723801450029546156046412888568473426148543876271503909284822303078049801113922412538126544329926094561366147446669422462725135766837662642451430288237750125715047996295489844530251115749641874431198952465159525954309635517231635720999511175972519937/31488807865122869393368946606905258090427358510263056881902260126273268613620094029570654385546278232018613516882486860685488436192434164121779142526563380772375266790330713043733329634453442159475340420497130656489612358376476868321800047085704593449207459741696"
+      },
+      {
+        "stage": 5,
+        "magnitude_upper": "1887436800",
+        "error_upper": "691389992232249675254229936931031265549177883231287733002929871318571543469934838285355866502704414143869592803775549318167039322738474632508972259699976166580781938192041342641637218474722079582234443367367768118793435643528423880011836242490641560361549836887432160608257/34622310392506957584946940144288832324819178359103260074178033026772100877957520390515409281853501465865381150278099185099233529659567999369251322492547208112268029722558797196081988742442283240850996127872528443254245182193766350116513179157596502523218400437714157458948096"
+      },
+      {
+        "stage": 6,
+        "magnitude_upper": "3774873600",
+        "error_upper": "1585730094345787448949058677304785231300764904111525924319653495874839637747941599962802516798071601426897456979369565357820996418920322389360655200897961221691880557161563273924762995746008140487063252485052989433546045847507128798519933590278839170773070847983353407317929355972182017/38067632857031246407630399952637454339360261162480498151827759598488080823306351962756308851101602575098847329028940110091637382285949586119445262876221302420044053515454972772932772091758022063878123412028196792475334366896073730256821732872925646925108354699626084168288392929655914496"
+      },
+      {
+        "stage": 7,
+        "magnitude_upper": "7549747200",
+        "error_upper": "3630757856821206812995615882767875671669976101429126817238625826726894331835339219934544899669143461811706544734950730157277092540608498071823353605723709059824490056348766601849551127206258818166810684309399328235419350233959360394793057081245413458572535536135634964208284162301689483972885610497/41855804968213567224547853478906320725054875457247406540771499545716837934567817284890561672488119458109166910841919797858872862722356017328064756151166307827869405370407152286801072676024887272960758524035337792904616958075776435777990406039363527010043736240963055342423554029893064011082834640896"
+      },
+      {
+        "stage": 8,
+        "magnitude_upper": "15099494400",
+        "error_upper": "8300121708835975526887678402133419059556848715325142592237878928224849720548644340645848338416076666556796777127298786680861398940912315867466778656291867236782412395498906915403014018540444568538070300074751729021234243894862952404372079057922187407285263987439559360583985995350448073145145995384031266471937/46020944252475287237870212884199033180620210660923048261998100776379565006208246561973370194536329221406749153247076699560650180816490655358168942243705375840708580716765564230733368217919000094579989235733761476822566574679670497657321756298451772713817730735254092349426494960250807374037851220383801379127296"
+      },
+      {
+        "stage": 9,
+        "magnitude_upper": "30198988800",
+        "error_upper": "18947053651719600199262265080231157643885909152033848862820775212294044446537119108470306938520718170635091186000956470590528305302573145381838947472853518417986898697048485892694005413609644806306152807002362366956442032540713377296933191676571100835180236963993864706673694206986263226444928865933129372061489242472185857/50600563326827654588123836679729326762389162441035529589225339506857584891998836722990095925359281123796769466079202977847452184346448369216753349985184627480379356069141590341116726935523304085309941919618186267140501870856173174654525838912289889085202514128089692388083353653807625633046581877161501565826926935273373696"
+      }
+    ],
+    "coefficient_error_upper": "18947053651719600199262265080231157643885909152033848862820775212294044446537119108470306938520718170635091186000956470590528305302573145381838947472853518417986898697048485892694005413609644806306152807002362366956442032540713377296933191676571100835180236963993864706673694206986263226444928865933129372061489242472185857/25907488423335759149119404380021415302343251169810191149683373827511083464703404402170929113783951935383945966632551924657895518385381565038977715192414529269954230307400494254651764190987931691678690262844511368775936957878360665423117229523092423211623687233581922502698677070749504324119849921106688801703386590859967332352",
+    "strict_half": true
+  },
+  "smallest_bits_satisfying_this_bound": 31,
+  "max_observed_l1_coefficient_error": "13604651/281474976710656",
+  "literal_counts": {
+    "complex_products": 7424,
+    "butterflies": 6912
+  },
+  "unshared_complex_products": 14336,
+  "controls": {
+    "half_step_boundary_rejects_universal_recovery": true,
+    "lattice_membership_required": true
+  },
+  "evidence": "Exact rational executable checks plus paper all-input proof; not Lean kernel verification; not RAM64 or kappa certificate."
+}
diff --git a/research/wordram-ntt-kernel/verify.py b/research/wordram-ntt-kernel/verify.py
new file mode 100644
index 0000000000..6695bdfd46
--- /dev/null
+++ b/research/wordram-ntt-kernel/verify.py
@@ -0,0 +1,44 @@
+"""Standalone portable replay of the bounded-kernel application."""
+import sys,json,hashlib,subprocess,time
+from pathlib import Path
+
+ROOT=Path(__file__).resolve().parent
+
+def main():
+    if not __debug__:
+        raise SystemExit('Run without Python -O: certificate assertions must be enabled.')
+    started=time.perf_counter()
+    manifest=json.loads((ROOT/'MANIFEST.json').read_text(encoding='utf-8'))
+    actual={x.relative_to(ROOT).as_posix() for x in ROOT.rglob('*') if x.is_file() and '__pycache__' not in x.parts and x!=ROOT/'MANIFEST.json'}
+    assert actual==set(manifest['files']), 'package file inventory mismatch'
+    for name,expected in manifest['files'].items():
+        assert hashlib.sha256((ROOT/name).read_bytes()).hexdigest()==expected, 'source drift: '+name
+    helper=json.loads((ROOT/'lean/STATUS.json').read_text())
+    assert helper['status']=='VERIFIED'
+    assert hashlib.sha256((ROOT/'lean/IntegerKernelRecovery20261024.lean').read_bytes()).hexdigest()==helper['sha256']
+    assert all(set(row['axioms'])<=set(helper['allowed_axioms']) for row in helper['theorems'])
+    subprocess.run([sys.executable,'-B','-m','unittest','discover','-s','ntt','-p','test_*.py'],cwd=ROOT,check=True)
+    sys.path.insert(0,str(ROOT/'ram'))
+    from ram.verify_wordram import run_checks
+    from ram.circuit_sharing import check as verify_circuit
+    from verify_integration import verify as integration
+    from recovery.fixedpoint_fft import run as recovery
+    ram=run_checks(); circuit=verify_circuit(); full=integration()
+    expected=json.loads((ROOT/'INTEGRATION-RESULTS.json').read_text())
+    assert full==expected, 'whole-program replay differs from retained source-bound result'
+    narrow=recovery(512,31,12);wide=recovery(512,40,12)
+    assert narrow['status']==wide['status']=='PASS'
+    assert narrow['smallest_bits_satisfying_this_bound']==31
+    from fractions import Fraction
+    assert Fraction(wide['budget']['coefficient_error_upper'])<Fraction(1,1000)
+    print(json.dumps({'status':'PASS','source_files':len(manifest['files']),
+      'ram_multiply_slice':ram['exhaustive_multiply_inputs'],
+      'ram_butterfly_cases':ram['butterfly_input_triples'],
+      'whole_program_cases':full['cases'],
+      'approximate_backend_cases_each_precision':wide['tested_pairs'],
+      'fused_static_instructions_512':full['records'][-1]['fused_static_instructions'],
+      'maximal_1024bit_operands':full['records'][-1]['comparisons'][1],
+      'seconds':round(time.perf_counter()-started,3),
+      'scope':'Portable source-integrity and executable replay; see paper for universal proof. No new kappa or complete Lean machine proof.'},indent=2))
+
+if __name__=='__main__':main()
diff --git a/research/wordram-ntt-kernel/verify_integration.py b/research/wordram-ntt-kernel/verify_integration.py
new file mode 100644
index 0000000000..834cb84e81
--- /dev/null
+++ b/research/wordram-ntt-kernel/verify_integration.py
@@ -0,0 +1,35 @@
+"""Independent end-to-end checks of literal programs, including dirty memory."""
+import json,random,time,hashlib
+from pathlib import Path
+from ram_multiplier import build_multiplier,execute,BASE
+from ntt.exact_ntt import multiply_digits,evaluate
+
+
+def verify():
+    rng=random.Random(20261024);records=[];total_cases=0
+    for s,t in [(1,1),(1,2),(2,2),(3,5),(8,8),(16,13),(64,64),(256,256)]:
+        fused=build_multiplier(s,t,True);duplicate=build_multiplier(s,t,False)
+        B=fused.butterflies
+        assert B==3*fused.n*(fused.n.bit_length()-1)//2
+        assert len(duplicate.program)-len(fused.program)==49*B
+        assert len(fused.program)<=60*B+193*fused.n+1144
+        cases=[([0]*s,[0]*t),([15]*s,[15]*t),([rng.randrange(BASE) for _ in range(s)],[rng.randrange(BASE) for _ in range(t)])]
+        if (s,t)==(1,1):cases=[([a],[b]) for a in range(BASE) for b in range(BASE)]
+        comparisons=[]
+        for a,b in cases:
+            f,fd=execute(fused,a,b,True);d,dd=execute(duplicate,a,b,True)
+            assert fd==dd
+            assert evaluate(fd,BASE)==evaluate(multiply_digits(a,b),BASE)
+            assert f.steps==sum(f.counts.values()) and f.steps<=len(fused.program)
+            saving=d.steps-f.steps
+            assert 33*B<=saving<=49*B
+            assert d.counts.get('mul',0)-f.counts.get('mul',0)==B
+            comparisons.append({'fused_steps':f.steps,'duplicate_steps':d.steps,'saved_instructions':saving,'fused_instruction_histogram':f.counts})
+            total_cases+=1
+        records.append({'lengths':[s,t],'n':fused.n,'butterflies':B,'fused_static_instructions':len(fused.program),'duplicate_static_instructions':len(duplicate.program),'owned_temporary_words':len(fused.temporaries),'output_words':len(fused.output),'comparisons':comparisons if s!=1 or t!=1 else {'exhaustive_256_cases':True,'minimum_steps':min(x['fused_steps'] for x in comparisons),'maximum_steps':max(x['fused_steps'] for x in comparisons)}})
+    return {'status':'PASS','cases':total_cases,'models':'Literal tcslib ISA at W=64; fixed lengths and fixed modulus; interpreted program includes setup, constant synthesis, arithmetic, carry, clearing and final accept','tests':'All single-hex-digit pairs; boundary/random cases through 1024-bit operands; dirty owned memory; operand/exterior preservation; all owned temporaries zero; independent NTT and integer product oracles; same-ABI fused vs recomputation control','records':records}
+
+if __name__=='__main__':
+    started=time.perf_counter();result=verify();result['wall_seconds']=time.perf_counter()-started
+    Path(__file__).with_name('integration-results.json').write_text(json.dumps(result,indent=2)+'\n',encoding='utf8')
+    print(json.dumps({'status':result['status'],'cases':result['cases'],'wall_seconds':result['wall_seconds'],'largest':result['records'][-1]},indent=2))