The Fermat-ring products of one HvdH step cost at most a quarter of T'(N)

Proved

NLogN.Asym.fermat_part

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

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

Let $K \ge 10^4$ and $N \ge 2^{2^{8K}+1}$ , and let $q = \mathrm{mkParams}(K,N)$ be the published parameter choice of the Harvey–van der Hoeven step. With $T'(m) = (m+1)(\mathrm{zsz}(m)+2)$ ,

4\cdot\bigl(3\cdot 2^{\mathrm{logOuter}(q)}\cdot T'(f_n(q)+1)\bigr) \le T'(N),

where $f_n(q) = 4\cdot 2^{e}\cdot P$ is the Fermat exponent (products are computed modulo $2^{f_n}+1$ ) and $2^{\mathrm{logOuter}}$ is the number of outer Fermat-ring products per transform. Thus the three batches of recursive Fermat-ring multiplications contribute at most $T'(N)/4$ to the recursion inequality.

Formalization Note. mkParams, Params.fn, Params.logOuter are from the published definition Def_IntMul_HvdH_MachineRef; TT' is defined in IntMul_HvdH_M_Defs3.

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

set_option linter.unusedSimpArgs false
open NLogN
open NLogN.Asym
open IntMul NLogN NLogN.Top IntMul.HvdH IntMul.HvdH.Ref

Formal statement

theorem NLogN.Asym.fermat_part (K : ℕ) (hK : 10 ^ 4 ≤ K) (N : ℕ) (hN : 2 ^ (2 ^ (8 * K) + 1) ≤ N) :
    4 * (3 * 2 ^ (mkParams K N).logOuter * TT' ((mkParams K N).fn + 1)) ≤ TT' N := 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.Asym.fermat_part` of the Lean development NLogN/HAsym.lean (lines 305–320), written for the prove2.me integer-multiplication campaign.

View graph