Schönhage–Strassen FM procedure: one recursion level is correct within its cost

Proved

NLogN.fmMain_runs

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

integer-multiplicationschonhage-strassen-tmturing-machines

Let pF, pD, pT, pP be procedure indices, where pD, pT, pP have bodies difBody pD, ditBody pT, pow2Body pP (forward FFT, inverse FFT, powers of two). Let $N\ge1$ and write $\ell$ = fmL N (bit length of $N$ ), $\beta$ = fmB N (bit length of $\ell$ ), $k=\lfloor \ell/2\rfloor-\beta$ , $K=2^k$ , $M=\lfloor N/K\rfloor$ , $Q=\lfloor (2M+2k+3)/K\rfloor+1$ and $N'=QK$ . Assume

(recursion hypothesis) FMSpec pF iprog I N' C: calling pF multiplies modulo $2^{N'}+1$ any two inputs in $[0,2^{N'}]$ within cost $C$ ;
the parameter conditions $\beta\le\ell/2$ , $KM=N$ , $M\ge1$ , $2M+2k+4\le N'\le N$ and $\ell\le N$ ;
ARG has $a$ then $b$ on top (over $L_A$ ) with $0\le a,b\le 2^N$ ; PRM has $N$ , RN has $2^N$ , RF has $2^N+1$ on top.

Then

\mathrm{IRuns}\ I\ \mathrm{iprog}\ (\mathrm{fmMain}\ pF\ pD\ pT\ pP)\ s\ \big(s[\mathrm{ARG} := (ab \bmod (2^N+1)) :: L_A]\big)\ \big(2^k C + \mathrm{fmLevelCost}(N)\big).

All other stacks are restored exactly.

fmMain folds the inputs, computes the parameters, splits each input into $K$ pieces of $M$ bits, twists them by powers of $2^Q$ , applies the forward FFT over $\mathbb Z/(2^{N'}+1)$ , multiplies pointwise by $K$ recursive calls, applies the inverse FFT, untwists, lifts to signed coefficients, propagates carries and recombines. The bound $\mathrm{fmLevelCost}(N) = 2\,\mathrm{difCost}+\mathrm{ditCost}+O(K N'+\ell^2+N)$ is $O(N\log N)$ ; solving the resulting recurrence gives the potential bound $A\,N\ell\lambda$ .

Formalization Note. States are IState NS records with item stacks G : Fin NS → List Item (head = top), input pointer ip and output out; s.upd X L replaces stack X by L; ints A is the list of integer items of A. The named stacks (ARG, PRM, RN, RF, DX, DL, …) are fixed indices in Fin 32. IRuns I iprog p s s' c means that p executes from s to exactly s' with some cost $c' \le c$ , so costs are upper bounds; the program text iprog and input I are arbitrary unless constrained.

Preamble

-- Schönhage–Strassen multitape-TM development (NLogN), generated by skeleton subtraction.

import Definitions.Def_IntMul_SS_Defs2

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN
open IntMul
variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt NS P}
set_option maxHeartbeats 4000000

Formal statement

theorem NLogN.fmMain_runs (pF pD pT pP : Fin P) (hPD : iprog pD = difBody pD)
    (hPT : iprog pT = ditBody pT) (hPP : iprog pP = pow2Body pP) (N C : ℕ)
    (hFM : FMSpec pF iprog I (fmN' N) C)
    (hN1 : 1 ≤ N) (hB : fmB N ≤ fmL N / 2) (hKM : 2 ^ fmK N * fmM N = N) (hM1 : 1 ≤ fmM N)
    (hnt : 2 * fmM N + 2 * fmK N + 4 ≤ fmN' N) (hnN : fmN' N ≤ N) (hℓ : fmL N ≤ N)
    (s : IState NS) (a b : ℤ) (LA LP LN LF : List Item) (ha : 0 ≤ a ∧ a ≤ 2 ^ N)
    (hb : 0 ≤ b ∧ b ≤ 2 ^ N) (hA : s.G ARG = .int a :: .int b :: LA)
    (hP : s.G PRM = .int N :: LP) (hN : s.G RN = .int (2 ^ N) :: LN)
    (hF : s.G RF = .int (2 ^ N + 1) :: LF) :
    IRuns I iprog (fmMain pF pD pT pP) s (s.upd ARG (.int ((a * b) % (2 ^ N + 1)) :: LA))
      (2 ^ fmK N * C + fmLevelCost N) := by sorry

Source

A. Schönhage, V. Strassen, Schnelle Multiplikation großer Zahlen, Computing 7 (1971), 281–292 (main theorem: O(n log n log log n) multitape TM multiplication). Lemma `NLogN.fmMain_runs` of the Lean development NLogN/SSFM5.lean (lines 38–244), written for the prove2.me integer-multiplication campaign.

View graph