Round-six lemma `partP_spec`

An 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.partP_spec {M : MulSpec} {P k K G Xb Φm Bx Bc : ℕ} {fs : List (List ℤ)}
    {bs : List (List ℤ × List ℤ × ℤ × ℤ)} {cc : List (List ℤ)} {v R : List ℤ}
    (hMB : MulBnd M (k + 2) Φm) (s : IState HS) {F : Fin HS → List ℤ}
    (hF : PartF P k K G fs.length (nBd bs) (jBody k fs bs cc).length F)
    (hD : PartD P k K G Xb Bc fs bs cc v) (hBx : 3 * k + 10 ≤ Bx) (hV : F V = v)
    (hT : F dTJ = jBody k fs bs cc ++ R) :
    MSp M partP (encK s F) (encK s (update (update F V []) W (wOut P k K fs bs cc v).reverse))
      (partC k K G fs bs cc (uC Φm Bx Bc))

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*).