HvdH machine lemma EX.bPhase_all (The full `fwdL` / `exactConvL` programs, part 8: the two axis phases a)

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

theorem NLogN.EX.bPhase_all (M : MulSpec) (q : Params) (kb mm Φ Bacc Q Bq Bx CB : ℕ) (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) (H : ∀ k < q.K, BAx q kb mm Bacc Q Bq BB k)
    (hCB : ∀ k < q.K,
      bapAxCost q.p (sK q k) (tK q k) q.α (mB q k) kb (BB k) mm Φ Bacc Q Bq ≤ CB)
    (Y : List (ℤ × ℤ)) (w : IState HS) (R RSt LN : List Item) (hg : Glob q kb w)
    (hD : w.G gD = gints Y ++ R) (hL : Y.length = NLogN.EX.TT q) (hLB : GB (BB 0) Y)
    (hS : w.G xS = ints (NLogN.EX.sl q) ++ RSt) (hPN : w.G gPN = .int (NLogN.EX.TT q : ℤ) :: LN) :
    bPhase.run w = w.upd gD (gints (tensorGo (fwdAxB q) q.tdims Y) ++ R) ∧ bPhase.ok M w ∧
      bPhase.cost M w ≤ bLoopCost q CB Bx + phOver q.K Bx ∧
      (tensorGo (fwdAxB q) q.tdims Y).length = q.S ∧
      GB (BB q.K) (tensorGo (fwdAxB q) q.tdims Y)

Context. The lemma belongs to the part The full fwdL / exactConvL programs, part 8: the two axis phases and fwdLP: A phase pushes the initial array size on xM, runs the axis loop, pops xM and moves q.s back from xU to xS; it changes nothing but gD. fwdLP fw = S̃ phase; ftlP fw; B̃ phase computes Ref.fwdL.

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|$.