The multiplication procedure of the HvdH machine is correct with cost G

Proved

NLogN.Top.mul_ok_all

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

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

Assume StepOK st n₀ lin calls, and let iprog be a five-procedure item-language program whose procedure 1 is the compiled multiplication routine mulRM n₀ st and whose procedures 2, 3, 4 are the DIF, DIT and bit-length procedures. Let $G:\mathbb N\to\mathbb N$ be monotone with, for every $N$ ,

\mathrm{topCost}(n_0,N) + \begin{cases}\mathrm{smallCost}(N) & N<n_0\\ \mathrm{lin}(N)+\sum_{(c,m)\in\mathrm{calls}(N)} c\,G(m) & N\ge n_0\end{cases} + 2 \le G(N).

Then for every bound $n$ , procedure 1 correctly multiplies (MulOK) according to the spec Mlt G n: for all integers $a,b$ of bit length $<n$ and any state whose argument stack starts with $a,b$ , calling procedure 1 replaces them by $a b$ within $G(\max(\mathrm{zsz}\,a,\mathrm{zsz}\,b))$ steps.

Formalization Note. Proved by strong induction on $n$ (the recursive calls are on strictly smaller sizes). IRuns I iprog p s s' c is the big-step semantics of the item language with cost bound $c$ . The machine layer: IState HS is a state with $64$ stacks of items (Item = integer or mark), an input position and an output; RM programs (straight-line register code RS, loops rep, conditionals, calls of the multiplication procedure through a MulSpec $M$ giving its domain and cost) have a functional semantics p.run s, a definedness predicate p.ok M s and a cost p.cost M s; Spec M p s s' c abbreviates p.ok M s ∧ p.run s = s' ∧ p.cost M s ≤ c. ints L / gints U push an integer list / a list of pairs as items (head = top); zsz z is the bit length of $|z|$ . MulBnd M m Φ says the multiplication procedure accepts all pairs of integers of bit length $\le m$ at cost $\le Φ$ . Register names (GU, CR, KB, XN, …) are fixed stack indices.

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.Top
open IntMul NLogN

Formal statement

theorem NLogN.Top.mul_ok_all {st : RM} {n₀ : ℕ} {lin : ℕ → ℕ} {calls : ℕ → List (ℕ × ℕ)}
    (hst : StepOK st n₀ lin calls) {I : List Sym} {iprog : Fin 5 → IStmt HS 5}
    (h1 : iprog 1 = (mulRM n₀ st).code 1 pcH)
    (h2 : iprog 2 = (difBody 2).ren ssH id) (h3 : iprog 3 = (ditBody 3).ren ssH id)
    (h4 : iprog 4 = blenProc) (G : ℕ → ℕ) (hGm : Monotone G)
    (hG : ∀ N, topCost n₀ N + (if N < n₀ then smallCost N else
        lin N + ((calls N).map fun q => q.1 * G q.2).sum) + 2 ≤ G N) :
    ∀ n, MulOK I iprog 1 (Mlt G 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.Top.mul_ok_all` of the Lean development NLogN/HTopInd.lean (lines 28–53), written for the prove2.me integer-multiplication campaign.

View graph