Cost bound for the stack-machine transposition program

Proved

NLogN.transP_cost

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

harvey-van-der-hoeven-tminteger-multiplicationturing-machines

Let $D$ be a list of $n\cdot m$ rows, each of $d$ integers bounded by $B$ in bit length, stored flattened on stack 0, with $nm\le 2^{kb}$ , $m\ge1$ , and stacks 1,2,3 holding $n$ , $m$ , $kb$ . Then the transposition program transP d costs at most $10^6(kb+1)(nm+1)(d+1)(B+kb+d+4)$ .

Formalization Note. Bnd B r says every entry of $r$ has bit length $\le B$ . The machine layer: IState HS is a state with $64$ stacks of items (Item = integer or mark), an input position and an output; RM programs (straight-line register code RS, loops rep, conditionals, calls of the multiplication procedure through a MulSpec $M$ giving its domain and cost) have a functional semantics p.run s, a definedness predicate p.ok M s and a cost p.cost M s; Spec M p s s' c abbreviates p.ok M s ∧ p.run s = s' ∧ p.cost M s ≤ c. ints L / gints U push an integer list / a list of pairs as items (head = top); zsz z is the bit length of $|z|$ . MulBnd M m Φ says the multiplication procedure accepts all pairs of integers of bit length $\le m$ at cost $\le Φ$ . Register names (GU, CR, KB, XN, …) are fixed stack indices.

Preamble

-- Harvey–van der Hoeven multitape-TM development (NLogN), generated by skeleton subtraction.

import Definitions.Def_IntMul_HvdH_M_Defs4

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

set_option linter.unusedSimpArgs false
open NLogN
open IntMul RS
set_option maxHeartbeats 1000000

Formal statement

theorem NLogN.transP_cost (d n m kb B : ℕ) (D : List (List ℤ)) (Rest : List Item) (s : IState HS)
    (hD : D.length = n * m) (hDw : ∀ r ∈ D, r.length = d) (hN : n * m ≤ 2 ^ kb) (hm : 1 ≤ m)
    (L1 L2 L3 : List Item) (h0 : s.G 0 = ints D.flatten ++ Rest) (h1 : s.G 1 = .int n :: L1)
    (h2 : s.G 2 = .int m :: L2) (h3 : s.G 3 = .int kb :: L3) (hDB : ∀ r ∈ D, Bnd B r) :
    (transP d).cost s ≤ 10 ^ 6 * (kb + 1) * (n * m + 1) * (d + 1) * (B + kb + d + 4) := by sorry

Source

D. Harvey, J. van der Hoeven, Integer multiplication in time O(n log n), Ann. of Math. 193 (2021), 563–617 (Theorem 1.1: multitape Turing machine multiplication in O(n log n)). Lemma `NLogN.transP_cost` of the Lean development NLogN/HTrans.lean (lines 1143–1249), written for the prove2.me integer-multiplication campaign.

View graph