M_runs (KFZ Call: the Prop 18 call inside the chirp procedure)

The following holds (Lean statement, in the scope of module Solutions.KFZCall):

theorem NLogN.KFZ.M_runs (j : Fin (7 + E)) (d18 : Fin HS) (hd0 : d18 ≠ 0) {n : ℕ} (hn : IntMul.OpenAI.Glue.n0 ≤ n)
    {p h d σ K B : ℕ} (hB : RB p h d σ K B) (hd : d = IntMul.OpenAI.Glue.dP n) (hdp : d - σ = dpN n)
    (hr : 2 ^ (h + 1) = IntMul.OpenAI.Glue.rP n) (hK : K = KP n) (hl : h + 1 = ℓP n) (hb : p / 6 = bP n)
    (hp : p = pP n) (Bd : ℕ) (hBd : ∀ x ∈ desc18 (pP n) (ℓP n) (KP n) (tsN n), zsz x ≤ Bd)
    (s : IState HS) (G : Fin HS → List ℤ) (hR : Regs G p h d σ K) (ZF ZG : List GI) (l : List ℤ)
    (h0 : G 0 = gflat ZF ++ gflat ZG ++ l) (hX : G (X18 d18) = [])
    (zh : List GI) (c : ℕ)
    (hcall : IRuns I iprog (.call j)
      (NLogN.KIL.encK (bgS s G d18 l) (NLogN.KFZ.fC d18 (gflat ZF ++ gflat ZG ++ [])
        (desc18 (pP n) (ℓP n) (KP n) (tsN n))))
      (NLogN.KIL.encK (bgS s G d18 l) (Function.update (NLogN.KFZ.fC d18 (gflat ZF ++ gflat ZG ++ [])
        (desc18 (pP n) (ℓP n) (KP n) (tsN n))) 0 (gflat zh ++ []))) c) :
    IRuns I iprog (Mcall j d18) (NLogN.KIL.encK s G) (NLogN.KIL.encK s (Function.update G 0 (gflat zh ++ l)))
      (c + cM B Bd (bP n) (desc18 (pP n) (ℓP n) (KP n) (tsN n)).length)

Context. The lemma belongs to the part KFZ Call: the Prop 18 call inside the chirp procedure.

Formalization Note. This lemma belongs to layer 5 of the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below $n\log n$: the uniform item-language machine (register programs over the NLogN multitape framework) assembling the Proposition 14 / Lemma 13 / Proposition 18 pieces, the resampling and chirp stages and the cost recurrences into one fixed machine, culminating in NLogN.KFTop.kappa_bound : IntMul.KappaBound (1 / 2 ^ 182) (the bound of Def_IntMul_MultitapeModel). All names refer to the definition bundles up to IntMul_Kappa_K_Defs33.