HvdH machine lemma EX.sBody_all (The full `fwdL` / `exactConvL` programs, part 4: the body of the `S̃` )

The following holds (Lean statement, in the scope of module NLogN.HEx4):

theorem NLogN.EX.sBody_all (M : MulSpec) (q : Params) (kb mm Φ Bacc Q Bq Bx : ℕ) (BS : ℕ → ℕ)
    (hM : MulBnd M mm Φ) (hsl : q.s.length = q.K) (hst : ∀ i < q.K, sK q i ≤ tK q i)
    (hBx : Vx q kb < 2 ^ Bx) (k : ℕ) (hk : k < q.K) (H : SAx q kb mm Bacc Q Bq BS k)
    (U : List (ℤ × ℤ)) (w : IState HS) (R LS LM LC : List Item) (hg : Glob q kb w)
    (hD : w.G gD = gints (XS q U k) ++ R) (hL : (XS q U k).length = NS q k)
    (hLB : GB (BS k) (XS q U k))
    (hS : w.G xS = .int (sK q k : ℤ) :: LS) (hMx : w.G xM = .int (NS q k : ℤ) :: LM)
    (hc : w.G cL = .int ((q.K : ℤ) - k) :: LC) :
    NLogN.EX.sBody.run w = (((w.upd gD (gints (XS q U (k + 1)) ++ R)).upd xM
        (.int (NS q (k + 1) : ℤ) :: LM)).upd xU (.int (sK q k : ℤ) :: w.G xU)).upd xS LS ∧
      NLogN.EX.sBody.ok M w ∧
      NLogN.EX.sBody.cost M w ≤
        sapAxCost q.p (sK q k) (tK q k) q.α (mS q k) kb (BS k) mm Φ Bacc Q Bq + sOver Bx ∧
      (XS q U (k + 1)).length = NS q (k + 1) ∧ GB (BS (k + 1)) (XS q U (k + 1))

Context. The lemma belongs to the part The full fwdL / exactConvL programs, part 4: the body of the S̃ axis loop: sBody (iteration k): push the registers of sapAxP (layout HAx2) computed from sₖ (top of xS), the counter, the size N (top of xM) and the globals; run sapAxP; pop the registers; then xM := (N / sₖ) tₖ, move sₖ from xS to xU.

Formalization Note. This is a lemma of the Lean development NLogN, a multitape-Turing-machine implementation of the Harvey–van der Hoeven $O(n\log n)$ integer multiplication algorithm, used in the proof of NLogN.FIN.theorem_1_1_nlogn : IntMul.MulTimeBound fun n => n * Real.log n. All names refer to the definition bundles IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs8 (namespace NLogN), built on the platform model Def_IntMul_MultitapeModel and the published reference Def_IntMul_HvdH_MachineRef. The machine layer: IState HS is a state of 64 item stacks; RM programs have a semantics p.run s, a definedness predicate p.ok M s and a cost p.cost M s relative to a multiplication spec M : MulSpec; zsz z is the bit length of $|z|$.