HvdH machine lemma EX.bBody_all (The full `fwdL` / `exactConvL` programs, part 6: the body of the `B̃` )

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

theorem NLogN.EX.bBody_all (M : MulSpec) (q : Params) (kb mm Φ Bacc Q Bq Bx : ℕ) (BB : ℕ → ℕ)
    (hM : MulBnd M mm Φ) (hsl : q.s.length = q.K) (hst : ∀ i < q.K, sK q i ≤ tK q i)
    (hα : 1 ≤ q.α) (hBx : Vx q kb < 2 ^ Bx) (k : ℕ) (hk : k < q.K)
    (H : BAx q kb mm Bacc Q Bq BB k)
    (Y : List (ℤ × ℤ)) (w : IState HS) (R LS LM LC : List Item) (hg : Glob q kb w)
    (hD : w.G gD = gints (XB q Y k) ++ R) (hL : (XB q Y k).length = NB q k)
    (hLB : GB (BB k) (XB q Y k))
    (hS : w.G xS = .int (sK q k : ℤ) :: LS) (hMx : w.G xM = .int (NB q k : ℤ) :: LM)
    (hc : w.G cL = .int ((q.K : ℤ) - k) :: LC) :
    bBody.run w = (((w.upd gD (gints (XB q Y (k + 1)) ++ R)).upd xM
        (.int (NB q (k + 1) : ℤ) :: LM)).upd xU (.int (sK q k : ℤ) :: w.G xU)).upd xS LS ∧
      bBody.ok M w ∧
      bBody.cost M w ≤
        bapAxCost q.p (sK q k) (tK q k) q.α (mB q k) kb (BB k) mm Φ Bacc Q Bq + bOver q Bx ∧
      (XB q Y (k + 1)).length = NB q (k + 1) ∧ GB (BB (k + 1)) (XB q Y (k + 1))

Context. The lemma belongs to the part The full fwdL / exactConvL programs, part 6: the body of the B̃ axis loop: bBody (iteration k, s = sₖ on top of xS, N = tₖ m on top of xM): push the registers of bapAxP (layout HAx5), compute u = (s⁻¹ mod t).val onto bKS with invP, run bapAxP, pop everything, then xM := (N / t) s and 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|$.