HvdH machine lemma ST.chirpPh_spec (The recursive step, part 4: generic helpers and the first phases (name)

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

theorem NLogN.ST.chirpPh_spec (M : MulSpec) (q : Params) (he : 1 ≤ q.e) (hdh : q.dh < q.K) (t : IState HS)
    (hw : CR.ChirpRegs q t) (LP L2 L28 : List Item) (hp : t.G CR.hPp = .int q.p :: LP) (kb S : ℕ)
    (h2 : t.G 2 = .int kb :: L2) (h28 : t.G 28 = .int (S : ℤ) :: L28)
    (hkb1 : 4 * q.r ≤ 2 ^ kb) (hkb2 : q.tdims.prod ≤ 2 ^ kb) (B : ℕ) (hB : CR.ChirpB q B)
    (hpB : q.p + 1 ≤ B) (hBig : 8 * q.r + 3 * q.tdims.prod + 4 < 2 ^ B) (hkbB : kb + 2 ≤ B)
    (hSB : zsz (S : ℤ) ≤ B) :
    Spec M chirpPh t ((t.upd 1 (.int (S : ℤ) :: t.G 1)).upd 28 (gints (chirpL q) ++ t.G 28))
      (chirpCost q kb B)

Context. The lemma belongs to the part The recursive step, part 4: generic helpers and the first phases (namespace NLogN.ST).

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