Additive bound for the cost of the Fermat-ring convolution program

Proved

NLogN.FW.fwCost_le_add

by xuanji · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

harvey-van-der-hoeven-tminteger-multiplicationturing-machines

For HvdH parameters $q$ with $P\ge 1$ and $K\ge 1$ and all $kb, Φ_m$ , with $T = 2^{\mathrm{logOuter}}\cdot r$ ,

\mathrm{fwCost}(q,kb,Φ_m) \le 10^9 K\bigl(T(P+1)(e+kb+1) + 2^{\mathrm{logOuter}}(kb+1)^2\bigr) + 2^{\mathrm{logOuter}}Φ_m.

So the Fermat-ring convolution costs $O(K\,T\,P\,(e+kb))$ machine steps plus one recursive multiplication per Fermat-ring coefficient.

Formalization Note. fwCost is the explicit cost of fwP (sum of the encoding, transform-pass, pointwise-product, decoding and move costs encCost, passCost, pmCost, dcCost).

Preamble

-- Harvey–van der Hoeven multitape-TM development (NLogN), generated by skeleton subtraction.

import Definitions.Def_IntMul_HvdH_M_Defs4

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN
open NLogN.FW
open IntMul IntMul.HvdH NLogN

Formal statement

theorem NLogN.FW.fwCost_le_add (q : Ref.Params) (kb Φm : ℕ) (hP : 1 ≤ q.P) (hK1 : 1 ≤ q.K) :
    fwCost q kb Φm ≤ 10 ^ 9 * q.K * (2 ^ q.logOuter * q.r * (q.P + 1) * (q.e + kb + 1) +
      2 ^ q.logOuter * (kb + 1) ^ 2) + 2 ^ q.logOuter * Φm := by sorry

Source

D. Harvey, J. van der Hoeven, Integer multiplication in time O(n log n), Ann. of Math. 193 (2021), 563–617 (Theorem 1.1: multitape Turing machine multiplication in O(n log n)). Lemma `NLogN.FW.fwCost_le_add` of the Lean development NLogN/HFW11.lean (lines 32–42), written for the prove2.me integer-multiplication campaign.

View graph