Round-six lemma `bwd_body`
ProvedJ6Seg.JK.bwd_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.J6SegILJKer8):
theorem J6Seg.JK.bwd_body {M : MulSpec} {Xb Φm Bx Bc : ℕ} (hMB : MulBnd M (k + 2) Φm) (s : IState HS)
{lp lp1 lk : 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) (N j : ℕ) (hj : j < bs.length) :
MSp M bwdB (encK s (update (bSt P k F bs bts R T0 j) CR [(N : ℤ) - j]))
(encK s (update (bSt P k F bs bts R T0 (j + 1)) CR [(N : ℤ) - j]))
((bs[j].1.length + bs[j].2.1.length + 5) * uC Φm Bx Bc)
Context. B-line IL, the J kernel (B4), part 8: one backward record
The backward table flatB k bs = ⋃_j (|cb| :: cb ++ |cz| :: cz ++ [pv, iv, fl]) (with the
reciprocal iv = ivOf k pv) lies on dTJ. Record j computes both dot products against
Z = (bwdS j).1 and BZ = (bwdS j).2, the numerator bt_j - d₁ - d₂, its fixed-point quotient
by pv (recip, or 0 for pv = 0), pushes it onto Z and, for fl = 1, onto BZ
(stepB): bwd_body.
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 ℤ)
variable {P k F bs bts R T0}
theorem J6Seg.JK.bwd_body {M : MulSpec} {Xb Φm Bx Bc : ℕ} (hMB : MulBnd M (k + 2) Φm) (s : IState HS)
{lp lp1 lk : 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) (N j : ℕ) (hj : j < bs.length) :
MSp M bwdB (encK s (update (bSt P k F bs bts R T0 j) CR [(N : ℤ) - j]))
(encK s (update (bSt P k F bs bts R T0 (j + 1)) CR [(N : ℤ) - j]))
((bs[j].1.length + bs[j].2.1.length + 5) * uC Φm Bx Bc) := by sorry