Clear the block and table stacks (round six, `jK`)

Proved

J6Seg.PJ.Rn.jK

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

complexity-theoryinteger-multiplicationkappa-improvement

Clear the block and table stacks.

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

theorem J6Seg.PJ.Rn.jK {Q R W N s t lam w α : ℕ} {v : Vr} {c : Cs} (hN : N ≤ 2 ^ W) (hv : BV W v)
    (h22 : v 22 = s) (h24 : v 24 = lam) (hs : 0 < s) (hws : w ≤ s) (hsW : s ≤ 2 ^ W)
    (hlW : lam ≤ 2 ^ W)
    (h32 : c 32 = Src.STL s t lam) (h33 : c 33 = Src.LNL s t lam)
    (hDI : c SDI = (diL Q R s t lam α).reverse) (hDD : c SDD = (ddL Q R s t lam α).reverse)
    (hGM : c SGM = (gamL Q R s t lam α).reverse) (hGI : c SGI = (giL Q R s t lam α).reverse)
    (h50 : c 50 = [])
    (bgm : ∀ i < lam, |(mkTables Q R s t α).gam i| ≤ 2 ^ W)
    (bgi : ∀ i < lam, |(mkTables Q R s t α).gi i| ≤ 2 ^ W)
    (bdd : ∀ i < lam, |(mkTables Q R s t α).dd i| ≤ 2 ^ W)
    (bdi : ∀ i < lam, |(mkTables Q R s t α).di i| ≤ 2 ^ W) :
    Rn J6Seg.PJ.jK v c (fun v' => Fxk [11] v v' ∧ BV W v')
      (update (update (update (update (update (update c 32 []) 33 []) SDI []) SDD []) SGM []) SGI [])
      (cJK W N s lam)

Context. B5 J side, part K19: clearing the work stacks

Rn.clr1: pop a whole stack (length in 11, counter 50). jK clears the block stacks 32, 33 (length s from 22) and the table stacks SDI … SGI (length λ from 24) after stage 2 (Rn.jK).

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_Defs71

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.PJ
open IntMul NLogN NLogN.KIL NLogN.RS Function

Formal statement

theorem J6Seg.PJ.Rn.jK {Q R W N s t lam w α : ℕ} {v : Vr} {c : Cs} (hN : N ≤ 2 ^ W) (hv : BV W v)
    (h22 : v 22 = s) (h24 : v 24 = lam) (hs : 0 < s) (hws : w ≤ s) (hsW : s ≤ 2 ^ W)
    (hlW : lam ≤ 2 ^ W)
    (h32 : c 32 = Src.STL s t lam) (h33 : c 33 = Src.LNL s t lam)
    (hDI : c SDI = (diL Q R s t lam α).reverse) (hDD : c SDD = (ddL Q R s t lam α).reverse)
    (hGM : c SGM = (gamL Q R s t lam α).reverse) (hGI : c SGI = (giL Q R s t lam α).reverse)
    (h50 : c 50 = [])
    (bgm : ∀ i < lam, |(mkTables Q R s t α).gam i| ≤ 2 ^ W)
    (bgi : ∀ i < lam, |(mkTables Q R s t α).gi i| ≤ 2 ^ W)
    (bdd : ∀ i < lam, |(mkTables Q R s t α).dd i| ≤ 2 ^ W)
    (bdi : ∀ i < lam, |(mkTables Q R s t α).di i| ≤ 2 ^ W) :
    Rn J6Seg.PJ.jK v c (fun v' => Fxk [11] v v' ∧ BV W v')
      (update (update (update (update (update (update c 32 []) 33 []) SDI []) SDD []) SGM []) SGI [])
      (cJK W N s lam) := 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.PJ.Rn.jK`, Solutions/J6SegILPreJK19.lean (lines 39–168) of the round-six development.

View graph