FM parameter computation pushes the rulers for the next level

Proved

NLogN.fmParams_runs

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

integer-multiplicationschonhage-strassen-tmturing-machines

Let pP be a procedure whose body is pow2Body pP. Let $N\in\mathbb N$ , with $\ell,\beta,k,M,Q,N'$ the parameters fmL, fmB, fmK, fmM, fmQ, fmN' of $N$ (as in fmMain_runs). Assume $\beta\le\ell/2$ , $k\le N'$ , $1\le N'\le N$ , $Q\le N$ , $\ell\le N$ and that PRM has $N$ on top. Then fmParams pP runs from $s$ to the state obtained by pushing

\mathrm{DL}\!:2^k,\ \mathrm{RM}\!:2^M,\ \mathrm{RQ}\!:2^Q,\ \mathrm{DE}\!:2^{2Q},\ \mathrm{RN}\!:2^{N'},\ \mathrm{RF}\!:2^{N'}+1,\ \mathrm{W2}\!:2^{N'-k},\ \mathrm{HB}\!:2^{N'-1},\ \mathrm{PRM}\!:N'

onto the respective stacks (all other stacks unchanged), with cost at most

1000(\ell+1)^2+1000(\beta+1)^2+30000(\ell+3)+180000(N+3).

These rulers ( $2^m$ items) drive the shifts and splits of the subsequent segments, and the new ring $\mathbb Z/(2^{N'}+1)$ on RN/RF together with $N'$ on PRM sets up the recursive calls. The computation uses bit lengths and a recursive power-of-two procedure, so its cost is $O(N)$ .

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.fmParams_runs (pP : Fin P) (hP : iprog pP = pow2Body pP) (s : IState NS) (N : ℕ)
    (LP : List Item) (hB : fmB N ≤ fmL N / 2) (hk : fmK N ≤ fmN' N) (hn1 : 1 ≤ fmN' N)
    (hnN : fmN' N ≤ N) (hQ : fmQ N ≤ N) (hℓ : fmL N ≤ N) (hPRM : s.G PRM = .int N :: LP) :
    IRuns I iprog (fmParams pP) s
      ((((((((((s.upd DL (.int (2 ^ fmK N) :: s.G DL)).upd RM (.int (2 ^ fmM N) :: s.G RM)).upd
        RQ (.int (2 ^ fmQ N) :: s.G RQ)).upd DE (.int (2 ^ (2 * fmQ N)) :: s.G DE)).upd
          RN (.int (2 ^ fmN' N) :: s.G RN)).upd RF (.int (2 ^ fmN' N + 1) :: s.G RF)).upd
            W2 (.int (2 ^ (fmN' N - fmK N)) :: s.G W2)).upd HB (.int (2 ^ (fmN' N - 1)) :: s.G HB)).upd
              PRM (.int (fmN' N) :: s.G PRM)))
      (1000 * (fmL N + 1) ^ 2 + 1000 * (fmB N + 1) ^ 2 + 30000 * (fmL N + 3) +
        180000 * (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.fmParams_runs` of the Lean development NLogN/SSFM4.lean (lines 329–369), written for the prove2.me integer-multiplication campaign.

View graph