HvdH machine lemma CR.crtOutP_cost (`crtOut` as a register program (namespace `NLogN.CR`))

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

theorem NLogN.CR.crtOutP_cost (sl : List ℕ) (h : CrtOK sl) (s : IState HS) (w : List ℤ) (S M kb : ℕ)
    (Rest L1 L2 RK LM : List Item) (hS : sl.prod = S) (hw : w.length = S) (hM : M ≤ S)
    (hkb : S ≤ 2 ^ kb)
    (h0 : s.G 0 = ints w ++ Rest) (h1 : s.G 1 = .int S :: L1) (h2 : s.G 2 = .int kb :: L2)
    (h3 : s.G 3 = natInts (keyL sl) ++ RK) (hm : s.G cMR = .int M :: LM)
    (B : ℕ) (hBw : Bnd B w) (hSB : S < 2 ^ B) :
    crtOutP.cost s ≤ 10 ^ 7 * (kb + 1) * (S + 1) * (B + kb + 5)

Context. The lemma belongs to the part crtOut as a register program (namespace NLogN.CR): Input: w (length S = ∏ sᵢ) on stack 0, S on 1, kb (S ≤ 2^kb) on 2, the keys natInts (keyL s) on 3, M ≤ S on cMR. Output: crtOut s M w on 0; all else restored.

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