Slab passes on representations (round six, `LRep_slabPass`)

Proved

J6Seg.LRep_slabPass

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

complexity-theoryinteger-multiplicationkappa-improvement

Slab passes on representations.

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

theorem J6Seg.LRep_slabPass {pre n n' post : ℕ} (hn : 0 < n) (hp : 0 < post) {L : List α}
    {φ : ℕ → ℕ → List α} (hL : LRep pre n post L φ) (src : ℕ → Option ℕ) (h : ℕ → α → β)
    (hsrc : ∀ l < n', ∀ k, src l = some k → k < n) :
    LRep pre n' post (slabPass n n' post src h L) (fun b c => slabLine n' src h (φ b c))

Context. B-line machine, sweep 2: the per-axis passes on line representations

A (pre, n, post) array L represents the lines φ b c (LRep pre n post L φ) when L[b (n·post) + a·post + c] = (φ b c)[a]. The machine's passes act on representations:

LRep_axisL: the in-place axis map applies f to every line;
LRep_slabPass: a monotone slab pass (output slab l = h l of input slab src l, or zeros) applies slabLine to every line (selection, J gather and scatter, output);
LRep_kerPass: expose (A, m, post) → (A, post, m) (blkTg), apply a kernel to each contiguous m-row (indexed by its block), expose back;
LRep_split / LRep_join: (pre, nc·λ, post) is (pre·nc, λ, post);
LRep_chunkPass: the chunk kernel chunksG g λ nc on every line, by one λ-exposure.

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_Defs62

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg
open IntMul.HvdH IntMul.HvdH.Ref NLogN.KFM NLogN.KFY
variable {α β : Type*} [Inhabited α] [Inhabited β]

Formal statement

theorem J6Seg.LRep_slabPass {pre n n' post : ℕ} (hn : 0 < n) (hp : 0 < post) {L : List α}
    {φ : ℕ → ℕ → List α} (hL : LRep pre n post L φ) (src : ℕ → Option ℕ) (h : ℕ → α → β)
    (hsrc : ∀ l < n', ∀ k, src l = some k → k < n) :
    LRep pre n' post (slabPass n n' post src h L) (fun b c => slabLine n' src h (φ b c)) := 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.LRep_slabPass`, Solutions/J6SegSw2.lean (lines 132–195) of the round-six development.

View graph