The chunk store (`tabK2` layout) (round six, `chunkStore2_sp`)

Proved

J6Seg.PreT.chunkStore2_sp

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

complexity-theoryinteger-multiplicationkappa-improvement

The chunk store (tabK2 layout).

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

theorem J6Seg.PreT.chunkStore2_sp (s : IState HS) (v : Fin HS → ℤ) (c : Fin HS → List ℤ) {O L : Fin HS}
    (hO : O ∉ rg) (hO5 : O.val < 56) (hL : L ∉ rg) (hL5 : L.val < 56) (hOL : O ≠ L)
    (hOx : O ≠ 13 ∧ O ≠ 50 ∧ O ≠ 51 ∧ O ≠ Cu ∧ O ≠ 53 ∧ O ≠ 54)
    (hLx : L ≠ 13 ∧ L ≠ 51 ∧ L ≠ 53 ∧ L ≠ 54 ∧ L ≠ Cu)
    (hc13 : c 13 = []) (hc51 : c 51 = []) (hc53 : c 53 = []) (hc54 : c 54 = []) (hcu : c Cu = [])
    (hcL : c L = [])
    {P R sN tN lam aN A pk b M nc : ℕ}
    (hi : StIn2 v P R sN tN lam aN A) (hPA : P ≤ A) (TB : J6Seg.PreT.TabB P R sN tN aN lam A)
    (h26 : v 26 = pk) (h28 : v 28 = b) (h29 : v 29 = nc)
    (hpkM : pk ≤ M) (hbM : b ≤ M) (hl : 1 ≤ lam) (hsA : sN ≤ 2 ^ A) (hncA : nc * lam ≤ 2 ^ A)
    (hncA' : nc * (9 + 10 * lam) ≤ 2 ^ A) :
    Sp (chunkStoreP2 O L) (encK s (J6Seg.PreT.RF v c))
      (encK s (J6Seg.PreT.RF (Z v) (Function.update (Function.update c O
        (tabsT (tabQ2 P R sN tN lam aN pk b) nc ++ c O)) L
        [((tabsT (tabQ2 P R sN tN lam aN pk b) nc).length : ℤ)])))
      (cCS2 P R A lam M nc)

Context. B-line IL, pre-tables (B5′, tabK2 layout), part 25: the chunk store chunkStore2_sp

chunkStoreP2 O L = preP L; nc rounds (counter 51) of chB2 O L; 6 := 0 builds tabsT (tabQ2 …) nc on O and its length on L. Compared with chunkStore_sp (old tabK): no 1 ≤ b, no λ ≤ M, no BH M width (only pk, b ≤ M for the 2^pk, 2^b header pushes).

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_Defs68

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.PreT
open IntMul NLogN NLogN.KIL NLogN.RS IntMul.HvdH

Formal statement

theorem J6Seg.PreT.chunkStore2_sp (s : IState HS) (v : Fin HS → ℤ) (c : Fin HS → List ℤ) {O L : Fin HS}
    (hO : O ∉ rg) (hO5 : O.val < 56) (hL : L ∉ rg) (hL5 : L.val < 56) (hOL : O ≠ L)
    (hOx : O ≠ 13 ∧ O ≠ 50 ∧ O ≠ 51 ∧ O ≠ Cu ∧ O ≠ 53 ∧ O ≠ 54)
    (hLx : L ≠ 13 ∧ L ≠ 51 ∧ L ≠ 53 ∧ L ≠ 54 ∧ L ≠ Cu)
    (hc13 : c 13 = []) (hc51 : c 51 = []) (hc53 : c 53 = []) (hc54 : c 54 = []) (hcu : c Cu = [])
    (hcL : c L = [])
    {P R sN tN lam aN A pk b M nc : ℕ}
    (hi : StIn2 v P R sN tN lam aN A) (hPA : P ≤ A) (TB : J6Seg.PreT.TabB P R sN tN aN lam A)
    (h26 : v 26 = pk) (h28 : v 28 = b) (h29 : v 29 = nc)
    (hpkM : pk ≤ M) (hbM : b ≤ M) (hl : 1 ≤ lam) (hsA : sN ≤ 2 ^ A) (hncA : nc * lam ≤ 2 ^ A)
    (hncA' : nc * (9 + 10 * lam) ≤ 2 ^ A) :
    Sp (chunkStoreP2 O L) (encK s (J6Seg.PreT.RF v c))
      (encK s (J6Seg.PreT.RF (Z v) (Function.update (Function.update c O
        (tabsT (tabQ2 P R sN tN lam aN pk b) nc ++ c O)) L
        [((tabsT (tabQ2 P R sN tN lam aN pk b) nc).length : ℤ)])))
      (cCS2 P R A lam M nc) := 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.PreT.chunkStore2_sp`, Solutions/J6SegILPre25.lean (lines 42–201) of the round-six development.

View graph