Repository navigation
Lower rational FFT and conditioned Toeplitz programs to fixed Hadamard stages - #4253
Merged
Mister-Meeseeks merged 5 commits intoOct 21, 2026
Merged
Conversation
jmbarrancoml
marked this pull request as ready for review
October 20, 2026 21:31
jmbarrancoml
marked this pull request as draft
October 20, 2026 21:53
jmbarrancoml
marked this pull request as ready for review
October 20, 2026 22:39
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
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.
I connect the actual rational FFT and complete conditioned Toeplitz program from PR #4205 to the retained fixed-Hadamard compiler. I preserve the original six-H words and Beneš stage counts, complete mixed singleton/two-wire layers, and execute the stored inverse with its scalar reciprocals and reversed gate order.
Under the retained leading-section and phase contracts, I give one coefficient/data grid with error below
2^-tagainst the same root or its inverse and signed widthsO(F0+t+log N+log lambda+log Q+log R). The new argument includes the final matrix norm in suffix amplification, adds the upstream coefficient defect, and charges rounding after each emitted stage. A scaled zero-shear program gives a suffix more than six times the invalid unit-endpoint allowance. DENSE-PROOF.md derives the corrected bound and states its dependencies.I preserve completed FFT head
6f17e6208a78cfade27f5c8f03383256f586ab24and its unchanged scientific receipt. The full extension retains unchanged source modules and proofs from PR #4205 head78c72e563173f3822fcb4efed9ceeccf05630258. I bind root admission, both actual plans, request bounds and prepared pages; controls reject changes after preparation.Verification uses four registered normal/optimized commands with an 840-second total allowance:
The new receipt covers 11 roots in both directions, 146,262 native stages and 992,742 complex roundings. I compare complete outputs with stored logical execution and exact root/inverse references, including reversed wires and 512-bit incoming data. Four generic cases cover mixed, idle, zero/tiny and empty programs; 24 shear words cover 2,184 segments and inverses; 25 controls check admission, precision and source/request/page integrity. The prior FFT receipt retains 13 cases, 2,525 stages and 23 controls. The canonical handoff records exact committed-export and hosted evidence.
All four registered and Git-free commands pass, with 35 export files unchanged. Hosted run 39508290934 passes and matches all four scientific records and both complete receipt digests. I checked the exact test-merge parents and publication tree. The first attempt failed during temporary Git-directory cleanup in an unchanged helper test, before package execution. The final empty retry commit has the same complete tree and export payload as the verified implementation commit.
I execute arithmetic H/2 stages. Physical T74 calls, complete tensor admission, setup/delivery/tape costs and the outer multiplication theorem remain open. Reviewers still need to assess the quantified proofs; finite replay does not establish them. The rounded forward/reverse programs need not be exact inverses. I make no selected-frontier change.
I credit Vlado Vojdanovski for the words, routing, full circuits and preceding stability structure; Chafik Boukhalfa for certified phases; and the retained rational-generator/Gaussian and classical LDU/Schur/perturbation lineage. Jose Manuel (
jmbarrancoml), with substantial OpenAI Codex assistance in mathematics, source analysis, implementation and writing. Internal agents belong to the author process.