The real cost bound from the unit bound

The real cost bound from the unit bound.

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

theorem NLogN.KFW.ctot_real {Kc : ℝ} (hKc : 0 ≤ Kc) {K S r P D w Z : ℕ} (hS : 1 ≤ S) (hP : 1 ≤ P)
    (hD : 1 ≤ D) (hr : 1 ≤ r) (hZr : Z + 32 ≤ r)
    (hwZ : w + KFM.EwB NLogN.KFW.A0 D + 2 < 2 ^ Z) (hK : 1 ≤ K) :
    (cTot Kc K S r (w + KFM.EwB NLogN.KFW.A0 D) P D (Nat.log mC D) (q0f D (Nat.log mC D))
      (padB (P * 2 ^ (K * q0f D (Nat.log mC D))) (P8Lift.Wc ^ Nat.log mC D)) Z (Z + 30) (Z + 5) w : ℝ) ≤
      Mb0 * (coefF (18 * Kc + 18) K D * ((P * 2 ^ (K * D) * S : ℕ) : ℝ) *
        (Xf r (KFR.PsiR r Z) (w + KFM.EwB NLogN.KFW.A0 D) : ℝ))

Context. The lemma belongs to the part KFW C-layer 21: the entry procedure with its closed cost.

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.