Row-by-row bound (round six, `Ncost6R_le`)

Proved

IntMul.Kappa.R6.Ncost6R_le

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

complexity-theoryinteger-multiplicationkappa-improvement

Row-by-row bound.

The following holds (Lean statement, in the scope of module Solutions.R6Params):

theorem IntMul.Kappa.R6.Ncost6R_le (P : Prm) (hP : P.Ok) (B p d ℓ : ℝ) (hB : 1 ≤ B) (hp1 : 1 ≤ p)
    (hp : p ≤ 6 * B ^ ((1 : ℝ) + P.x)) (hd1 : B ^ P.ε / 2 ≤ d) (hd2 : d ≤ B ^ P.ε)
    (hℓ0 : 0 ≤ ℓ) (hℓ : ℓ ≤ 4 * B ^ (1 - P.ε)) :
    Ncost6R P p d ℓ ≤ Cst P * B ^ (1 - P.gap) * (Real.log B + 1)

Context. Round six: the parameter map n ↦ (b, b', p, L, T, d, ℓ, r, K, α², V) and the cost Ncost6

Stack parameters (Colkitt/Jain, stack-notes.tex §1 Idea D, Idea C):

b = lg n (bP6), b' = b^(1+x) (b'P6; x : ℕ so ⌈b^(1+x)⌉ = b^(1+x)), p = 6 b' (pP6);
L (LP6) = least L with 4n ≤ 2^L b', T = 2^L (TP6), so 4n ≤ T b' < 8n;
d = ⌊b^ε⌋ (dP6), ℓ = ⌈L/d⌉ = (L + d - 1)/d (ℓP6), r = 2^ℓ (rP6), K = ℓ - 1 (KP6, one chunk per axis);
α² = ⌊p/(48d)⌋ = ⌊b'/(8d)⌋ (α2P6, a natural number), α = √(α²) (αP6), γ = 2 d α² (γP6);
bit volume V = T p (VP6), with 24 n ≤ V ≤ 48 n.

Normalization (same as OpenAI's RCost.Ncost) Ncost6 is the per-bit cost: the Table-1 cost divided by V = T p. The machine time is C₀ (V · Ncost6 · polylog + n); since V ≤ 48 n, a bound Ncost6 ≤ C b^(1-gap) polylog gives time O(n lg^(1-gap) polylog).

Ncost6 P n = d + ℓ d^λ' + d p^δ + (ℓ + log₂ p) + p^δ + ℓ (d ln p)^τ + 1 (rows: prefix moves 1-ε; butterflies ε(1-λ'); fine exposures/Gaussian/chirps/reserved axes 1-ε-poly; pointwise products ε; precision p^δ = b^poly; CRT reversal ε(1-τ) = max(ε,1-ε)(1-τ) as ε ≥ 1/2). Note ℓ ≈ b^(1-ε) and p^δ ≤ 6 b^poly.

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.Ncost6R_le (P : Prm) (hP : P.Ok) (B p d ℓ : ℝ) (hB : 1 ≤ B) (hp1 : 1 ≤ p)
    (hp : p ≤ 6 * B ^ ((1 : ℝ) + P.x)) (hd1 : B ^ P.ε / 2 ≤ d) (hd2 : d ≤ B ^ P.ε)
    (hℓ0 : 0 ≤ ℓ) (hℓ : ℓ ≤ 4 * B ^ (1 - P.ε)) :
    Ncost6R P p d ℓ ≤ Cst P * B ^ (1 - P.gap) * (Real.log B + 1) := 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.Ncost6R_le`, Solutions/R6Params.lean (lines 342–435) of the round-six development.

View graph