Recursive inverse Fermat-ring FFT (decimation in time) is correct within its cost

Proved

NLogN.dit_runs

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

integer-multiplicationschonhage-strassen-tmturing-machines

Let pT be a procedure index whose body is ditBody pT and let $n\ge 1$ ; write $F=2^n+1$ . For every $j$ , every state $s$ , every list $B$ of integers and every $E\in\mathbb N$ , assume

$|B| = 2^j$ , and either $j=0$ or $2^j E = 2n$ (so $2^E$ is a $2^j$ -th root of unity mod $F$ , as $2^{2n}\equiv 1$ );
every entry of $B$ is a canonical residue, $0\le b<F$ ;
stack DX holds the items of $B$ (first entry on top) followed by $R$ ; DL has $2^j$ on top, DE has $2^E$ on top, RN has $2^n$ and RF has $F$ on top.

Then calling pT runs from $s$ to the state in which DX holds $\mathrm{ditZ}(F,n,E,j,B)$ followed by $R$ , all other stacks unchanged:

\mathrm{IRuns}\ I\ \mathrm{iprog}\ (\mathrm{call}\ pT)\ s\ \big(s[\mathrm{DX} := \mathrm{ints}(\mathrm{ditZ}(F,n,E,j,B))\mathbin{+\!\!+}R]\big)\ \big(500000\,(n+3)(j+1)\,2^j\big).

Here ditZ is the reference recursive decimation-in-time transform: it transforms the two halves recursively with $2E$ and combines them with butterflies whose twiddle factors are powers of $2$ , realised as shifts followed by reduction mod $F$ .

This is the inverse transform of the Schönhage–Strassen algorithm; with $j=k$ and $E=2Q$ it is applied once per recursion level, at cost $O(n\,k\,2^k)$ .

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.dit_runs (pT : Fin P) (hP : iprog pT = ditBody pT) (n : ℕ) (hn : 1 ≤ n) :
    ∀ j (s : IState NS) (B : List ℤ) (R LL LE LN LF : List Item) (E : ℕ),
      B.length = 2 ^ j → (j = 0 ∨ 2 ^ j * E = 2 * n) → Canon (2 ^ n + 1) B →
      s.G DX = ints B ++ R → s.G DL = .int (2 ^ j) :: LL → s.G DE = .int (2 ^ E) :: LE →
      s.G RN = .int (2 ^ n) :: LN → s.G RF = .int (2 ^ n + 1) :: LF →
      IRuns I iprog (.call pT) s (s.upd DX (ints (ditZ (2 ^ n + 1) n E j B) ++ R))
        (ditCost n j) := 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.dit_runs` of the Lean development NLogN/SSDit.lean (lines 317–539), written for the prove2.me integer-multiplication campaign.

View graph