Repository navigation
Research: execute certified Gaussian resampling through exact integer recovery - #2313
Merged
Mister-Meeseeks merged 1 commit intoOct 15, 2026
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
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.
PR2298 leaves its actual Gaussian resampling routines unexecuted and asks for an independent implementation with rigorous enclosures. This package implements that numerical path through exact integer output: periodic Gaussian expansion, nearest-coordinate selection, Neumann correction, retained permutations, executed normalized FFTs, two forward transforms, pointwise products, the opposite transform, CRT, integer decoding and carry propagation.
Status: independent implementation and finite uniform correctness certificate. At source lengths
5,7,13, target lengths8,16,32,alpha=5, numerical precision 256 and enclosure precision 448, the certificate covers every pair of nonnegative inputs up to 14,592 bits. Its uniform coefficient recovery error is less than 2^-49. This is an operator/error argument for the whole input domain, supported by examples; it is not an exhaustive input search.All acceptance arithmetic is integer or rational. Infinite Gaussian tails and the inverse remainder are enclosed explicitly. Independent odd-order Fourier matrices bound the entire Gaussian operator residual, which is charged in the error budget; those matrices do not supply the multiplication output. Recovery requires a unique integer in each enclosure before computing the final bits.
PROOF.mdsections 3–6 are the main review target.Local evidence covers 243 complete operator entries, 30 rounded complex-vector executions, and 289 complete integer products, including maximal 14,592-bit inputs. Those products execute 10,548 Gaussian line calls and independently check all 9,155 recovered coefficients. Controls exercise permutations, selectors, a required inverse correction, nonzero periodic windings, normalization, precision and input domains. Removing the correction is tested as a failure only where its effect exceeds the numerical budget.
Both registered normal and optimized replays passed on CPython 3.12.14/macOS arm64. A standalone read-only export reproduced the receipt without Git or network; a corrupted pinned source was rejected before imports. The package also includes a CLI for individual products. Metadata/source pins and the staged whitespace check passed. No hosted-CI pass is claimed at submission.
Limits: this is a dense reference implementation with indexed arrays and a conventional FFT. It does not run the selected recursive suppliers, implement the fast Gaussian chirp/tape routines, or establish their cost. These small valid Gaussian boxes are not the eventual outer parameter regime. It supplies an executable oracle for those future implementations, not a new kappa, selected-frontier change or all-size faster multiplication theorem. The written finite proof still needs independent review; it is not formal-kernel verification.
Base:
0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2, priority revision 4. PR2298 is pinned at8507498d363735ced0b0a3f02d5ecf80ed3e3805; relevant PR2234/2287 heads and the canonical base were rechecked. The final overlap refresh covered 527 open PRs, 1,022 Discussion records and 1,538 local records, with complete remote pagination and no warnings; it excludes arbitrary code diffs. No matching integrated numerical implementation was found. Coordination: Discussion2291 claim.Mason Hale, with substantial OpenAI Codex assistance in mathematics, implementation, verification and writing. Credit Harvey and van der Hoeven for the Gaussian algorithms, OpenAI's frozen outer formulas, Jose Manuel's immediate handoff and proposed callees, and the PR371/684/902/1430 audit lineage.
NOTICE.mdandSOURCES.jsonpreserve attribution and exact pins. New work is Apache-2.0; no independent human review is claimed.