FM preprocessing: cut into pieces, twist, and forward-transform one input

Proved

NLogN.fmPrep_runs

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

integer-multiplicationschonhage-strassen-tmturing-machines

Let pD have body difBody pD. Let $N,n,M,Q,k\in\mathbb N$ with $n\ge1$ , $2^kQ=n$ , $M\le n$ , $Q\le n$ , $k+1\le n$ ; write $F=2^n+1$ and $K=2^k$ . Let $x$ be an integer with $|x|<2^{KM}$ and bit length at most $N$ . Assume ARG has $x$ on top (over $L_A$ ), DX $=R$ , and the rulers $2^k$ on DL, $2^M$ on RM, $2^Q$ on RQ, $2^{2Q}$ on DE, $2^n$ on RN, $F$ on RF. Then fmPrep pD runs from $s$ to the state where $x$ is popped from ARG and

\mathrm{DX} = \mathrm{difZ}\big(F,\,2Q,\,k,\,\mathrm{wtZ}(F,Q,0,\mathrm{pcs}(M,K,x))\big)\mathbin{+\!\!+}R,

with cost at most $\mathrm{prepCost}(N,n,k)=\mathrm{difCost}(n,k)+40000\cdot2^k(n+3)+1000(N+n+10)$ .

Here $\mathrm{pcs}(M,K,x)$ are the $K$ signed $M$ -bit pieces of $x$ (least significant first), $\mathrm{wtZ}$ twists the $i$ -th piece by $2^{iQ}$ mod $F$ (with $(2^Q)^K=2^n\equiv-1$ , which turns cyclic into negacyclic convolution), and $\mathrm{difZ}$ is the forward decimation-in-frequency FFT with root $2^{2Q}$ . This is applied to each of the two factors.

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}

Formal statement

theorem NLogN.fmPrep_runs (pD : Fin P) (hPD : iprog pD = difBody pD) (s : IState NS) (N n M Q k : ℕ)
    (x : ℤ) (LA R LL LM LQ LE LN LF : List Item) (hn : 1 ≤ n) (hKQ : 2 ^ k * Q = n)
    (hM : M ≤ n) (hQ : Q ≤ n) (hkn : k + 1 ≤ n) (hx : x.natAbs < 2 ^ (2 ^ k * M))
    (hxN : zsz x ≤ N)
    (hA : s.G ARG = .int x :: LA) (hDL : s.G DL = .int (2 ^ k) :: LL) (hX : s.G DX = R)
    (hRM : s.G RM = .int (2 ^ M) :: LM) (hRQ : s.G RQ = .int (2 ^ Q) :: LQ)
    (hDE : s.G DE = .int (2 ^ (2 * Q)) :: LE)
    (hN : s.G RN = .int (2 ^ n) :: LN) (hF : s.G RF = .int (2 ^ n + 1) :: LF) :
    IRuns I iprog (fmPrep pD) s
      ((s.upd ARG LA).upd DX
        (ints (difZ (2 ^ n + 1) (2 * Q) k (wtZ (2 ^ n + 1) Q 0 (pcs M (2 ^ k) x))) ++ R))
      (prepCost N n k) := 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.fmPrep_runs` of the Lean development NLogN/SSFM1.lean (lines 236–310), written for the prove2.me integer-multiplication campaign.

View graph