Cost bound for the radix sort of tagged rows

Proved

NLogN.sortW_cost

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

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

Let $R$ be a list of rows of width $w \ge 1$ (integers of bit length $\le B$ ) stored flattened on stack 0, with stack 54 holding $|R|$ and stack 3 holding $kb$ , where $kb+2\le B$ and $\mathrm{zsz}(|R|w), \mathrm{zsz}(w)\le B$ . Then the sorting program sortW w (a $kb$ -pass binary radix sort on the first entry of each row) costs at most $2\cdot10^5(kb+1)(|R|w+1)(B+2) + 9000(B+2)$ .

Formalization Note. 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

Formal statement

theorem NLogN.sortW_cost (w kb : ℕ) (t : IState HS) (R : List (List ℤ)) (Rest : List Item)
    (hR : ∀ r ∈ R, r.length = w) (hw : 1 ≤ w) (L54 L3 : List Item)
    (h0 : t.G 0 = ints R.flatten ++ Rest) (h54 : t.G 54 = .int R.length :: L54)
    (h3 : t.G 3 = .int kb :: L3)
    (B : ℕ) (hBe : ∀ r ∈ R, Bnd B r) (hBN : zsz ((R.length * w : ℕ) : ℤ) ≤ B)
    (hBk : kb + 2 ≤ B) (hBw : zsz (w : ℤ) ≤ B) :
    (sortW w).cost t ≤ 200000 * (kb + 1) * (R.length * w + 1) * (B + 2) + 9000 * (B + 2) := 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.sortW_cost` of the Lean development NLogN/HTrans.lean (lines 1102–1137), written for the prove2.me integer-multiplication campaign.

View graph