HvdH machine lemma CR.out_cost (Cost of the key generation (namespace `NLogN.CR`))

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

theorem NLogN.CR.out_cost (s0 : IState HS) (s : List ℕ) (hs : ∀ x ∈ s, 0 < x) (Rst LP T0 LK L4 : List Item)
    (hK : s0.G kKR = .int s.length :: LK) (h4 : s0.G kK4 = .int ((4 * s.length : ℕ) : ℤ) :: L4)
    (N k : ℕ) (B : ℕ) (hB : 2 * s.prod + 4 * s.length + 1 < 2 ^ B) :
    outBody.cost (withCtr kC1 s0 N k (keySt s0 s Rst LP T0 k)) ≤
      (s.length + 1) * 210000 * (B + 2)

Context. The lemma belongs to the part Cost of the key generation (namespace NLogN.CR).

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