Round-six lemma `jTab_bnd`
ProvedJ6Seg.PJ.jTab_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.J6SegILPreJK31):
theorem J6Seg.PJ.jTab_bnd {P k' K G Xb Bc B kJ : ℕ} {fs : List (List ℤ)}
{bs : List (List ℤ × List ℤ × ℤ × ℤ)} {cc : List (List ℤ)} {v : List ℤ}
(hD : JK.PartD P k' K G Xb Bc fs bs cc v) (hXb : Xb ≤ B) (hBc : Bc + 4 ≤ B)
(hk : kJ + 1 ≤ B) (hP : P + 2 ≤ B) :
Bnd B (tabsT (fun _ => JK.jTab P kJ K G fs bs cc) 1)
Context. B5 J side, part K31: the entries of the J table are bounded
jTab_bnd: from the shapes and bounds PartD of a line (at any kernel precision k'), every
entry of tabsT (fun _ => jTab P kJ K G fs bs cc) 1 has zsz ≤ B once Xb ≤ B, Bc + 4 ≤ B,
kJ + 1 ≤ B and P + 2 ≤ B.
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.PJ open IntMul NLogN NLogN.KIL NLogN.RS Function
theorem J6Seg.PJ.jTab_bnd {P k' K G Xb Bc B kJ : ℕ} {fs : List (List ℤ)}
{bs : List (List ℤ × List ℤ × ℤ × ℤ)} {cc : List (List ℤ)} {v : List ℤ}
(hD : JK.PartD P k' K G Xb Bc fs bs cc v) (hXb : Xb ≤ B) (hBc : Bc + 4 ≤ B)
(hk : kJ + 1 ≤ B) (hP : P + 2 ≤ B) :
Bnd B (tabsT (fun _ => JK.jTab P kJ K G fs bs cc) 1) := by sorry