p2L_runs (KFUU §2h: the set-up of phase 2 (volume, powers))

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

theorem NLogN.KFUU.p2L_runs {eSw : Fin P} {dS : Fin HS} {K : ℝ} (hK : SwOKU I iprog eSw dS K) (hdS : dS ≠ 0)
    {Dsc : Fin HS} (hD : Dsc = 18 ∨ Dsc = 19) (hDd : Dsc ≠ dS)
    (u w cz cr : ℕ) (bs : List Bool) (hu : 1 ≤ u) (hcz : cz = 2 * cr) (hcr : 1 ≤ cr)
    (xs0 : List ℤ) (hx : Bnd w xs0) (Z : ℕ) (hZ3 : 3 ≤ Z)
    (hVZ : zsz ((vol (shP u bs) * cz : ℕ) : ℤ) ≤ Z) (zw : zsz (w : ℤ) ≤ Z)
    (t : IState HS) (R : List Item) {LW LU L2 LA LM LB LH : List Item}
    (hW : t.G rW = .int (w : ℤ) :: LW) (hUu : t.G NLogN.KFUU.rU = .int (u : ℤ) :: LU)
    (h2 : t.G rU2 = .int ((2 ^ u : ℕ) : ℤ) :: L2)
    (hH : t.G NLogN.KFUU.rH = .int ((bs.length / 2 : ℕ) : ℤ) :: LH) :
    IRuns I iprog (p2L eSw dS Dsc) (p2St t R u cz cr bs xs0 LA LM LB 0)
      (p2St t R u cz cr bs xs0 LA LM LB (bs.length / 2))
      ((bs.length / 2 + 1) * (⌈cSwV K w u (vol (shP u bs) * cr)⌉₊ + 32 * cU Z + 3000))

Context. The lemma belongs to the part KFUU §2h: the set-up of phase 2 (volume, powers).

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.