Κ = 0.003 for integer multiplication crossed

aleph_minus_one

See also https://bigospeedrun.com/integer-multiplication

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...