The slot body (round six, `vlB`)

Proved

J6Seg.PJ.Rn.vlB

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

complexity-theoryinteger-multiplicationkappa-improvement

The slot body.

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

theorem J6Seg.PJ.Rn.vlB (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hu : BV W u)
    (h1 : u 1 = c) (h2 : u 2 = n) (h3 : u 3 = y) (h20 : u 20 = Q) (h22 : u 22 = s) (h23 : u 23 = t)
    (h25 : u 25 = α) (h26 : u 26 = B.w) (h9 : u 9 = 2 ^ Q) (h10 : u 10 = 2 ^ (Q + 1))
    (hBs : B.s = s) (hs : 0 < s) (hBa : B.st a = c)
    (hBl : B.st (c + y / (2 * B.w + 1)) = c) (hBn : B.len (c + y / (2 * B.w + 1)) = n)
    (hy : y < n * (2 * B.w + 1)) (hnN : n ≤ N) (hQW : Q ≤ W + 1)
    (hcpl : ∀ i h, T.cpl i h = HvdH.expNeg Q (s ^ 2) (α ^ 2 * (HvdH.eKz s t i h).toNat))
    (hMI : D SMI = ((List.range n).map (miV Q T B a)).reverse)
    (bMI : ∀ i < n, |miV Q T B a i| ≤ 2 ^ W)
    (bss : s * s ≤ 2 ^ W)
    (bX : α ^ 2 * (HvdH.eKz s t ((c + y / (2 * B.w + 1) : ℕ) : ℤ)
      (((y % (2 * B.w + 1) : ℕ) : ℤ) - B.w)).toNat ≤ 2 ^ W)
    (bC : |T.cpl (c + y / (2 * B.w + 1)) (((y % (2 * B.w + 1) : ℕ) : ℤ) - B.w)| ≤ 2 ^ W)
    (bV : |gV Q T B a y| ≤ 2 ^ W) :
    Rn (progL PJ.vlB) u D (fun v' => Fxk [4, 5, 8, 29] u v' ∧ BV W v')
      (update (update D SV (gV Q T B a y :: D SV)) SC (gC B c y :: D SC)) (costL W N PJ.vlB)

Context. B5 J side, part K4: the capacitance row, slot values

For row a (block start c on 1, length n on 2) and slot y < n (2w+1) on 3 (u = y / (2w+1), j = y % (2w+1)): the body PJ.vlB reads miV a u from SMI (reversed), computes the coupling entry with one expNeg call and pushes gV y = fmul (miV a u) (cpl (c+u) (j-w)) on SV = 46 and the column tag gC y = if hcT then col else -1 on SC = 13 (Rn.vlB).

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_Defs70

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.PJ
open IntMul NLogN NLogN.KIL NLogN.RS Function J6Seg.PJ.E Finset
variable {Q W N : ℕ} {T : Tables} {B : Blocks} {u : Vr} {D : Cs} {a c n y s t α : ℕ}

Formal statement

theorem J6Seg.PJ.Rn.vlB (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hu : BV W u)
    (h1 : u 1 = c) (h2 : u 2 = n) (h3 : u 3 = y) (h20 : u 20 = Q) (h22 : u 22 = s) (h23 : u 23 = t)
    (h25 : u 25 = α) (h26 : u 26 = B.w) (h9 : u 9 = 2 ^ Q) (h10 : u 10 = 2 ^ (Q + 1))
    (hBs : B.s = s) (hs : 0 < s) (hBa : B.st a = c)
    (hBl : B.st (c + y / (2 * B.w + 1)) = c) (hBn : B.len (c + y / (2 * B.w + 1)) = n)
    (hy : y < n * (2 * B.w + 1)) (hnN : n ≤ N) (hQW : Q ≤ W + 1)
    (hcpl : ∀ i h, T.cpl i h = HvdH.expNeg Q (s ^ 2) (α ^ 2 * (HvdH.eKz s t i h).toNat))
    (hMI : D SMI = ((List.range n).map (miV Q T B a)).reverse)
    (bMI : ∀ i < n, |miV Q T B a i| ≤ 2 ^ W)
    (bss : s * s ≤ 2 ^ W)
    (bX : α ^ 2 * (HvdH.eKz s t ((c + y / (2 * B.w + 1) : ℕ) : ℤ)
      (((y % (2 * B.w + 1) : ℕ) : ℤ) - B.w)).toNat ≤ 2 ^ W)
    (bC : |T.cpl (c + y / (2 * B.w + 1)) (((y % (2 * B.w + 1) : ℕ) : ℤ) - B.w)| ≤ 2 ^ W)
    (bV : |gV Q T B a y| ≤ 2 ^ W) :
    Rn (progL PJ.vlB) u D (fun v' => Fxk [4, 5, 8, 29] u v' ∧ BV W v')
      (update (update D SV (gV Q T B a y :: D SV)) SC (gC B c y :: D SC)) (costL W N PJ.vlB) := 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.vlB`, Solutions/J6SegILPreJK4.lean (lines 133–255) of the round-six development.

View graph