FM post-processing: untwist, lift to signed coefficients and carry into M-bit digits

Proved

NLogN.fmPost_runs

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

integer-multiplicationschonhage-strassen-tmturing-machines

Let $n\ge1$ , $1\le M\le n$ , $k+1\le n$ and $Q$ with $2^kQ=n$ ; write $F=2^n+1$ and $K=2^k$ . Let $D$ be a list of $K$ canonical residues mod $F$ . Assume DX holds $D$ (first entry on top) over $R_X$ , and the rulers $2^k$ on DL, $2^{n-k}$ on W2, $2^{n-1}$ on HB, $2^M$ on RM, $2^Q$ on RQ, $2^n$ on RN, $F$ on RF. Let

(d, c) = \mathrm{carZ}\big(M,\ \mathrm{liftL}(n,k,Q,K,D),\ 0\big),

where $\mathrm{liftL}$ maps $D_i$ to $\big(((D_i 2^{(K-i)Q} \bmod F)\,2^{n-k}+2^{n-1})\bmod F\big)-2^{n-1}$ (untwisting, division by $K$ via $2^{2n}\equiv1$ , and lifting to the symmetric range), and $\mathrm{carZ}$ propagates carries, producing digits $d_i=(e_i+c_i)\bmod 2^M$ and final carry $c$ . Then fmPost runs from $s$ to the state where DX is $R_X$ , the digits $d$ are pushed on DG in reverse order (last on top) and $c$ is pushed on CY, with cost at most

2^k\,(60000(n+3)+30)+2000(n+3).

Applied to the inverse FFT output, the lifted coefficients are exactly the negacyclic convolution of the input pieces (ss_lift); this step turns them into base- $2^M$ digits for recombination.

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.fmPost_runs (s : IState NS) (n M Q k : ℕ) (D : List ℤ)
    (RX LL L2 LH LM LQ LN LF : List Item)
    (hn : 1 ≤ n) (hM1 : 1 ≤ M) (hM : M ≤ n) (hKQ : 2 ^ k * Q = n) (hk : k + 1 ≤ n)
    (hDl : D.length = 2 ^ k) (hD : Canon (2 ^ n + 1) D)
    (hX : s.G DX = ints D ++ RX) (hDL : s.G DL = .int (2 ^ k) :: LL)
    (h2 : s.G W2 = .int (2 ^ (n - k)) :: L2) (hH : s.G HB = .int (2 ^ (n - 1)) :: LH)
    (hRM : s.G RM = .int (2 ^ M) :: LM) (hRQ : s.G RQ = .int (2 ^ Q) :: LQ)
    (hN : s.G RN = .int (2 ^ n) :: LN) (hF : s.G RF = .int (2 ^ n + 1) :: LF) :
    IRuns I iprog fmPost s
      (((s.upd DX RX).upd DG ((ints (carZ M (liftL n k Q (2 ^ k) D) 0).1).reverse ++ s.G DG)).upd
        CY (.int (carZ M (liftL n k Q (2 ^ k) D) 0).2 :: s.G CY))
      (2 ^ k * (60000 * (n + 3) + 30) + 2000 * (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.fmPost_runs` of the Lean development NLogN/SSFM3.lean (lines 318–362), written for the prove2.me integer-multiplication campaign.

View graph