Round-six lemma `iB`
ProvedJ6Seg.PJ.Rn.iBAn 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.J6SegILPreJK14):
theorem J6Seg.PJ.Rn.iB (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hu : BV W u)
(h1 : u 1 = B.st (Lg L r)) (h2 : u 2 = B.len (Lg L r)) (h3 : u 3 = i) (h6 : u 6 = r)
(h7 : u 7 = Lg L r) (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) (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) (hm : 0 < m) (hmN : m ≤ N)
(hLb : ∀ j ∈ L, j ≤ 2 ^ W) (h54 : D 54 = []) (bss : s * s ≤ 2 ^ W)
(hCB : CcBnd W s t α T B (Lg L r)) :
Rn PJ.iB u D (fun v' => Fxk [4, 5, 8, 12, 29] u v' ∧ BV W v')
(update D SCC (ccOf T B L B.w r i :: D SCC)) (cIB W N B.w)
Context. B5 J side, part K14: one coupling window
For row r (on 6, l = L[r] on 7) and window slot i (on 3): read b = L[qOf r i],
sum ccT (jL), push ccOf r i on SCC = 46 (Rn.iB); iL = forL 53 11 3 iB pushes the
whole window (Rn.iL).
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*).
-- 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 i m s t α : ℕ}
theorem J6Seg.PJ.Rn.iB (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hu : BV W u)
(h1 : u 1 = B.st (Lg L r)) (h2 : u 2 = B.len (Lg L r)) (h3 : u 3 = i) (h6 : u 6 = r)
(h7 : u 7 = Lg L r) (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) (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) (hm : 0 < m) (hmN : m ≤ N)
(hLb : ∀ j ∈ L, j ≤ 2 ^ W) (h54 : D 54 = []) (bss : s * s ≤ 2 ^ W)
(hCB : CcBnd W s t α T B (Lg L r)) :
Rn PJ.iB u D (fun v' => Fxk [4, 5, 8, 12, 29] u v' ∧ BV W v')
(update D SCC (ccOf T B L B.w r i :: D SCC)) (cIB W N B.w) := by sorry