FM pointwise products by recursive calls

Proved

NLogN.fmPw_runs

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

integer-multiplicationschonhage-strassen-tmturing-machines

Let pF satisfy FMSpec pF iprog I n C: calling it multiplies any $a,b\in[0,2^n]$ modulo $F=2^n+1$ (given PRM $=n$ , RN $=2^n$ , RF $=F$ on top) within cost $C$ . Let $A,B$ be lists of equal length of canonical residues mod $F$ , with the bit length of $|A|$ at most $n$ . Assume V holds $A$ over $R_V$ , DX holds $B$ over $R_X$ , DL has $|A|$ on top, and PRM, RN, RF hold $n$ , $2^n$ , $F$ on top. Then fmPw pF runs from $s$ to the state where V $=R_V$ , DX $=R_X$ , and the products

\mathrm{pmulZ}(F,A,B) = \big((a_i b_i)\bmod F\big)_i

are pushed onto P1 in reverse order (last on top), with cost at most

|A|\,\big(C+2000(n+3)+30\big)+1000(n+3).

This is the only place where the procedure recurses: the $K=2^k$ pointwise products of the transformed sequences are computed by $K$ calls of FM at the smaller size, which yields the term $2^k C$ in fmMain_runs.

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. FMSpec is a hypothesis about the procedure pF, discharged by induction on $N$ in the final proof.

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}

Formal statement

theorem NLogN.fmPw_runs (pF : Fin P) (n C : ℕ) (hFM : FMSpec pF iprog I n C) (s : IState NS)
    (A B : List ℤ) (RV RX LL LP LN LF : List Item) (hl : A.length = B.length)
    (hzK : zsz (A.length : ℤ) ≤ n) (hA : Canon (2 ^ n + 1) A) (hB : Canon (2 ^ n + 1) B)
    (hV : s.G V = ints A ++ RV) (hX : s.G DX = ints B ++ RX) (hL : s.G DL = .int A.length :: LL)
    (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 (fmPw pF) s
      (((s.upd V RV).upd DX RX).upd P1 ((ints (pmulZ (2 ^ n + 1) A B)).reverse ++ s.G P1))
      (A.length * (C + 2000 * (n + 3) + 30) + 1000 * (n + 3)) := 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.fmPw_runs` of the Lean development NLogN/SSFM2.lean (lines 78–136), written for the prove2.me integer-multiplication campaign.

View graph