Round-six lemma `bwdP_spec`
ProvedJ6Seg.JK.bwdP_specAn 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.J6SegILJKer9):
theorem J6Seg.JK.bwdP_spec {M : MulSpec} {Xb Φm Bx Bc : ℕ} (hMB : MulBnd M (k + 2) Φm) (s : IState HS)
{lp lp1 lk lh : List ℤ} (hF : BwdF P k F lp lp1 lk) (hD : BwdD P bs bts Xb Bc)
(hk : 2 * Xb + 2 * P + Bc + 6 ≤ k) (hBx : 2 * k + 8 ≤ Bx)
(hT : F dTJ = flatB k bs ++ R) (hTT : F J6Seg.JK.TT = T0) (hA : F A = bts) (hZ : F Z = [])
(hBZ : F BZ = []) (hHM : F HM = (bs.length : ℤ) :: lh) :
MSp M J6Seg.JK.bwdP (encK s F) (encK s (bSt P k F bs bts R T0 bs.length))
((∑ j ∈ range bs.length, (recL bs j + 6) + 1) * uC Φm Bx Bc)
Context. B-line IL, the J kernel (B4), part 9: the backward loop
bwdP runs bwdB for the m = top HM records: from A = bts, Z = BZ = [] and the table
flatB k bs on dTJ it leaves Z = (bwdS P bs bts m).1 = bwdK P bs bts [] []
(bwdK_eq_bwdS), BZ = (bwdS m).2, A = [], the table moved onto TT (bwdP_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 k : ℕ} {F : Fin HS → List ℤ} {bs : List (List ℤ × List ℤ × ℤ × ℤ)} {bts R T0 : List ℤ}
theorem J6Seg.JK.bwdP_spec {M : MulSpec} {Xb Φm Bx Bc : ℕ} (hMB : MulBnd M (k + 2) Φm) (s : IState HS)
{lp lp1 lk lh : List ℤ} (hF : BwdF P k F lp lp1 lk) (hD : BwdD P bs bts Xb Bc)
(hk : 2 * Xb + 2 * P + Bc + 6 ≤ k) (hBx : 2 * k + 8 ≤ Bx)
(hT : F dTJ = flatB k bs ++ R) (hTT : F J6Seg.JK.TT = T0) (hA : F A = bts) (hZ : F Z = [])
(hBZ : F BZ = []) (hHM : F HM = (bs.length : ℤ) :: lh) :
MSp M J6Seg.JK.bwdP (encK s F) (encK s (bSt P k F bs bts R T0 bs.length))
((∑ j ∈ range bs.length, (recL bs j + 6) + 1) * uC Φm Bx Bc) := by sorry