CrocSwap pull request pushes the integer multiplication bound past κ = 0.003
Κ = 0.003 for integer multiplication crossed
A contributor to CrocSwap's integer-mult-bounds repository combines query thinning with fresh-helper retiming across 19 full native calls, raising the author-checked conditional bound to T(n) = O(n (log n)^(1 - 0.00300105)) — a 1.39% gain over PR #4440 and 30.5% over the pinned 0.0023. The claim remains conditional, awaiting review, with no unconditional theorem or practical runtime asserted.
This is an author-checked conditional construction awaiting review.
- jdb1729
@platypii and I have been pursuing Lean verification of improvements to kappa here: https://github.com/platypii/integer-mult-bounds-lean
Current status of the campaign: kappa >= 2^-14.38 proved unconditionally on Mathlib's TM2 machine. Contributions welcome!
- joeldw
Does anyone know if there's a simple way of understanding how exactly this speedup works? Standard O(N log N) multiplication uses frequency decomposition via FFT, iiuc; what might this construction look like?
- readthenotes1
"Apply the verified fresh-helper retiming to all 19 full native calls of #4440's p17 query-thinned complex controller. All 16 paid query shears, whole idle calls, main operators and the stronger BIT supplier are retained. "
I understand many of those words but apparently none of them within context...