A `Γ` loop (round six, `stG_sp`)

A Γ loop (generic pushed value F k = eF(Γ_k)).

The following holds (Lean statement, in the scope of module Solutions.J6SegILPre8):

theorem J6Seg.PreT.stG_sp (s : IState HS) (v : Fin HS → ℤ) (c : Fin HS → List ℤ) {O : Fin HS}
    (hO : O ∉ rg) (hO5 : O.val < 56) (hOC : O ≠ Cu) (hc : c Cu = []) {P R sN tN lam aN A : ℕ}
    (hi : StIn2 v P R sN tN lam aN A) (hPA : P ≤ A)
    {eF : Ex HS} (hiF : InRg eF) (hpF : Poly eF = true) (hdF : J6Seg.PreT.dg eF ≤ 40)
    (hoF : ∀ (u : Fin HS → ℤ) (cu : Fin HS → List ℤ), eF.ok (encK s (J6Seg.PreT.RF u cu))) (F : ℕ → ℤ)
    (hF : ∀ k (u : Fin HS → ℤ) (cu : Fin HS → List ℤ), u 4 = gamI P sN tN aN k → u 9 = 2 ^ P →
      eF.eval (encK s (J6Seg.PreT.RF u cu)) = F k)
    (bq : ∀ k < lam, |expNeg P sN (2 * aN ^ 2 * tN * (k + 1))| ≤ 2 ^ A)
    (bF : ∀ k < lam, |F k| ≤ 2 ^ A) (bG : ∀ k < lam, |gamI P sN tN aN (k + 1)| ≤ 2 ^ A) :
    ∃ v' : Fin HS → ℤ, (∀ j, j ≠ 4 → j ≠ 5 → j ≠ 11 → j ≠ 12 → v' j = v j) ∧ VB v' A ∧
    Sp (stG O eF) (encK s (J6Seg.PreT.RF v c)) (encK s (J6Seg.PreT.RF v' (Function.update c O (rv F lam ++ c O))))
      (cStG A lam eF)

Context. B-line IL, pre-tables (B5), part 8: the stage tables gam, gi

stG O eF = Γ := 2^P; loop U < λ { q := expNeg P s (2α²t(U+1)); X := eF(Γ); Γ := fmul P Γ (2^P - q⁺); push X; U++ }: with eF = Γ (stGam) it pushes gamI 0 … gamI (λ-1), with eF = fdiv P 2^P Γ (stGi) the values giI u.

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