The chunk kernel in IL (round six, `chunkI2_runs`)

Proved

J6Seg.KR.chunkI2_runs

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

complexity-theoryinteger-multiplicationkappa-improvement

The chunk kernel in IL.

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

theorem J6Seg.KR.chunkI2_runs {M : MulSpec} {pM : Fin Pp} (hM : MulOK I iprog pM M) (hdom : ∀ x y, M.dom x y)
    {b pk φD B BH : ℕ} {φT : ℕ → ℕ} (hΦD : ∀ x y : ℤ, zsz x ≤ B → zsz y ≤ B → M.Φ x y ≤ φD)
    (hΦT : ∀ n, ∀ x y : ℤ, zsz x ≤ b * (2 * n) + 2 → zsz y ≤ b * (2 * n) + 2 → M.Φ x y ≤ φT n)
    (hb : 1 ≤ b) (P lam : ℕ) (hlam : 1 ≤ lam) (s : IState HS) (di gi gam dd : List ℤ)
    (ds : List (ℕ × List ℤ × List ℤ)) (x : List GI) (l : List ℤ)
    (hx : x.length = lam) (hdi : di.length = lam) (hgi : gi.length = lam) (hga : gam.length = lam)
    (hdd : dd.length = lam)
    (hds : ∀ d ∈ ds, 1 ≤ d.1 ∧ d.2.1.length = d.1 ∧ d.2.2.length = d.1 ∧ d.1 ≤ lam ∧
        d.1 ≤ lam ∧ d.1 ≤ lam ∧ d.1 ≤ lam ∧ TB (2 ^ pk) d.2.1 ∧
        TB (2 ^ pk) d.2.2 ∧ 2 * (2 * d.1) * 2 ^ (2 * pk) < 2 ^ (b - 1) ∧
        zsz ((2 * d.1 : ℕ) : ℤ) ≤ B ∧ (∀ v ∈ blkHdr2 d.1 b, zsz v ≤ BH))
    (hsum : J6Seg.KR.sumN ds ≤ lam) (hok : chunkOK P (2 ^ pk) di gi gam dd ds x) (hxb : AB (2 ^ pk) x)
    (tdi : TB (2 ^ pk) di) (tgi : TB (2 ^ pk) gi) (tga : TB (2 ^ pk) gam) (tdd : TB (2 ^ pk) dd)
    (hBb : b + 4 ≤ B) (hBp : 2 * pk + 4 ≤ B) (hPB : P + 3 ≤ B) (hlB : zsz ((2 * lam : ℕ) : ℤ) ≤ B)
    (hBBH : B ≤ BH) (hBH : ∀ v ∈ tabK2 P pk b lam di gi gam dd ds, zsz v ≤ BH) :
    IRuns I iprog (chunkI2 pM)
      (encK s (BF (KF [] [] [] [] [] [] [] [] [] [] [] []) (gflat x ++ l) [] [] []
        (tabK2 P pk b lam di gi gam dd ds) [] [] [] [] [] [] []))
      (encK s (BF (KF [] [] [] [] [] [] [] [] [] [] [] []) (gflat (chunkG2 P di gi gam dd ds x) ++ l)
        [] [] [] (tabK2 P pk b lam di gi gam dd ds) [] [] [] [] [] [] []))
      (cKer2 pk b lam φD φT B BH ds)

Context. B3′, part 5: the chunk kernel with in-kernel constants

chunkI2 pM (hdrK, the block loop of blkI2, finK) on the table tabK2 … (J6SegKs0). chunkI2_runs is chunkI_runs for the new layout; the cost cKer2 uses cLoop2.

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_Defs66

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.KR
open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFV
variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

Formal statement

theorem J6Seg.KR.chunkI2_runs {M : MulSpec} {pM : Fin Pp} (hM : MulOK I iprog pM M) (hdom : ∀ x y, M.dom x y)
    {b pk φD B BH : ℕ} {φT : ℕ → ℕ} (hΦD : ∀ x y : ℤ, zsz x ≤ B → zsz y ≤ B → M.Φ x y ≤ φD)
    (hΦT : ∀ n, ∀ x y : ℤ, zsz x ≤ b * (2 * n) + 2 → zsz y ≤ b * (2 * n) + 2 → M.Φ x y ≤ φT n)
    (hb : 1 ≤ b) (P lam : ℕ) (hlam : 1 ≤ lam) (s : IState HS) (di gi gam dd : List ℤ)
    (ds : List (ℕ × List ℤ × List ℤ)) (x : List GI) (l : List ℤ)
    (hx : x.length = lam) (hdi : di.length = lam) (hgi : gi.length = lam) (hga : gam.length = lam)
    (hdd : dd.length = lam)
    (hds : ∀ d ∈ ds, 1 ≤ d.1 ∧ d.2.1.length = d.1 ∧ d.2.2.length = d.1 ∧ d.1 ≤ lam ∧
        d.1 ≤ lam ∧ d.1 ≤ lam ∧ d.1 ≤ lam ∧ TB (2 ^ pk) d.2.1 ∧
        TB (2 ^ pk) d.2.2 ∧ 2 * (2 * d.1) * 2 ^ (2 * pk) < 2 ^ (b - 1) ∧
        zsz ((2 * d.1 : ℕ) : ℤ) ≤ B ∧ (∀ v ∈ blkHdr2 d.1 b, zsz v ≤ BH))
    (hsum : J6Seg.KR.sumN ds ≤ lam) (hok : chunkOK P (2 ^ pk) di gi gam dd ds x) (hxb : AB (2 ^ pk) x)
    (tdi : TB (2 ^ pk) di) (tgi : TB (2 ^ pk) gi) (tga : TB (2 ^ pk) gam) (tdd : TB (2 ^ pk) dd)
    (hBb : b + 4 ≤ B) (hBp : 2 * pk + 4 ≤ B) (hPB : P + 3 ≤ B) (hlB : zsz ((2 * lam : ℕ) : ℤ) ≤ B)
    (hBBH : B ≤ BH) (hBH : ∀ v ∈ tabK2 P pk b lam di gi gam dd ds, zsz v ≤ BH) :
    IRuns I iprog (chunkI2 pM)
      (encK s (BF (KF [] [] [] [] [] [] [] [] [] [] [] []) (gflat x ++ l) [] [] []
        (tabK2 P pk b lam di gi gam dd ds) [] [] [] [] [] [] []))
      (encK s (BF (KF [] [] [] [] [] [] [] [] [] [] [] []) (gflat (chunkG2 P di gi gam dd ds x) ++ l)
        [] [] [] (tabK2 P pk b lam di gi gam dd ds) [] [] [] [] [] [] []))
      (cKer2 pk b lam φD φT B BH ds) := 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.KR.chunkI2_runs`, Solutions/J6SegKs5.lean (lines 43–265) of the round-six development.

View graph