One `Γ` step (`clG_sp`)

One Γ step.

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

theorem J6Seg.PreT.clG_sp (s : IState HS) (w : Fin HS → ℤ) (cc : Fin HS → List ℤ) {A : ℕ} (hA : 2 ≤ A)
    (hw : VB w A) {P sN tN aN k : ℕ} (h20 : w 20 = P) (h22 : w 22 = sN) (h23 : w 23 = tN)
    (h25 : w 25 = aN) (h12 : w 12 = k) (h9 : w 9 = 2 ^ P) (h10 : w 10 = 2 ^ (P + 1))
    {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)))
    {Fk : ℤ} (hF : ∀ (u : Fin HS → ℤ) (cu : Fin HS → List ℤ), u 4 = w 4 → u 9 = 2 ^ P →
      eF.eval (encK s (J6Seg.PreT.RF u cu)) = Fk)
    (hq : |expNeg P sN (2 * aN ^ 2 * tN * (k + 1))| ≤ 2 ^ A) (hFk : |Fk| ≤ 2 ^ A)
    (hG : |J6Seg.fmul P (w 4) (2 ^ P - max (expNeg P sN (2 * aN ^ 2 * tN * (k + 1))) 0)| ≤ 2 ^ A) :
    Sp (clG eF) (encK s (J6Seg.PreT.RF w cc))
      (encK s (J6Seg.PreT.RF (Function.update (Function.update (Function.update w 5
        (expNeg P sN (2 * aN ^ 2 * tN * (k + 1)))) 11 Fk) 4
        (J6Seg.fmul P (w 4) (2 ^ P - max (expNeg P sN (2 * aN ^ 2 * tN * (k + 1))) 0))) cc))
      (cCall (.reg 20) (.reg 22) jQE (.lit 0) (BW A) (expNegCost P (BW A) (BW A)) +
        J6Seg.PreT.cE eF (BW A) + J6Seg.PreT.cE gUpE (BW A))

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