Round-six lemma `sp_dupR`

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_dupR {X Y Z C R : Fin HS} (hXY : X ≠ Y) (hXZ : X ≠ Z) (hYZ : Y ≠ Z) (hXC : X ≠ C)
    (hYC : Y ≠ C) (hZC : Z ≠ C) (hRC : R ≠ C) (hRX : R ≠ X) (hRY : R ≠ Y) (hRZ : R ≠ Z)
    (hX5 : X.val < 56) (hY5 : Y.val < 56) (hZ5 : Z.val < 56) (hC5 : C.val < 56)
    (hR5 : R.val < 56) (s : IState HS) (f : Fin HS → List ℤ) (L lx lr : List ℤ)
    (hX : f X = L ++ lx) (hC : f C = []) (hR : f R = (L.length : ℤ) :: lr) (B : ℕ)
    (hL : Bnd B L) (hn : zsz (L.length : ℤ) ≤ B) :
    Sp (dupR X Y Z C R) (encK s f)
      (encK s (Function.update (Function.update (Function.update f X lx) Y (L.reverse ++ f Y)) Z
        (L.reverse ++ f Z))) (cMvP L.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*).