FM final correction: remove sentinel and carry, reduce modulo 2^N+1

Proved

NLogN.fmFinal_runs

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

integer-multiplicationschonhage-strassen-tmturing-machines

Let $N\ge1$ , $s$ a state, $0\le z<2^{N+1}$ and $|c|\le 2^N$ . Assume ZZ has $z$ on top (over $L_Z$ ), CY has $c$ on top (over $L_Y$ ), RN has $2^N$ and RF has $2^N+1$ on top. Then the segment fmFinal runs from $s$ to the state where ZZ and CY are popped and

(z-2^N-c)\bmod (2^N+1)

is pushed on ARG, with cost at most $25000\,(N+3)$ . The residue is the canonical one in $[0,2^N]$ (Lean's % with positive modulus).

In the Schönhage–Strassen procedure $z$ is the Horner value $2^N+\sum_i d_i 2^{iM}$ (with a leading sentinel $1$ ) and $c$ is the final carry, whose weight $2^N$ is $\equiv-1$ ; this step therefore produces the product modulo $2^N+1$ .

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.fmFinal_runs (s : IState NS) (N : ℕ) (z c : ℤ) (LZ LY LN LF : List Item) (hN1 : 1 ≤ N)
    (hz : 0 ≤ z ∧ z < 2 ^ (N + 1)) (hc : |c| ≤ 2 ^ N)
    (hZ : s.G ZZ = .int z :: LZ) (hY : s.G CY = .int c :: LY)
    (hN : s.G RN = .int (2 ^ N) :: LN) (hF : s.G RF = .int (2 ^ N + 1) :: LF) :
    IRuns I iprog fmFinal s
      (((s.upd ZZ LZ).upd CY LY).upd ARG (.int ((z - 2 ^ N - c) % (2 ^ N + 1)) :: s.G ARG))
      (25000 * (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.fmFinal_runs` of the Lean development NLogN/SSFM3.lean (lines 454–509), written for the prove2.me integer-multiplication campaign.

View graph