The slot loop (round six, `vlL`)

Proved

J6Seg.PJ.Rn.vlL

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

complexity-theoryinteger-multiplicationkappa-improvement

The slot loop.

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

theorem J6Seg.PJ.Rn.vlL {v : Vr} (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hv : BV W v)
    (h1 : v 1 = c) (h2 : v 2 = n) (h11 : v 11 = n * (2 * B.w + 1)) (h20 : v 20 = Q) (h22 : v 22 = s)
    (h23 : v 23 = t) (h25 : v 25 = α) (h26 : v 26 = B.w) (h9 : v 9 = 2 ^ Q)
    (h10 : v 10 = 2 ^ (Q + 1))
    (hBs : B.s = s) (hs : 0 < s) (hBa : B.st a = c)
    (hBl : ∀ u < n, B.st (c + u) = c ∧ B.len (c + u) = n)
    (hnW : n * (2 * B.w + 1) < 2 ^ W) (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)
    (hSV : D SV = []) (hSC : D SC = []) (h50 : D 50 = [])
    (bMI : ∀ i < n, |miV Q T B a i| ≤ 2 ^ W)
    (bss : s * s ≤ 2 ^ W)
    (bX : ∀ u < n, ∀ j < 2 * B.w + 1, α ^ 2 * (HvdH.eKz s t ((c + u : ℕ) : ℤ)
      ((j : ℤ) - B.w)).toNat ≤ 2 ^ W)
    (bC : ∀ u < n, ∀ j < 2 * B.w + 1, |T.cpl (c + u) ((j : ℤ) - B.w)| ≤ 2 ^ W)
    (bV : ∀ y < n * (2 * B.w + 1), |gV Q T B a y| ≤ 2 ^ W) :
    Rn PJ.vlL v D (fun v' => Fxk [3, 4, 5, 8, 29] v v' ∧ BV W v')
      (cfV D (gV Q T B a) (gC B c) (n * (2 * B.w + 1)))
      (cFor W (n * (2 * B.w + 1)) (costL W N PJ.vlB))

Context. B5 J side, part K5: the slot loop

PJ.vlL = forL 50 11 3 PJ.vlB (count n (2w+1) on 11): pushes gV y on SV and gC y on SC for all slots y (Rn.vlL); both stacks end reversed.

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} {D : Cs} {a c n s t α : ℕ}

Formal statement

theorem J6Seg.PJ.Rn.vlL {v : Vr} (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hv : BV W v)
    (h1 : v 1 = c) (h2 : v 2 = n) (h11 : v 11 = n * (2 * B.w + 1)) (h20 : v 20 = Q) (h22 : v 22 = s)
    (h23 : v 23 = t) (h25 : v 25 = α) (h26 : v 26 = B.w) (h9 : v 9 = 2 ^ Q)
    (h10 : v 10 = 2 ^ (Q + 1))
    (hBs : B.s = s) (hs : 0 < s) (hBa : B.st a = c)
    (hBl : ∀ u < n, B.st (c + u) = c ∧ B.len (c + u) = n)
    (hnW : n * (2 * B.w + 1) < 2 ^ W) (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)
    (hSV : D SV = []) (hSC : D SC = []) (h50 : D 50 = [])
    (bMI : ∀ i < n, |miV Q T B a i| ≤ 2 ^ W)
    (bss : s * s ≤ 2 ^ W)
    (bX : ∀ u < n, ∀ j < 2 * B.w + 1, α ^ 2 * (HvdH.eKz s t ((c + u : ℕ) : ℤ)
      ((j : ℤ) - B.w)).toNat ≤ 2 ^ W)
    (bC : ∀ u < n, ∀ j < 2 * B.w + 1, |T.cpl (c + u) ((j : ℤ) - B.w)| ≤ 2 ^ W)
    (bV : ∀ y < n * (2 * B.w + 1), |gV Q T B a y| ≤ 2 ^ W) :
    Rn PJ.vlL v D (fun v' => Fxk [3, 4, 5, 8, 29] v v' ∧ BV W v')
      (cfV D (gV Q T B a) (gC B c) (n * (2 * B.w + 1)))
      (cFor W (n * (2 * B.w + 1)) (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.vlL`, Solutions/J6SegILPreJK5.lean (lines 42–95) of the round-six development.

View graph