body_runs (KFZ Full: the whole chirp procedure body)

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

theorem NLogN.KFZ.body_runs (j : Fin (7 + E)) (d18 : Fin HS) (hd0 : d18 ≠ 0) {n : ℕ} (hn : IntMul.OpenAI.Glue.n0 ≤ n)
    {D p h σ K α B : ℕ} (hB : RB p h (D + 1) σ K B) (hD : D + 1 = IntMul.OpenAI.Glue.dP n)
    (hdp : D + 1 - σ = 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)
    (sv t : Fin (D + 1) → ℕ) [∀ i, NeZero (t i)] (hst : ∀ i, sv i ≤ t i) (htp : ∀ i, 0 < t i)
    (hT : ∀ i, t i ≤ 2 ^ (h + 1)) (htl : t (Fin.last D) = 2 ^ (h + 1))
    (hprod : ∏ i, t i = 2 ^ ((D + 1) * h + σ))
    (hM : 2 ^ ((D + 1) * h + σ - (h + 1)) = ∏ i : Fin D, t i.castSucc)
    (bs ss : List ℕ) (hbl : bs.length = D + 1) (hsl : ss.length = D + 1) (hb1 : ∀ b ∈ bs, b ≤ 1)
    (hstl : ∀ (i : ℕ) (hi : i < D + 1), ss[i]'(by omega) ≤ 2 ^ (h + bs[i]'(by omega)))
    (hσ : bs.sum = σ) (hsB : NLogN.KFZ.eS h bs (D + 1) + h + 6 ≤ B) (hdB : D + 1 + 2 ≤ B)
    (hKB : zsz (K : ℤ) ≤ B) (hpB : zsz (p : ℤ) ≤ B) (hαB : zsz (α : ℤ) ≤ B)
    (hdesc : descA 1 (axD h bs ss) ++ [(2 * 2 ^ NLogN.KFZ.eS h bs (D + 1) : ℤ)] = descT sv t)
    (f : Fin HS → List ℤ) (hf : EmptyEx f)
    (hc : f NLogN.KFZ.cS = (K : ℤ) :: (p : ℤ) :: (α : ℤ) :: (h : ℤ) :: ((D + 1 : ℕ) : ℤ) ::
      (NLogN.KFZ.zl bs ++ NLogN.KFZ.zl ss))
    (xs : List GI) (l : List ℤ) (h0 : f 0 = gflat xs ++ l) (hxs : xs.length = ∏ i, t i)
    (gx : NLogN.KFB.GB (p + 2) xs) (zh : List GI) (hzh : zh.length = ∏ i, t i) (gh : NLogN.KFB.GB (p + 2) zh)
    (gU : NLogN.KFB.GB (p + 2) (List.zipWith (gmulT p) xs (aLz p h D sv t)))
    (gG : NLogN.KFB.GB (p + 2) (zGz p h D sv t xs)) (gF : NLogN.KFB.GB (p + 2) (zFz p h D sv t))
    (gV : NLogN.KFB.GB (p + 2) (List.zipWith (gmulT p) zh (iLz p h D t))) (c18 : ℕ)
    (hcall : IRuns I (kTable ext) (.call j)
      (NLogN.KIL.encK (bgS s (preM (FC f p h D σ K sv t (gflat xs ++ l)) (zFz p h D sv t)
          (zGz p h D sv t xs) l) d18 l)
        (NLogN.KFZ.fC d18 (gflat (zFz p h D sv t) ++ gflat (zGz p h D sv t xs) ++ [])
          (desc18 (pP n) (ℓP n) (KP n) (tsN n))))
      (NLogN.KIL.encK (bgS s (preM (FC f p h D σ K sv t (gflat xs ++ l)) (zFz p h D sv t)
          (zGz p h D sv t xs) l) d18 l)
        (Function.update (NLogN.KFZ.fC d18 (gflat (zFz p h D sv t) ++ gflat (zGz p h D sv t xs) ++ [])
          (desc18 (pP n) (ℓP n) (KP n) (tsN n))) 0 (gflat zh ++ []))) c18) :
    IRuns I (kTable ext) (body j d18) (NLogN.KIL.encK s f)
      (NLogN.KIL.encK s (Function.update f 0 (gflat (yz p h D sv t zh) ++ l)))
      (c18 + NLogN.KFZ.cBody B Bd (bP n) (desc18 (pP n) (ℓP n) (KP n) (tsN n)).length p h D σ sv t)

Context. The lemma belongs to the part KFZ Full: the whole chirp procedure body: body j d18 = setupP; T1; …; T7; wP setC (PP j d18); popsL regL.

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.