Un pull request de CrocSwap eleva κ a 0,00300105 en la cota de la multiplicación entera
Κ = 0.003 for integer multiplication crossed
El colaborador 1337isnot1337 combina el adelgazamiento de consultas del PR #4440 con una nueva reordenación temporal del helper para subir κ de 0,00296 a 0,00300105 (+1,3868%) en la cota condicional T(n) = O(n (log n)^(1 - 0,00300105)). La construcción recorta las llamadas pagadas de 72.902 a 69.273 y demuestra con intervalos exactos que la raíz del perfil fijo queda entre 0,0030010541830 y 0,0030010541834. El autor la presenta como una construcción condicional verificada por él mismo y pendiente de revisión.
La enorme palabra sigue siendo algorítmica en lugar de materializada.
- jdb1729
@platypii y yo hemos estado trabajando en la verificación con Lean de mejoras a kappa aquí: https://github.com/platypii/integer-mult-bounds-lean
Estado actual de la campaña: kappa >= 2^-14.38 demostrado de forma incondicional en la máquina TM2 de Mathlib. ¡Se agradecen contribuciones!
- joeldw
¿Alguien sabe si hay una forma sencilla de entender cómo funciona exactamente esta aceleración? La multiplicación estándar O(N log N) usa descomposición en frecuencias mediante FFT, si no me equivoco; ¿cómo podría ser esta construcción?
- 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. "
Entiendo muchas de esas palabras, pero al parecer ninguna dentro del contexto...