HvdH machine lemma scaleZP_top (`twD` as a register program)

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

theorem NLogN.scaleZP_top (s : IState HS) (h10 : s.IsInt 10) (h10' : 0 ≤ s.top 10)
    (h11 : s.IsInt 11) (h11' : 0 ≤ s.top 11) (h12 : s.IsInt 12) (h13 : s.IsInt 13)
    (h14 : s.IsInt 14) (h14' : 0 ≤ s.top 14) (hx : |s.top 12| < 2 ^ (s.top 14).toNat)
    (hy : |s.top 13| < 2 ^ (s.top 14).toNat) :
    scaleZP.ok s ∧ scaleZP.run s = (s.upd 15 (.int (scaleZ (s.top 10).toNat (s.top 11).toNat
      (s.top 12, s.top 13)).1 :: s.G 15)).upd 16 (.int (scaleZ (s.top 10).toNat (s.top 11).toNat
      (s.top 12, s.top 13)).2 :: s.G 16) ∧
    scaleZP.cost s ≤ scaleCost (s.top 10).toNat (s.top 11).toNat (s.top 14).toNat

Context. The lemma belongs to the part twD as a register program: twDP: inputs p on 28, n on 29, j on 53; pushes (twD p n j).1 on 15 and (twD p n j).2 on 16. It runs twiddleP and then scaleZP with k = 0 and the bit bound twBz p (an upper bound for the size of the twiddle factors). Uses (pushed and popped) registers 10 … 14, 17 … 19, 41 … 44, 51, 52 and those of twiddleP.

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