Stack-machine concatenation a·2^m + b of integer items runs in O(m)

Proved

NLogN.Runs.catR

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

integer-multiplicationschonhage-strassen-tmturing-machines

Let $q,i,j,k,t_1,t_2$ be pairwise distinct stacks of a state $\sigma$ ( $q$ control stack, $t_1,t_2$ scratch). Let $a\neq 0$ be an integer, $m\in\mathbb N$ and $0\le b<2^m$ . Assume stack $i$ is $\mathrm{enc}(a)$ followed by $R_i$ , stack $j$ is $\mathrm{enc}(2^m)$ (a "ruler") followed by $R_j$ , stack $k$ is $\mathrm{enc}(b)$ followed by $R_k$ ; $R_i$ , $R_k$ and the tops of $t_1,t_2$ do not start with a bit symbol. Then catR q i j k t1 t2 runs from $\sigma$ to

\big(\sigma[i := \mathrm{enc}(\operatorname{sg}(a,\ |a|\,2^m+b)) \mathbin{+\!\!+} R_i]\big)[k := R_k]

with cost at most $\mathrm{catCost}(m) = 2\,\mathrm{moveCost}(m)+\mathrm{zipCost}(0,m)+23 = O(m)$ . Here $\operatorname{sg}(a,n)$ is $n$ with the sign of $a$ ; for $a>0$ the result is $a\,2^m+b$ . The ruler on $j$ is left in place.

The operation appends the $m$ -bit block $b$ below the bits of $a$ in time linear in $m$ only (independent of the size of $a$ ), which is what makes the Horner recombination of the $M$ -bit output digits linear-time.

Formalization Note. Machine states are St S records: stacks stk : Fin S → List Sym over the 16-letter alphabet Sym = Fin 16 (head = top), input position ip and output out; σ.set i L replaces stack i. An integer item is stored as (Item.int z).enc: a sign header followed by the minimal binary magnitude, least significant bit nearest the header; bitOf detects bit symbols, and the hypotheses bitOf (…).head? = none say that the following stack content does not start with a bit (so item boundaries are recognisable). Runs I prog p σ σ' c means p runs from σ to exactly σ' with some cost $c'\le c$ ; the procedures prog and input I are arbitrary.

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

set_option linter.unusedSimpArgs false
open NLogN
variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}

Formal statement

theorem NLogN.Runs.catR {q i j k t1 t2 : Fin S} (hqi : q ≠ i) (hqj : q ≠ j) (hqk : q ≠ k)
    (hqt1 : q ≠ t1) (hqt2 : q ≠ t2) (hij : i ≠ j) (hik : i ≠ k) (hit1 : i ≠ t1) (hit2 : i ≠ t2)
    (hjk : j ≠ k) (hjt1 : j ≠ t1) (hjt2 : j ≠ t2) (hkt1 : k ≠ t1) (hkt2 : k ≠ t2) (ht12 : t1 ≠ t2)
    (σ : St S) (a : ℤ) (b m : ℕ) (ha : a ≠ 0) (hb : b < 2 ^ m) (Ri Rj Rk : List Sym)
    (hi : σ.stk i = (Item.int a).enc ++ Ri) (hj : σ.stk j = (Item.int ((2 : ℤ) ^ m)).enc ++ Rj)
    (hk : σ.stk k = (Item.int (b : ℤ)).enc ++ Rk)
    (hRi : bitOf Ri.head? = none) (hRk : bitOf Rk.head? = none)
    (ht1 : bitOf (σ.stk t1).head? = none) (ht2 : bitOf (σ.stk t2).head? = none) :
    Runs I prog (NLogN.catR q i j k t1 t2 : Stmt S P) σ
      ((σ.set i ((Item.int (sg a (a.natAbs * 2 ^ m + b))).enc ++ Ri)).set k Rk) (catCost m) := 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.Runs.catR` of the Lean development NLogN/Cat.lean (lines 71–144), written for the prove2.me integer-multiplication campaign.

View graph