The kernel loop (round six, `kerQ`)

Proved

IntMul.Kappa.R6.IL3H.kerQ

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

complexity-theoryinteger-multiplicationkappa-improvement

The kernel loop.

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

theorem IntMul.Kappa.R6.IL3H.kerQ {c : IntMul.Kappa.R6.IL3H.Cfg} (hc : CfgOK c) (jK jL : Fin Pp) (rowC : IStmt HS Pp)
    (hK : tbl jK = kerLoopC jK jL) (hL : tbl jL = levCH c jL rowC)
    {K S r H P D ρ q0 Bp Z Zr G b : ℕ} {CB : ℕ → ℝ}
    (L1 : LvH c Isym tbl jL rowC K r Z Zr H G CB 1) (hρ : ρ < K) (hS : 1 ≤ S) (hP : 1 ≤ P)
    (hb : b ≤ D) (hZ16 : zsz ((16 * (c.Wr * (P * 2 ^ (K * D) * S * r)) : ℕ) : ℤ) ≤ Z)
    (hV : zsz ((VbH c K (K * D) S r H 1 (ρ + K * (D - 1)) P : ℕ) : ℤ) ≤ Zr) (hH1 : 1 ≤ H)
    (Mb Bz : ℕ) (hMb : zsz (Mb : ℤ) ≤ Bz) (hM : K * D + P + D + S + 2 ≤ Mb) :
    ∀ (d i : ℕ) (σ : Fin HS → Option ℤ), CoreR σ K S r H P D ρ 0 q0 Bp → σ vG = some (G : ℤ) →
      σ 11 = some (i : ℤ) → σ 12 = some (b : ℤ) → i + d = b →
      SImplQ Isym tbl (fun s => Agree σ s) 0 H r (fun x : Fin D => KFH.stT K D S ρ x)
        (P * 2 ^ (K * D) * S)
        (tensF fun x : Fin D => if i ≤ x.val ∧ x.val < b then Cm else 1) (.call jK) d
        ((c.Wr + 4) * d)
        (fun _ => d * (⌊CB 1 * ((nN P (K * D) S * Yu r Zr H : ℕ) : ℝ)⌋₊ + cKO Bz) + cKE Bz)

Context. Round six, item language (I3): the kernel loop of the uniform Proposition 14

kerLoopC jK jL (at index jK): with i on 11 and b on 12, while i < b, the level procedure jL on the single bit i of the layer (a level frame kerTF: E = 1 bit at e = ρ + K (D - 1 - i), t = K D, B = P), then i ↦ i + 1.

levRH_of6: a six-register level frame on a BaseR state with K, r, H is a LevRH.
kerQ: kerLoopC implements the kernels C on the bits i ≤ x < b of the layer.

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_Defs22

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.IL3H
open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW Complex P8Lift Butterfly IntMul.Kappa.R6.Cx
variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp}

Formal statement

theorem IntMul.Kappa.R6.IL3H.kerQ {c : IntMul.Kappa.R6.IL3H.Cfg} (hc : CfgOK c) (jK jL : Fin Pp) (rowC : IStmt HS Pp)
    (hK : tbl jK = kerLoopC jK jL) (hL : tbl jL = levCH c jL rowC)
    {K S r H P D ρ q0 Bp Z Zr G b : ℕ} {CB : ℕ → ℝ}
    (L1 : LvH c Isym tbl jL rowC K r Z Zr H G CB 1) (hρ : ρ < K) (hS : 1 ≤ S) (hP : 1 ≤ P)
    (hb : b ≤ D) (hZ16 : zsz ((16 * (c.Wr * (P * 2 ^ (K * D) * S * r)) : ℕ) : ℤ) ≤ Z)
    (hV : zsz ((VbH c K (K * D) S r H 1 (ρ + K * (D - 1)) P : ℕ) : ℤ) ≤ Zr) (hH1 : 1 ≤ H)
    (Mb Bz : ℕ) (hMb : zsz (Mb : ℤ) ≤ Bz) (hM : K * D + P + D + S + 2 ≤ Mb) :
    ∀ (d i : ℕ) (σ : Fin HS → Option ℤ), CoreR σ K S r H P D ρ 0 q0 Bp → σ vG = some (G : ℤ) →
      σ 11 = some (i : ℤ) → σ 12 = some (b : ℤ) → i + d = b →
      SImplQ Isym tbl (fun s => Agree σ s) 0 H r (fun x : Fin D => KFH.stT K D S ρ x)
        (P * 2 ^ (K * D) * S)
        (tensF fun x : Fin D => if i ≤ x.val ∧ x.val < b then Cm else 1) (.call jK) d
        ((c.Wr + 4) * d)
        (fun _ => d * (⌊CB 1 * ((nN P (K * D) S * Yu r Zr H : ℕ) : ℝ)⌋₊ + cKO Bz) + cKE Bz) := 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.IL3H.kerQ`, Solutions/R6IL3Top2.lean (lines 72–243) of the round-six development.

View graph