FM preprocessing loop: cut M-bit pieces and twist them by powers of 2^Q

Proved

NLogN.prepLoop_runs

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

integer-multiplicationschonhage-strassen-tmturing-machines

Let $n,M,Q,K\in\mathbb N$ with $KQ=n$ , $M\le n$ , $Q\le n$ and bit length of $K$ at most $n$ ; write $F=2^n+1$ , and let $x\in\mathbb Z$ . Assume XA has $x$ on top (over $L_X$ ), W has $1$ , CC has $K$ , RM has $2^M$ , RQ has $2^Q$ , RN has $2^n$ , RF has $F$ on top. Then the loop "while CC is nonzero do prepStep" runs from $s$ to the state where

\mathrm{XA}: \mathrm{qit}(M,K,x),\qquad \mathrm{QS} \mathrel{+}= \mathrm{reverse}\big(\mathrm{wtZ}(F,Q,0,\mathrm{pcs}(M,K,x))\big),\qquad \mathrm{W}: 2^n,\qquad \mathrm{CC}: 0

replace the tops of XA, W, CC (and the twisted pieces are pushed on QS, last on top), with cost at most $K\,(30000(n+3)+30)+30$ .

Here $\mathrm{pcs}(M,K,x)$ are the first $K$ signed $M$ -bit pieces of $x$ , $\mathrm{qit}(M,K,x)$ is the signed quotient left after $K$ cuts, and $\mathrm{wtZ}$ multiplies the $i$ -th piece by $2^{iQ}$ and reduces mod $F$ . Each iteration splits off one piece, shifts it by the current weight $W=2^{iQ}$ , reduces it, and multiplies $W$ by $2^Q$ . This is the loop inside fmPrep.

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.prepLoop_runs (s : IState NS) (n M Q K : ℕ) (x : ℤ) (LX LW LC LM LQ LN LF : List Item)
    (hKQ : K * Q = n) (hM : M ≤ n) (hQ : Q ≤ n) (hK : zsz (K : ℤ) ≤ n)
    (hX : s.G XA = .int x :: LX) (hW : s.G W = .int 1 :: LW) (hC : s.G CC = .int K :: LC)
    (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 (.loop CC (fun c => c != .zero) prepStep) s
      ((((s.upd XA (.int (qit M K x) :: LX)).upd QS
        ((ints (wtZ (2 ^ n + 1) Q 0 (pcs M K x))).reverse ++ s.G QS)).upd W
          (.int (2 ^ n) :: LW)).upd CC (.int 0 :: LC))
      (K * (30000 * (n + 3) + 30) + 30) := 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.prepLoop_runs` of the Lean development NLogN/SSFM1.lean (lines 180–227), written for the prove2.me integer-multiplication campaign.

View graph