Round-six lemma `cpl_body`
ProvedJ6Seg.JK.cpl_bodyAn 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.J6SegILJKer11):
theorem J6Seg.JK.cpl_body {M : MulSpec} {Xb Φm Bx Bc : ℕ} (hMB : MulBnd M Xb Φm) (s : IState HS)
{lp lp1 : List ℤ} (hF : CplF P F lp lp1) (hm : cc.length ≤ ze.length)
(hwf : ∀ r (h : r < cc.length), cc[r].length + r ≤ ze.length)
(hcB : ∀ r (h : r < cc.length), Bnd Xb cc[r]) (hzB : Bnd Xb ze) (hzl : ze.length < 2 ^ Bc)
(hXB : 2 * Xb + P + Bc + 3 ≤ Bx) (N r : ℕ) (hr : r < cc.length) :
MSp M cplB (encK s (update (cSt P F cc ze R T0 r) CR [(N : ℤ) - r]))
(encK s (update (cSt P F cc ze R T0 (r + 1)) CR [(N : ℤ) - r]))
((cc[r].length + 2) * uC Φm Bx Bc)
Context. B-line IL, the J kernel (B4), part 11: the coupling window
Row r of cplP reads |cc_r|, runs the dot loop on the window E = ze.drop r and pushes
W_r = dotF P cc_r (ze.drop r) onto W, then drops the head of E (cpl_body). After
m = top HM rows W = (W_0, …, W_{m-1}).reverse (cplP_spec).
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_Defs66
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open J6Seg J6Seg.JK
open IntMul NLogN NLogN.KIL Function Finset
variable (P : ℕ) (F : Fin HS → List ℤ) (cc : List (List ℤ)) (ze R T0 : List ℤ)
variable {P F cc ze R T0}
theorem J6Seg.JK.cpl_body {M : MulSpec} {Xb Φm Bx Bc : ℕ} (hMB : MulBnd M Xb Φm) (s : IState HS)
{lp lp1 : List ℤ} (hF : CplF P F lp lp1) (hm : cc.length ≤ ze.length)
(hwf : ∀ r (h : r < cc.length), cc[r].length + r ≤ ze.length)
(hcB : ∀ r (h : r < cc.length), Bnd Xb cc[r]) (hzB : Bnd Xb ze) (hzl : ze.length < 2 ^ Bc)
(hXB : 2 * Xb + P + Bc + 3 ≤ Bx) (N r : ℕ) (hr : r < cc.length) :
MSp M cplB (encK s (update (cSt P F cc ze R T0 r) CR [(N : ℤ) - r]))
(encK s (update (cSt P F cc ze R T0 (r + 1)) CR [(N : ℤ) - r]))
((cc[r].length + 2) * uC Φm Bx Bc) := by sorry