Условная граница κ для целочисленного умножения пробила отметку 0,003
Κ = 0.003 for integer multiplication crossed
В pull request #4441 репозитория CrocSwap/integer-mult-bounds автор 1337isnot1337 объединил прореживание запросов из #4440 и новую ретайминговую границу вспомогательного блока, подняв условную κ до 0,00300105 — на 1,3868% выше, чем 0,00296 у #4440. Это даёт оценку T(n) = O(n (log n)^(1 − 0,00300105)). Утверждение остаётся условным и ждёт ревью: автор прямо оговаривает, что не заявляет ни безусловной теоремы, ни практической скорости.
Это авторская условная конструкция, прошедшая проверку и ожидающая ревью.
- jdb1729
@platypii и я занимались Lean-верификацией улучшений для kappa здесь: https://github.com/platypii/integer-mult-bounds-lean
Текущий статус кампании: kappa >= 2^-14.38 доказано безусловно на TM2-машине Mathlib. Приветствуется любой вклад!
- joeldw
Кто-нибудь знает простой способ понять, как именно работает это ускорение? Стандартное умножение O(N log N) использует частотное разложение через FFT, насколько я понимаю; как может выглядеть эта конструкция?
- readthenotes1
"Применить верифицированный fresh-helper retiming ко всем 19 полным нативным вызовам p17 query-thinned complex controller из #4440. Все 16 платных query shears, целые idle calls, main operators и более сильный BIT supplier сохранены."
Я понимаю многие из этих слов, но, видимо, ни одного в контексте...