Round-six lemma `rB`

Proved

J6Seg.PJ.Rn.rB

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

complexity-theoryinteger-multiplicationkappa-improvement

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

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

theorem J6Seg.PJ.Rn.rB (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hu : BV W u) (h6 : u 6 = r) (hr : r < m)
    (h11 : u 11 = 2 * B.w + 1) (h20 : u 20 = Q) (h22 : u 22 = s)
    (h23 : u 23 = t) (h25 : u 25 = α) (h26 : u 26 = B.w) (h28 : u 28 = m)
    (hBs : B.s = s) (hs : 0 < s) (hB : BlocksOK s t B) (hQW : Q ≤ W + 1) (hwW : 2 * B.w + 1 < 2 ^ W)
    (hcpl : ∀ i h, T.cpl i h = HvdH.expNeg Q (s ^ 2) (α ^ 2 * (HvdH.eKz s t i h).toNat))
    (hL : D 30 = L.map (fun j : ℕ => (j : ℤ))) (hLm : L.length = m) (hmN : m ≤ N) (hsN : s ≤ N)
    (hLs : ∀ j ∈ L, j < s)
    (h32 : D 32 = (List.range s).map (fun j => (B.st j : ℤ)))
    (h33 : D 33 = (List.range s).map (fun j => (B.len j : ℤ)))
    (h53 : D 53 = []) (h54 : D 54 = []) (bss : s * s ≤ 2 ^ W)
    (hCB : CcBnd W s t α T B (Lg L r)) :
    Rn PJ.rB u D (fun v' => Fxk J6Seg.PJ.FR u v' ∧ BV W v')
      (update D SCC (rvL (ccOf T B L B.w r) (2 * B.w + 1) ++ (((2 * B.w + 1 : ℕ) : ℤ) :: D SCC)))
      (cRB W N B.w)

Context. B5 J side, part K15: all coupling windows onto 41

ccP = 11 := 2w+1; forL 50 28 6 (rows reads; push 2w+1 on SCC; iL); 11 := m(2w+2); mvK SCC 41 puts JK.flatT (rows of ccOf) in front of stack 41 (Rn.ccP).

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 J6Seg.PJ.E Finset
variable {Q W N : ℕ} {T : Tables} {B : Blocks} {L : List ℕ} {u : Vr} {D : Cs} {r m s t α : ℕ}

Formal statement

theorem J6Seg.PJ.Rn.rB (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hu : BV W u) (h6 : u 6 = r) (hr : r < m)
    (h11 : u 11 = 2 * B.w + 1) (h20 : u 20 = Q) (h22 : u 22 = s)
    (h23 : u 23 = t) (h25 : u 25 = α) (h26 : u 26 = B.w) (h28 : u 28 = m)
    (hBs : B.s = s) (hs : 0 < s) (hB : BlocksOK s t B) (hQW : Q ≤ W + 1) (hwW : 2 * B.w + 1 < 2 ^ W)
    (hcpl : ∀ i h, T.cpl i h = HvdH.expNeg Q (s ^ 2) (α ^ 2 * (HvdH.eKz s t i h).toNat))
    (hL : D 30 = L.map (fun j : ℕ => (j : ℤ))) (hLm : L.length = m) (hmN : m ≤ N) (hsN : s ≤ N)
    (hLs : ∀ j ∈ L, j < s)
    (h32 : D 32 = (List.range s).map (fun j => (B.st j : ℤ)))
    (h33 : D 33 = (List.range s).map (fun j => (B.len j : ℤ)))
    (h53 : D 53 = []) (h54 : D 54 = []) (bss : s * s ≤ 2 ^ W)
    (hCB : CcBnd W s t α T B (Lg L r)) :
    Rn PJ.rB u D (fun v' => Fxk J6Seg.PJ.FR u v' ∧ BV W v')
      (update D SCC (rvL (ccOf T B L B.w r) (2 * B.w + 1) ++ (((2 * B.w + 1 : ℕ) : ℤ) :: D SCC)))
      (cRB W N B.w) := 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.rB`, Solutions/J6SegILPreJK15.lean (lines 41–142) of the round-six development.

View graph