What was already known
The textbook transform uses N log₂ N operations. Coppersmith, Feig and Linzer’s 1994 multiply-add construction uses (7/8) N log₂ N at powers of four, with an extra N/8 at odd powers of two. Sussman’s original 11 October note gives the new circuit; revision 2 adds its complete Lean checking report on 22 October.
This revision has no four-dimension assessment. Read the criteria.
AI involvement
Jacob Sussman directed the project. Claude agents wrote and ran the searches that found the retained circuits and wrote their proofs. The new sharing pattern and recursive circuit are the retained AI construction; the older Coppersmith–Feig–Linzer four-point step is credited separately.
Importance
Provides an explicit recursive circuit with a smaller leading operation count in this fixed model.
Limitations
This is a constant-factor bound, not a sub-N-log-N algorithm or an optimality result. A multiply-add counts as one line; charging each scalar multiplication separately changes the bound. The separate 5/6 arithmetic-operation theorem, asymptotic power-saving projects, hardware measurements and processor timings are outside this assessed contribution. Priority over the complete hardware literature remains unestablished.
Technical verification
Formal checking
Original note reports exact arithmetic replay on all unit inputs through 16,384 points; this does not check the all-size theorem.
- Checker
- Sussman project’s exact arithmetic replay programs
- Scope
- Finite circuit instances through 16,384 points in the stated operation models
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Correction and publication history
Added the 22 October Lean checking report for the exact multiply-add circuit bound.
Read this published revisionRecorded the original 11 October circuit construction and its finite exact checks. Complete all-size Lean checking is documented separately.
Read this published revision