HvdH machine lemma CR.crtInP_cost (Chunking, `crtIn` and `evalDigits` as register programs (namespace `NL)

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

theorem NLogN.CR.crtInP_cost (M : MulSpec) (sl : List ℕ) (h : CrtOK sl) (s : IState HS) (b L x S kb B : ℕ)
    (LX LR LL L1 L2 RK : List Item) (hS : sl.prod = S) (hkb : S ≤ 2 ^ kb)
    (hX : s.G cX = .int (x : ℤ) :: LX) (hR : s.G cRB = .int (2 ^ b) :: LR)
    (hL : s.G cLR = .int L :: LL) (h1 : s.G 1 = .int S :: L1) (h2 : s.G 2 = .int kb :: L2)
    (h3 : s.G 3 = natInts (keyL sl) ++ RK) (hLS : L ≤ S)
    (hx : x < 2 ^ (b * L)) (hbB : b ≤ B) (hSB : S < 2 ^ B) :
    crtInP.cost M s ≤ 3 * 10 ^ 6 * (kb + 1) * (S + 1) * (B + kb + 5)

Context. The lemma belongs to the part Chunking, crtIn and evalDigits as register programs (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|$.