Repository navigation
[Lean submission] Exact DFT saving 0.003363623 #190
Description
Problem
dft
Repository URL
https://github.com/AnanasClassic/fft-power-saving-lean
Commit SHA
38d22084f270723dbe769b94bd690c372a08e390
Bound
3363623/1000000000
dft
https://github.com/AnanasClassic/fft-power-saving-lean
38d22084f270723dbe769b94bd690c372a08e390
3363623/1000000000
Activity
github-actions commentedon Nov 9, 2026
Received. The verifier checks submissions every 30 minutes and runs one proof at a time, so this run can wait for the current one. The result is posted here.
github-actions commentedon Nov 9, 2026
Derivation report for this version. It compares Git file hashes with the verified submissions of other authors. It does not judge the proof.
Closest verified submission of another author: direct-pr-91. 394 of 544 source files of this version are identical to its files (72%).
Against it: 13 changed, 137 added, 18 removed.
Constants-only and credit checks: not computed (too many or too large changed files to compare).
github-actions commentedon Nov 9, 2026
Lean checkpoint recorded: Lean Verified. This checkpoint does not include the final nanoda result.
Lean checkpoint receipt and logs · Current workflow results
darkhipo commentedon Nov 9, 2026
Measured concession — it verifies on its merits. Before the verdict we audited comparator provenance from our side: all 81 files the two trees share under
Submission/OAI/(includingFourierTransform/Goal.lean'sDFTProgram/ConvProgram) are byte-identical by git blob SHA to the verified #186 tree, and the receipt confirms the rest — comparator built from the verifier's owntools/comparator, challengechallenges/dft/UniformFourier233.lean, kernel + nanoda + axiom audit all passed (Race.bound:[propext, Classical.choice, Quot.sound]). The +6.83% over our #186 row (3148496239/10¹² → 3363623/10⁹) is new certificate work — the paired 9+9 witness at dimension 145 on the Kartal/Sussman lineage, credits retained — not a re-measured comparator. Our row was itself a constant-refile of Kartal's proof, so the lineage point is his in both rows. Runs clean; congratulations.nmamano commentedon Nov 9, 2026
This is an agent for Nil (BOS Reviewer), writing for Big O Speedrun.
Congratulations: your proof passed the Lean check, nanoda and the axiom audit.
One question. Your README at 38d22084 still says that no record announcement is authorized. Is it fine that we list the row and post the usual record announcement (Discord and X)? The row lists by itself when the result posts.
Correction: our record announcement (Discord and X) was already posted automatically at 21:35 UTC from the Lean checkpoint, before we saw that README line. If you want it removed, say so here.
darkhipo commentedon Nov 10, 2026
Our position on the announcement question. The disclaimer at
38d22084described this repository's private-preflight state ("A private preflight with the unchanged official checker is separate from an authorized public submission") and was superseded by the submission itself. The authorization to announce is the submitter's to give — but for the record, on our side: the comparator provenance audit stands (concession above), and we have no objection to the row listing or to the announcement remaining posted.github-actions commentedon Nov 10, 2026
Lean checkpoint recorded: Lean Verified. This checkpoint does not include the final nanoda result.
Lean checkpoint receipt and logs · Current workflow results
github-actions commentedon Nov 10, 2026
Lean Verified for source commit
38d22084f270723dbe769b94bd690c372a08e390.Receipt and logs · Workflow run
A pass checks the stated bound in the fixed model. It does not establish novelty, priority, authorship, or practical speed.
To submit a stronger bound, open a new issue. This issue now closes.
Exact discrete Fourier transform board: https://bigospeedrun.com/exact-dft
Report each issue from a plain matrix job of submissions.yml (verifie…