FM recombination: Horner evaluation of M-bit digits by concatenation

Proved

NLogN.fmHorner_runs

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

integer-multiplicationschonhage-strassen-tmturing-machines

Let $n,M,k\in\mathbb N$ with $M\le n$ and $k+1\le n$ , and let $D=(d_0,\dots,d_{2^k-1})$ be a list of $2^k$ integers with $0\le d_i<2^M$ . Assume stack DG holds the items of $D$ in reverse order (last digit on top) followed by $L_G$ , DL has $2^k$ on top and RM has $2^M$ on top. Then fmHorner runs from $s$ to the state where DG is $L_G$ and

2^{2^k M}+\sum_{i<2^k} d_i\,2^{iM}

(i.e. $2^{2^kM}+\mathrm{zev}(2^M,D)$ ) is pushed on ZZ, with cost at most $2^k\,(2000(n+3)+30)+1000(n+3)$ .

The loop starts from the sentinel $1$ and concatenates one $M$ -bit digit per iteration (cat), so each step costs $O(M)$ regardless of the size of the accumulated number; this keeps recombination linear in $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.fmHorner_runs (s : IState NS) (n M k : ℕ) (Dg : List ℤ) (LG LL LM : List Item)
    (hM : M ≤ n) (hk : k + 1 ≤ n) (hDl : Dg.length = 2 ^ k)
    (hDg : ∀ b ∈ Dg, 0 ≤ b ∧ b < 2 ^ M)
    (hG : s.G DG = (ints Dg).reverse ++ LG) (hDL : s.G DL = .int (2 ^ k) :: LL)
    (hRM : s.G RM = .int (2 ^ M) :: LM) :
    IRuns I iprog fmHorner s
      ((s.upd DG LG).upd ZZ (.int (2 ^ (2 ^ k * M) + zev (2 ^ M) Dg) :: s.G ZZ))
      (2 ^ k * (2000 * (n + 3) + 30) + 1000 * (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.fmHorner_runs` of the Lean development NLogN/SSFM3.lean (lines 380–452), written for the prove2.me integer-multiplication campaign.

View graph