Repository navigation
Prove complete clean six-tape multiplication and eight explicit applications - #2775
Merged
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
One fixed finite six-tape machine now returns the exact padded product and erases all five other tapes for every valid input width, including zero. Exact six-phase setup accounting (40n + 30 physical transitions) gives the complete upper bound 280n² + 278n + 68, with actual terminal heads and genuine halt. This extends the retained toolkit/multiplication lineage in PRs #1641 and #2235.
The Mathlib-only public package adds explicit bounded dirty windows; independent tape-origin relocation; exact setup invoices; fixed injective alphabet transport; minimal Nat.size operand width with literal padding; ZMod/signed residue labels; designated-tape endpoint adapters; and accumulator-output multiplication with literally unchanged input ABI. Window, width/residue and accumulator theorem statements retain the conservative 280n² + 322n + 122 bound.
Validation: all 74 bundled proof modules plus the aggregator rebuilt in a fresh directory with Lean 4.34.1 against pinned Mathlib d13f23b723b8a846827a245b89c10fc7d3f11612. The complete defining-module/transitive-axiom audit covered 5,350 declarations, including 2,824 theorems and 547 private declarations; only propext, Classical.choice and Quot.sound are admitted. Four actual Lean ownership/axiom fixtures and source/operational controls passed. External dependency binaries are supplied source-revision-checked cache artifacts, not independently rebuilt. Hosted CI and independent human review are not claimed.
The input is two supplied LSB stack words, not a serialized/signed parser. Residue output is the full double-width natural product, not an executed truncation. The fixed tape permutation preserves operand ABI as an adapter; multiplication consumes the operands. This is quadratic execution infrastructure, not a new kappa or the full fast multiplication algorithm.
Refreshed main 8e22a9d and 1,898 recently updated PR metadata records. Compared actual relevant sources, including existing alphabet/multiplication work linked by #2411 and paid return/output/widening/padding #2418/#2438/#2439/#2635/#2636. FRONTIER.md and reviews record substantial overlap and bounded coverage; no first-use claim. Existing arithmetic, compiler, PR64/1379/1641 and Mathlib attribution and licenses remain.
Substantial OpenAI Codex assistance included one root plus three parallel agents. Open next questions: charged serialized/signed parsing, marked-caller bank integration, and variable-depth physical recursion/routing.