One block in IL (round six, `blkI2_runs`)

Proved

J6Seg.KR.blkI2_runs

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

complexity-theoryinteger-multiplicationkappa-improvement

One block in IL.

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

theorem J6Seg.KR.blkI2_runs {M : MulSpec} {pM : Fin Pp} (hM : MulOK I iprog pM M) (hdom : ∀ x y, M.dom x y)
    {b n pk φD φT B BH : ℕ} (hΦD : ∀ x y : ℤ, zsz x ≤ B → zsz y ≤ B → M.Φ x y ≤ φD)
    (hΦT : ∀ x y : ℤ, zsz x ≤ b * (2 * n) + 2 → zsz y ≤ b * (2 * n) + 2 → M.Φ x y ≤ φT)
    (hb : 1 ≤ b) (hn1 : 1 ≤ n) (hbig : 2 * (2 * n) * 2 ^ (2 * pk) < 2 ^ (b - 1))
    (P : ℕ) (s : IState HS) (G : Fin HS → List ℤ) (hG : GOK P pk b G)
    (am ap : List ℤ) (z : List GI) (r0 o dt du : List ℤ) (c : ℕ)
    (hz : z.length = n) (ham : am.length = n) (hap : ap.length = n)
    (hdi : n ≤ (G TDI).length) (hgi : n ≤ (G TGI).length) (hga : n ≤ (G TGA).length)
    (hdd : n ≤ (G TDD).length)
    (hok : blkOK P (2 ^ pk) (2 * n) (G TDI) (G TGI) (G TGA) (G TDD) am ap z)
    (tdi : TB (2 ^ pk) (G TDI)) (tgi : TB (2 ^ pk) (G TGI)) (tga : TB (2 ^ pk) (G TGA))
    (tdd : TB (2 ^ pk) (G TDD)) (tam : TB (2 ^ pk) am) (tap : TB (2 ^ pk) ap)
    (hBb : b + 4 ≤ B) (hBp : 2 * pk + 4 ≤ B) (hPB : P + 3 ≤ B)
    (hBn : zsz ((2 * n : ℕ) : ℤ) ≤ B)
    (hBH : ∀ v ∈ blkHdr2 n b, zsz v ≤ BH) (hBc : zsz ((c + 1 : ℕ) : ℤ) ≤ BH) :
    IRuns I iprog (blkI2 pM)
      (encK s (BF G (gflat z ++ r0) [] [] o (blkHdr2 n b ++ (am ++ (ap ++ dt))) du [] [] [] [] []
        [((c + 1 : ℕ) : ℤ)]))
      (encK s (BF G r0 [] [] (gflat (blkG P (2 * n) (G TDI) (G TGI) (G TGA) (G TDD) am ap z).reverse
        ++ o) dt ((blkHdr2 n b ++ am ++ ap).reverse ++ du) [] [] [] [] [] [(c : ℤ)]))
      (cBlk2 n pk b φD φT B BH)

Context. B3′, part 3: one block in IL with in-kernel constants

blkI2 pM is blkI pM with the header hdrRS2 (reads blkHdr2 n b, computes the constants). blkI2_runs: as blkI_runs, with blkHdr2 and the cost cBlk2.

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.blkI2_runs {M : MulSpec} {pM : Fin Pp} (hM : MulOK I iprog pM M) (hdom : ∀ x y, M.dom x y)
    {b n pk φD φT B BH : ℕ} (hΦD : ∀ x y : ℤ, zsz x ≤ B → zsz y ≤ B → M.Φ x y ≤ φD)
    (hΦT : ∀ x y : ℤ, zsz x ≤ b * (2 * n) + 2 → zsz y ≤ b * (2 * n) + 2 → M.Φ x y ≤ φT)
    (hb : 1 ≤ b) (hn1 : 1 ≤ n) (hbig : 2 * (2 * n) * 2 ^ (2 * pk) < 2 ^ (b - 1))
    (P : ℕ) (s : IState HS) (G : Fin HS → List ℤ) (hG : GOK P pk b G)
    (am ap : List ℤ) (z : List GI) (r0 o dt du : List ℤ) (c : ℕ)
    (hz : z.length = n) (ham : am.length = n) (hap : ap.length = n)
    (hdi : n ≤ (G TDI).length) (hgi : n ≤ (G TGI).length) (hga : n ≤ (G TGA).length)
    (hdd : n ≤ (G TDD).length)
    (hok : blkOK P (2 ^ pk) (2 * n) (G TDI) (G TGI) (G TGA) (G TDD) am ap z)
    (tdi : TB (2 ^ pk) (G TDI)) (tgi : TB (2 ^ pk) (G TGI)) (tga : TB (2 ^ pk) (G TGA))
    (tdd : TB (2 ^ pk) (G TDD)) (tam : TB (2 ^ pk) am) (tap : TB (2 ^ pk) ap)
    (hBb : b + 4 ≤ B) (hBp : 2 * pk + 4 ≤ B) (hPB : P + 3 ≤ B)
    (hBn : zsz ((2 * n : ℕ) : ℤ) ≤ B)
    (hBH : ∀ v ∈ blkHdr2 n b, zsz v ≤ BH) (hBc : zsz ((c + 1 : ℕ) : ℤ) ≤ BH) :
    IRuns I iprog (blkI2 pM)
      (encK s (BF G (gflat z ++ r0) [] [] o (blkHdr2 n b ++ (am ++ (ap ++ dt))) du [] [] [] [] []
        [((c + 1 : ℕ) : ℤ)]))
      (encK s (BF G r0 [] [] (gflat (blkG P (2 * n) (G TDI) (G TGI) (G TGA) (G TDD) am ap z).reverse
        ++ o) dt ((blkHdr2 n b ++ am ++ ap).reverse ++ du) [] [] [] [] [] [(c : ℤ)]))
      (cBlk2 n pk b φD φT B BH) := 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.blkI2_runs`, Solutions/J6SegKs3.lean (lines 40–150) of the round-six development.

View graph