Round-six lemma `jBody_bnd`
ProvedJ6Seg.JK.jBody_bndAn 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.J6SegILJKer13):
theorem J6Seg.JK.jBody_bnd {P k K G Xb Bc Bx : ℕ} {fs : List (List ℤ)} {bs : List (List ℤ × List ℤ × ℤ × ℤ)}
{cc : List (List ℤ)} {v : List ℤ} (hD : PartD P k K G Xb Bc fs bs cc v) (hBx : k + 1 ≤ Bx)
(hc : Bc ≤ Bx) : Bnd Bx (jBody k fs bs cc)
Context. B-line IL, the J kernel (B4), part 13: one real part
partP: from the row v (length G) on V and the table body
flatT fs ++ flatB k bs ++ flatT cc on dTJ, the forward loop, the backward loop, the cyclic
extension and the coupling window leave W = Wl.reverse with
Wl = (range m).map (wF P cc (zext K (bwdS P bs (fA P fs v m) m).1)); every other stack is as
before (V emptied), the table is restored from TT (partP_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 NLogN.KFB Function Finset
theorem J6Seg.JK.jBody_bnd {P k K G Xb Bc Bx : ℕ} {fs : List (List ℤ)} {bs : List (List ℤ × List ℤ × ℤ × ℤ)}
{cc : List (List ℤ)} {v : List ℤ} (hD : PartD P k K G Xb Bc fs bs cc v) (hBx : k + 1 ≤ Bx)
(hc : Bc ≤ Bx) : Bnd Bx (jBody k fs bs cc) := by sorry