Top-level program tail: call FM and write the 2n-bit product

Proved

NLogN.main_tail

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

integer-multiplicationschonhage-strassen-tmturing-machines

Let $n\in\mathbb N$ , $s$ a state, and $a,b<2^n$ . Let $N_0 = 2^{|n+1|_2+1}$ (mainN0 n, where $|\cdot|_2$ is the bit length). Assume ARG is exactly $[b,a]$ , T1 and T2 are both exactly $[2^n]$ , PRM has $N_0$ , RN has $2^{N_0}$ and RF has $2^{N_0}+1$ on top. Run, in the Schönhage–Strassen program ssProg, the statement: call procedure $1$ (the FM procedure); shift T1 left by the ruler T2; write ARG with ruler T1. Then there is a final state $t$ with

\mathrm{IRuns}\ I\ \mathrm{ssProg}\ (\dots)\ s\ t\ \big(\Phi(N_0)+\mathrm{shlCost}(n)+\mathrm{outRCost}(2n)\big),\qquad t.\mathrm{out} = s.\mathrm{out}\mathbin{+\!\!+}\mathrm{bin}_{2n}(ab),

where $\Phi$ = fmPhi is the potential $\Phi(N)=2^{2100}\,N\,\ell(N)\,\lambda(N)$ ( $\ell$ = bit length of $N$ , $\lambda$ = bit length of $\ell^4$ ).

Since $N_0>2n$ , the residue $ab \bmod (2^{N_0}+1)$ equals $ab$ , so the output is the $2n$ -bit product. The cost bound $\Phi(N_0)$ for the FM call is the potential-function bound proved by induction on the recursion; this lemma combines it with output to finish the top-level analysis.

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. The input word $I$ is arbitrary here because the tail performs no reads.

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
set_option maxHeartbeats 2000000

Formal statement

theorem NLogN.main_tail {I : List Sym} (n : ℕ) (s : IState NS) (a b : ℕ) (ha : a < 2 ^ n)
    (hb : b < 2 ^ n) (LP LN LF : List Item) (hA : s.G ARG = [.int (b : ℤ), .int (a : ℤ)])
    (hT1 : s.G T1 = [.int (2 ^ n)]) (hT2 : s.G T2 = [.int (2 ^ n)])
    (hP : s.G PRM = .int (mainN0 n) :: LP) (hN : s.G RN = .int (2 ^ mainN0 n) :: LN)
    (hF : s.G RF = .int (2 ^ mainN0 n + 1) :: LF) :
    ∃ t, IRuns I ssProg (.seq (.call 1) (.seq (.op (.shl T1 T2)) (.op (.write ARG T1)))) s t
      (fmPhi (mainN0 n) + shlCost n + outRCost (2 * n)) ∧ t.out = s.out ++ bin (2 * n) (a * b) := 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.main_tail` of the Lean development NLogN/SSMain.lean (lines 183–214), written for the prove2.me integer-multiplication campaign.

View graph