cost_final (KFZ CostR: the chirp procedure cost against `cLineU`)

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

theorem NLogN.KFZ.cost_final (C18 : ℝ) (hC18 : 0 ≤ C18) (A18 c18 : ℕ)
    (hc : (c18 : ℝ) ≤ C18 * (((tsN n).prod * IntMul.OpenAI.Glue.rP n * (pP n + 3) : ℕ) : ℝ) *
      Ncost (6 * (lg n : ℝ)) (IntMul.OpenAI.Glue.dP n) (KP n) (ℓP n) (αP n) *
      (Real.log (6 * (lg n : ℝ)) + 1) ^ A18) :
    ((c18 + NLogN.KFZ.cBody (NLogN.KFZ.BN n) (NLogN.KFZ.BN n) (bP n) (desc18 (pP n) (ℓP n) (KP n) (tsN n)).length (pP n) (NLogN.KFZ.hN n)
      D (σN n) (sBD n D) (tBD n D) + 2 : ℕ) : ℝ) ≤ (2 * C18 + Kc) * cLineU n (A18 + 2)

Context. The lemma belongs to the part KFZ CostR: the chirp procedure cost against cLineU.

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.