Reduction of an integer modulo 2^n+1 in linear time

Proved

NLogN.fred_runs

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

integer-multiplicationschonhage-strassen-tmturing-machines

Let $X$ be a stack different from RN, RF, T1, T2, and let $n\in\mathbb N$ and $z\in\mathbb Z$ with $|z|<2^{2n+1}$ . Assume $X$ has $z$ on top (over $L$ ), RN has $2^n$ and RF has $2^n+1$ on top. Then fred X runs from $s$ to

s\big[X := (z \bmod (2^n+1)) :: L\big]

with cost at most $20000\,(n+3)$ ; the result is the canonical residue in $[0,2^n]$ .

The procedure splits $z$ twice by $2^n$ , uses $2^n\equiv-1$ to fold the pieces with additions and a negation, and then applies at most two additions and two subtractions of the modulus. It is the reduction step after every butterfly, twist and untwist in the Fermat ring.

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.fred_runs {X : Fin NS} (h1 : X ≠ RN) (h2 : X ≠ RF) (h3 : X ≠ T1) (h4 : X ≠ T2)
    (s : IState NS) (z : ℤ) (n : ℕ) (L LN LF : List Item) (hX : s.G X = .int z :: L)
    (hN : s.G RN = .int (2 ^ n) :: LN) (hF : s.G RF = .int (2 ^ n + 1) :: LF)
    (hz : z.natAbs < 2 ^ (2 * n + 1)) :
    IRuns I iprog (fred X) s (s.upd X (.int (z % (2 ^ n + 1)) :: L)) (20000 * (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.fred_runs` of the Lean development NLogN/SSBase.lean (lines 229–269), written for the prove2.me integer-multiplication campaign.

View graph