HvdH machine lemma exp_post_cost (`expBits` as a register program)

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

theorem NLogN.exp_post_cost (n : ℕ) (u : IState HS) (L5 : List Item) (h5 : u.G 5 = .int n :: L5)
    (v30 v31 v32 v33 v34 v35 v36 v37 v38 : ℤ)
    (L30 L31 L32 L33 L34 L35 L36 L37 L38 : List Item)
    (h30 : u.G 30 = .int v30 :: L30) (h31 : u.G 31 = .int v31 :: L31)
    (h32 : u.G 32 = .int v32 :: L32) (h33 : u.G 33 = .int v33 :: L33)
    (h34 : u.G 34 = .int v34 :: L34) (h35 : u.G 35 = .int v35 :: L35)
    (h36 : u.G 36 = .int v36 :: L36) (h37 : u.G 37 = .int v37 :: L37)
    (h38 : u.G 38 = .int v38 :: L38)
    (M : ℤ) (B : ℕ) (big : ∀ z : ℤ, |z| ≤ M → zsz z ≤ B) (hnB : n + 20 ≤ B)
    (m30 : |v30| ≤ M) (m31 : |v31| ≤ M) (m32 : |v32| ≤ M) (m33 : |v33| ≤ M) (m34 : |v34| ≤ M)
    (m35 : |v35| ≤ M) (m36 : |v36| ≤ M) (m37 : |v37| ≤ M) (m38 : |v38| ≤ M)
    (m36' : |v36 + 2 ^ (n + 8)| ≤ M) (m37' : |v37 + 2 ^ (n + 8)| ≤ M)
    (hP9 : (2 : ℤ) ^ (n + 9) ≤ M) (hnM : (n : ℤ) + 9 ≤ M) :
    expPost.cost u ≤ 500 * 10 ^ 7 * (B + 4) ^ 2

Context. The lemma belongs to the part expBits as a register program: Inputs n on register 5, x on 6, y on 7; the two components of expBits n x y are pushed on registers 8 and 9. Scratch registers 30 … 39.

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