Schoolbook multiplication of integer items in quadratic time

Proved

NLogN.smul_runs

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

integer-multiplicationschonhage-strassen-tmturing-machines

Let $A,X,Y,W,Q,R,T$ be seven pairwise distinct item stacks (in an arbitrary item-language program with $S$ stacks). Assume $A$ has $x$ and then $y$ on top (over $L$ ). Then the schoolbook procedure smul A X Y W Q R T runs from $s$ to

s\big[A := (x\cdot y) :: L\big]

with cost at most

\mathrm{smulCost}(|x|_2+|y|_2) = 2000\,(|x|_2+|y|_2+2)^2,

where $|z|_2$ is the bit length of $|z|$ . The loop repeatedly splits off the lowest bit of $y$ , adds $\pm x$ to the accumulator when it is nonzero, and shifts $x$ left by one bit.

This is the base case of FM: for $N$ with bit length below the threshold $2048$ , the product is computed by smul and reduced with fred; its cost is then bounded by a constant.

Formalization Note. Item states IState S have item stacks G (head = top), input pointer ip and output out; s.upd X L replaces stack X. IRuns asserts the exact final state and an upper bound on the cost. Unlike the other FM lemmas this one is stated for any number of stacks $S$ .

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
variable {S P : ℕ} {I : List Sym} {iprog : Fin P → IStmt S P}

Formal statement

theorem NLogN.smul_runs {A X Y W Q R T : Fin S} (hd : [A, X, Y, W, Q, R, T].Nodup)
    (s : IState S) (x y : ℤ) (L : List Item) (hA : s.G A = .int x :: .int y :: L) :
    IRuns I iprog (smul A X Y W Q R T) s (s.upd A (.int (x * y) :: L))
      (smulCost (zsz x + zsz y)) := 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.smul_runs` of the Lean development NLogN/ISchool.lean (lines 132–226), written for the prove2.me integer-multiplication campaign.

View graph