Round-six lemma `sp_mvP`

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.J6SegKr2):

theorem J6Seg.KR.sp_mvP {X Y T C R : Fin HS} (hXY : X ≠ Y) (hXT : X ≠ T) (hXC : X ≠ C) (hYT : Y ≠ T)
    (hYC : Y ≠ C) (hTC : T ≠ C) (hRX : R ≠ X) (hRY : R ≠ Y) (hRT : R ≠ T) (hRC : R ≠ C)
    (hX5 : X.val < 56) (hY5 : Y.val < 56) (hT5 : T.val < 56) (hC5 : C.val < 56)
    (hR5 : R.val < 56) (s : IState HS) (f : Fin HS → List ℤ) (z : List GI) (lx lr : List ℤ)
    (hX : f X = gflat z ++ lx) (hT : f T = []) (hC : f C = [])
    (hR : f R = (z.length : ℤ) :: lr) (B : ℕ) (hz : GB B z) (hn : zsz (z.length : ℤ) ≤ B) :
    Sp (mvP X Y T C R) (encK s f)
      (encK s (Function.update (Function.update f X lx) Y (gflat z.reverse ++ f Y)))
      (cMvP z.length B)

Context. B3 (chunk kernel), part 2: register loops on managed states

Counted register loops (RS.rep with the count on top of a register) on encK states:

• mvP X Y T C R: move n Gaussian pairs from X to Y, keeping each pair's orientation (gflat z ++ lx on X ↦ gflat z.reverse on top of Y);
• rdP V O C R: round pairs (rs P on both parts) from a reversed flat list on V to O (gsw u ++ lv ↦ gflat ((u.reverse).map rsG) on top of O);
• rgP A Y C R: a real table as Gaussian pairs (a ++ la on A ↦ gflat (a.reverse.map (·, 0)) on top of Y);
• zeroR, dropR, dupR: push zeros, drop, duplicate-move with a register count.

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