Round-six lemma `vStep_fsp`

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

theorem IntMul.Kappa.R6.IL2C.vStep_fsp {T : Ex HS} {tf : ℤ → ℤ → ℤ} {Bb : ℕ} {Tm Rv : ℤ}
    (hT : SegTR T tf Bb Tm Rv) (s : IState HS) (G : Fin HS → List ℤ) (hGc : G IntMul.Kappa.R6.IL2C.rC = [])
    {tgt q : Fin HS} (ht56 : tgt.val < 56) (htA : tgt ≠ IntMul.Kappa.R6.IL2C.rA) (htU : tgt ≠ IntMul.Kappa.R6.IL2C.rU) (htV : tgt ≠ IntMul.Kappa.R6.IL2C.rV)
    (htW : tgt ≠ IntMul.Kappa.R6.IL2C.rW) (htC : tgt ≠ IntMul.Kappa.R6.IL2C.rC) (ht6 : tgt ≠ pRu) (ht7 : tgt ≠ pRv) (ht8 : tgt ≠ pRw)
    (hq56 : q.val < 56) (hqA : q ≠ IntMul.Kappa.R6.IL2C.rA) (hqU : q ≠ IntMul.Kappa.R6.IL2C.rU) (hqV : q ≠ IntMul.Kappa.R6.IL2C.rV) (hqW : q ≠ IntMul.Kappa.R6.IL2C.rW)
    (hq6 : q ≠ pRu) (hq7 : q ≠ pRv) (hq8 : q ≠ pRw)
    {v Q : ℕ} {lt : List ℤ} (hGt : G tgt = (v : ℤ) :: lt) (hvQ : v < Q)
    {LQ : List Item} (hGq : (encK s G).G q = .int (Q : ℤ) :: LQ)
    {n : ℕ} {LR LN : List Item}
    (hRR : (encK s G).G IntMul.Kappa.R6.IL2C.pR = .int Rv :: LR) (hNn : (encK s G).G pN = .int (n : ℤ) :: LN)
    {eru erv erw eu ev ew : Ex HS} {ru rv rw u v' w : ℤ}
    (Eru : ESp eru (encK s G) Bb ru) (Erv : ESp erv (encK s G) Bb rv)
    (Erw : ESp erw (encK s G) Bb rw)
    (n1 : NoRad erv) (n2 : NoRad erw) (n3 : NoRad eu) (n4 : NoRad ev) (n5 : NoRad ew)
    (s2 : NoSeg ev) (s3 : NoSeg ew)
    (hsz : eru.size + erv.size + erw.size + eu.size + ev.size + ew.size ≤ 60)
    (Eu : ESp eu (encK s G) Bb u) (Ev : ESp ev (encK s G) Bb v') (Ew : ESp ew (encK s G) Bb w)
    (hru : 0 < ru) (hrv : 0 < rv) (hrw : 2 ≤ rw) (hnb : zsz (n : ℤ) ≤ Bb)
    (hu : 0 ≤ u) (hv : 0 ≤ v') (hw : 0 < w) (hTm : 1 ≤ Tm)
    (hTQ : Tm * w * rw ^ n ≤ (Q : ℤ) * Q) (h3 : 3 * ((Q : ℤ) * Q) < 2 ^ Bb)
    {c : ℤ} (hc : c = 1 ∨ c = -1) :
    FSp (vStep eru erv erw eu ev ew T tgt c q) (encK s G)
      (encK s (Function.update G tgt
        ((subM Q v (-(c * segSum tf ru rv rw w u v' n)) : ℤ) :: lt))) (cV T Bb n)

Context. Round six, compact controls (I2C): the key program of the correction

keyProgC computes, for the record index m on register rm, the key κ m = l.stepP (fun x c => TlS x (Psi x c)) m (the pull composite of the program followed by the ideal map) and pushes it on rK (keyProgC_fsp). The layout parameters are read from the registers 24 … 35 and 13 (QL); the values x, t, u, y live on 4, 5, 9, 12. Each of the eleven value updates is one segment loop (vStep, vStep_fsp).

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