Magnitude bounds for all intermediate lists of the HvdH reference step

Proved

NLogN.BD.refStep_LB_mkParams

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

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

Let $K \ge 20$ , $N \ge 2^{2^{8K}+1}$ , $q = \mathrm{mkParams}(K,N)$ and $x, y\in\mathbb N$ . There is an explicit bound $B_q = 2\max(2^p, B_W)\,c_S^K$ with $B_q < 2^P$ and $\mathrm{size}(B_q) \le p + \lfloor p/8\rfloor$ such that every intermediate list of refStep q x y has all (real and imaginary) entries bounded by $B_q$ in absolute value: (a) the CRT digit vectors rU q x, rU q y and their scaled complex versions ecU; (b) every stage of the Gaussian-resampling ( $\tilde S$ ) passes of the three forward transforms (inputs $U$ , $V$ and the pointwise product $W$ ) and every stage of the $\tilde B$ passes; (c) the inputs of the Fermat convolution and the chirp table chirpL q; (d) every convL and FtL output (and every fermatW output is bounded by $2^P$ ); (e) the products $W$ , $Y$ ; (f) the output of exactConvL and the crtOut digits.

Formalization Note. LB L B (resp. LBz) says every pair (resp. integer) in the list has absolute values $\le B$ ; tensorGo (axs.take k) dims is the list after the first $k$ axis passes. All list functions (refStep, fwdL, FtL, convL, fermatW, exactConvL, crtIn/crtOut, tensorGo) are those of the published Def_IntMul_HvdH_MachineRef. These bounds size the registers of the machine implementation.

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 NLogN.BD
open IntMul.HvdH IntMul.HvdH.Ref NLogN.Asym

Formal statement

theorem NLogN.BD.refStep_LB_mkParams (K N : ℕ) (hK : 20 ≤ K) (hN : 2 ^ (2 ^ (8 * K) + 1) ≤ N)
    (x y : ℕ) :
    let q := mkParams K N
    Bq q < 2 ^ q.P ∧ Nat.size (Bq q) ≤ q.p + q.p / 8 ∧
    -- (a)
    LBz (rU q x) (Bq q) ∧ LBz (rU q y) (Bq q) ∧
    LB (ecU q (rU q x)) (Bq q) ∧ LB (ecU q (rU q y)) (Bq q) ∧
    -- (b) the `S̃` stages
    (∀ k, LB (tensorGo ((axS q).take k) q.sdims (ecU q (rU q x))) (Bq q)) ∧
    (∀ k, LB (tensorGo ((axS q).take k) q.sdims (ecU q (rU q y))) (Bq q)) ∧
    (∀ k, LB (tensorGo ((axS q).take k) q.sdims (ecW q (rU q x) (rU q y))) (Bq q)) ∧
    -- (c) the `fermatW` arguments
    LB (ftIn q (ecU q (rU q x))) (Bq q) ∧ LB (ftIn q (ecU q (rU q y))) (Bq q) ∧
    LB (ftIn q (ecW q (rU q x) (rU q y))) (Bq q) ∧ LB (chirpL q) (Bq q) ∧
    -- (d)
    (∀ X Y, LB (fermatW q X Y) (2 ^ q.P)) ∧ (∀ X Y, LB (convL q X Y) (Bq q)) ∧
    (∀ X, LB (FtL q X) (Bq q)) ∧
    -- (b) the `B̃` stages
    (∀ X k, LB (tensorGo ((axB q).take k) q.tdims (FtL q X)) (Bq q)) ∧
    (∀ X, LB (fwdL q X) (Bq q)) ∧
    -- (e)
    LB (ecW q (rU q x) (rU q y)) (Bq q) ∧ LB (ecY q (rU q x) (rU q y)) (Bq q) ∧
    -- (f)
    LBz (exactConvL q (rU q x) (rU q y)) (Bq q) ∧
    LBz (crtOut q.s (2 * q.L - 1) (exactConvL q (rU q x) (rU q y))) (Bq q) := 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.BD.refStep_LB_mkParams` of the Lean development NLogN/HBd3.lean (lines 361–460), written for the prove2.me integer-multiplication campaign.

View graph