Round six: the per-bit cost is O(lg^{1-gap} polylog)

Proved

IntMul.Kappa.R6.Ncost6_le

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

complexity-theoryinteger-multiplicationkappa-improvement

Let $P$ satisfy Prm.Ok. The round-six per-bit cost is

N(P,n) = d + \ell d^{\lambda'} + d p^{\delta} + (\ell + \log_2 p) + p^{\delta} + \ell (d \ln p)^{\tau} + 1

with the parameter map of params6_ok. Then there are constants $C \ge 0$ , $A \in \mathbb N$ and $n_1$ such that for all $n \ge n_1$

N(P, n) \le C\, (\lg n)^{1 - \mathrm{gap}(P)}\, (\log \lg n + 1)^{A}.

Combined with $V \le 48n$ this yields running time $O(n \lg^{1-\mathrm{gap}} n\,\mathrm{polylog})$ for a machine whose time per bit is bounded by $N$ .

In Lean:

theorem IntMul.Kappa.R6.Ncost6_le (P : Prm) (hP : P.Ok) : ∃ (C : ℝ) (A : ℕ) (n₁ : ℕ), 0 ≤ C ∧ ∀ n, n₁ ≤ n →
    Ncost6 P n ≤ C * (IntMul.lg n : ℝ) ^ (1 - P.gap) * (Real.log (IntMul.lg n) + 1) ^ A

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).

Preamble

-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_R6_Defs1

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6
open Real

Formal statement

theorem IntMul.Kappa.R6.Ncost6_le (P : Prm) (hP : P.Ok) : ∃ (C : ℝ) (A : ℕ) (n₁ : ℕ), 0 ≤ C ∧ ∀ n, n₁ ≤ n →
    Ncost6 P n ≤ C * (IntMul.lg n : ℝ) ^ (1 - P.gap) * (Real.log (IntMul.lg n) + 1) ^ A := by sorry

Source

S. Jain, round-six networks for the integer-multiplication κ-improvement campaign (https://github.com/Swapnil-jain/integer-mult-kappa, commit 5868dc7) and D. Colkitt, integer-mult-bounds (https://github.com/CrocSwap/integer-mult-bounds); target `IntMul.Kappa.jain_round6_framework`. Lean declaration `IntMul.Kappa.R6.Ncost6_le`, Solutions/R6Params.lean (lines 448–453) of the round-six development.

View graph