Round-six lemma `cAK2_le`

Proved

J6Seg.AC.cAK2_le

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

complexity-theoryinteger-multiplicationkappa-improvement

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

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

theorem J6Seg.AC.cAK2_le {w2 bk win pk b φ1 φ2 B BH J Z : ℕ} (hw2 : w2 ≤ win) (hbk : bk ≤ win)
    (hJ : jA w2 bk ≤ J) (hZ : zsz ((b * (2 * (w2 + bk)) : ℕ) : ℤ) ≤ Z) :
    cAK2 w2 bk win pk b φ1 φ2 B BH ≤
      10 ^ 13 * (win + 1) * (BH + B + b + pk + 10) + 4 * (win + 1) * φ1 + 8000 * φ2 +
        2 * 10 ^ 6 * (J + 1) * (BkA w2 bk b + 2) + 2000 * (b * (2 * (w2 + bk)) + 1) * (Z + 4)

Context. A-axis costs 3: the kernel pass as a natural-number polynomial

kerC_le: kerC Ckn B m post Lmax nc Tot pre N ≤ R·Ckn + 10^5 (B+2) (R (m+1) + pre·nc·(Lmax+2) + pre (Tot+3) + N + 3), R = pre·nc·post;
cAK2_le: the A kernel v2 per row: cAK2 … ≤ 10^13 (win+1) X + 4 (win+1) φ1 + 8000 φ2 + 2·10^6 (J+1)(BkA+2) + 2000 (m+1)(Z+4) with X = BH + B + b + pk + 10, m = b · 2(w2+bk), jA ≤ J, zsz m ≤ Z.

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_Defs68

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg
open IntMul NLogN IntMul.Kappa.R6 J6Seg J6Seg.KR J6Seg.KR.AK

Formal statement

theorem J6Seg.AC.cAK2_le {w2 bk win pk b φ1 φ2 B BH J Z : ℕ} (hw2 : w2 ≤ win) (hbk : bk ≤ win)
    (hJ : jA w2 bk ≤ J) (hZ : zsz ((b * (2 * (w2 + bk)) : ℕ) : ℤ) ≤ Z) :
    cAK2 w2 bk win pk b φ1 φ2 B BH ≤
      10 ^ 13 * (win + 1) * (BH + B + b + pk + 10) + 4 * (win + 1) * φ1 + 8000 * φ2 +
        2 * 10 ^ 6 * (J + 1) * (BkA w2 bk b + 2) + 2000 * (b * (2 * (w2 + bk)) + 1) * (Z + 4) := 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 `J6Seg.AC.cAK2_le`, Solutions/J6SegAKCost3.lean (lines 31–91) of the round-six development.

View graph