Round-six lemma `l13U_arith`

Proved

NLogN.KFX.l13U_arith

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.KFX4Core):

theorem NLogN.KFX.l13U_arith {c n w M R Lτ X δ Ks Ksw Kcr cto cfr core : ℝ} (hn1 : 1 ≤ n) (hw : 0 ≤ w)
    (hM1 : 1 ≤ M) (hR : 0 ≤ R) (hLτ : 0 ≤ Lτ) (hX1 : 1 ≤ X) (hδ : 0 ≤ δ) (hKs : 0 ≤ Ks)
    (hKsw : 0 ≤ Ksw) (hKcr : 0 ≤ Kcr)
    (hc : c ≤ 2000 * cto + 4 * (26 + Ksw * (2 * n * (w + 1) + 1) * Lτ) +
      (400 * core + 10 ^ 10 * (X + 4) ^ 2) + 2000 * cfr)
    (hcore : core ≤ 1 + 16 * Ks * (2 * n * (w + 1) + 1) * Lτ +
      2 * 10 ^ 15 * (M * X ^ 3 + 2 * n * (w + 1)) +
      Kcr * (M * X ^ 3 + 2 * n * (w + 1) + δ * M * X * (2 * R * (w + 1) + X)))
    (hcto : cto ≤ 3 * 10 ^ 4 * (n * (w + 1))) (hcfr : cfr ≤ 3 * 10 ^ 4 * (n * (w + 1))) :
    c ≤ (10 ^ 19 + 12 * Ksw + 19200 * Ks + 2000 * Kcr) *
      (n * (w + 1) * (Lτ + 1) + M * X ^ 3 + δ * M * X * (R * (w + 1) + X))

Context. KFX §4: the register-driven Lemma 13 core

The fixed code l13U q is KFL.l13code with every size-dependent literal read from the master registers (MReg): w, 2·M·R on 1, 6 (for toBitsU/fromBitsU), the swap flags on 11, 12, and Q = 2^{fK}, B = R·2(w+1), 2^ρ, gx, N0, N1, N2, N3, A = zsz V, 2^K on 13, 15, 16, 17, 18, 19, 46, 47, 48, 49, f, K on 36, 37. The slot swaps preL px py are realized by two optional swaps (optA: swap 0 or 2 by the flag on 11, optB: swap 1 by the flag on 12). l13U_runs is KFL.l13_runs for this code.

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_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN NLogN.KFX
open IntMul NLogN.RS NLogN.KIL NLogN.KFD NLogN.KFE NLogN.KFB NLogN.KFL NLogN.KFW NLogN.KFH AModel Butterfly

Formal statement

theorem NLogN.KFX.l13U_arith {c n w M R Lτ X δ Ks Ksw Kcr cto cfr core : ℝ} (hn1 : 1 ≤ n) (hw : 0 ≤ w)
    (hM1 : 1 ≤ M) (hR : 0 ≤ R) (hLτ : 0 ≤ Lτ) (hX1 : 1 ≤ X) (hδ : 0 ≤ δ) (hKs : 0 ≤ Ks)
    (hKsw : 0 ≤ Ksw) (hKcr : 0 ≤ Kcr)
    (hc : c ≤ 2000 * cto + 4 * (26 + Ksw * (2 * n * (w + 1) + 1) * Lτ) +
      (400 * core + 10 ^ 10 * (X + 4) ^ 2) + 2000 * cfr)
    (hcore : core ≤ 1 + 16 * Ks * (2 * n * (w + 1) + 1) * Lτ +
      2 * 10 ^ 15 * (M * X ^ 3 + 2 * n * (w + 1)) +
      Kcr * (M * X ^ 3 + 2 * n * (w + 1) + δ * M * X * (2 * R * (w + 1) + X)))
    (hcto : cto ≤ 3 * 10 ^ 4 * (n * (w + 1))) (hcfr : cfr ≤ 3 * 10 ^ 4 * (n * (w + 1))) :
    c ≤ (10 ^ 19 + 12 * Ksw + 19200 * Ks + 2000 * Kcr) *
      (n * (w + 1) * (Lτ + 1) + M * X ^ 3 + δ * M * X * (R * (w + 1) + X)) := 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 `NLogN.KFX.l13U_arith`, Solutions/KFX4Core.lean (lines 918–984) of the round-six development.

View graph