Round-six lemma `segStepR_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.segStepR_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 : 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) {a0 : ℤ} {lt : List ℤ} (hGt : G tgt = a0 :: lt)
    (za0 : zsz a0 ≤ Bb) {ru rv rw : ℤ} {n : ℕ} {Lu Lv Lw LR LN : List Item}
    (hRu : (encK s G).G pRu = .int ru :: Lu) (hRv : (encK s G).G pRv = .int rv :: Lv)
    (hRw : (encK s G).G pRw = .int rw :: Lw) (hRR : (encK s G).G IntMul.Kappa.R6.IL2C.pR = .int Rv :: LR)
    (hNn : (encK s G).G pN = .int (n : ℤ) :: LN)
    (hru : 0 < ru) (hrv : 0 < rv) (hrw : 2 ≤ rw)
    (zru : zsz ru ≤ Bb) (zrv : zsz rv ≤ Bb) (zrw : zsz rw ≤ Bb) (hnb : zsz (n : ℤ) ≤ Bb)
    {eu ev ew ea efin : Ex HS} {u v w a r : ℤ}
    (hu : 0 ≤ u) (hv : 0 ≤ v) (hw : 0 < w) (hub : zsz u ≤ Bb) (hvb : zsz v ≤ Bb)
    (hTm : 1 ≤ Tm) (hbig : |a| + Tm * w * rw ^ n < 2 ^ Bb)
    (hrv' : NoSeg ev) (hrw' : NoSeg ew) (hra : NoSeg ea)
    (Eu : ESp eu (encK s G) Bb u) (Ev : ESp ev (encK s G) Bb v) (Ew : ESp ew (encK s G) Bb w)
    (Ea : ESp ea (encK s G) Bb a)
    (Efin : ∀ G' : Fin HS → List ℤ, G' IntMul.Kappa.R6.IL2C.rA = (a + segSum tf ru rv rw w u v n) :: G IntMul.Kappa.R6.IL2C.rA →
      (∀ i, i ≠ IntMul.Kappa.R6.IL2C.rA → i ≠ IntMul.Kappa.R6.IL2C.rU → i ≠ IntMul.Kappa.R6.IL2C.rV → i ≠ IntMul.Kappa.R6.IL2C.rW → G' i = G i) → ESp efin (encK s G') Bb r) :
    FSp (segStepR eu ev ew ea T tgt efin) (encK s G)
      (encK s (Function.update G tgt (r :: lt)))
      (cStepR T Bb n (eu.size + ev.size + ew.size + ea.size + efin.size))

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