HvdH machine lemma AX.tmpQ_all (One resampling axis, part 7: derived scalars and table removal for the)

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

theorem NLogN.AX.tmpQ_all (e s α B : ℕ) (st : IState HS) (hB1 : 2 * e + 2 < 2 ^ B) (hB2 : s ^ 2 < 2 ^ B)
    (hB3 : 2 * α ^ 2 + 2 < 2 ^ B) (st' : IState HS)
    (h1 : st'.G xE = .int (e : ℤ) :: st.G xE) (h2 : st'.G xK = .int ((s ^ 2 : ℕ) : ℤ) :: st.G xK)
    (h3 : st'.G xG = .int ((2 * α ^ 2 - 2 : ℕ) : ℤ) :: st.G xG) :
    tmpQ.ok st' ∧ tmpQ.run st' = ((st'.upd xG (st.G xG)).upd xK (st.G xK)).upd xE (st.G xE) ∧
      tmpQ.cost st' ≤ 6 * B + 6

Context. The lemma belongs to the part One resampling axis, part 7: derived scalars and table removal for the B̃ axis.

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