p2U_runs (KFUU §2i: phase 2 in IL)

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

theorem NLogN.KFUU.p2U_runs {pM : Fin P} (hMul : MulOK I iprog pM NLogN.KFUU.MS) {pS : Fin HS} (hpS : LS pS)
    {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)
    (zU : zsz ((2 ^ u : ℕ) : ℤ) ≤ Z)
    (t : IState HS) (R : List Item)
    (h0 : t.G 0 = ints (Dl (mzB u bs.length cz) (bgB bs) (List.range bs.length ++ [bs.length])
      (lay1 (bgB bs) bs.length 0) xs0 0) ++ R)
    {RS LN LZ LW LU L2 : List Item}
    (hpS0 : t.G pS = ints (NLogN.KFUU.zl (shP u bs)) ++ RS) (hN : t.G nR = .int (bs.length : ℤ) :: LN)
    (hZ : t.G rCZ = .int (cz : ℤ) :: LZ)
    (hW : t.G rW = .int (w : ℤ) :: LW) (hUu : t.G NLogN.KFUU.rU = .int (u : ℤ) :: LU)
    (h2 : t.G rU2 = .int ((2 ^ u : ℕ) : ℤ) :: L2) :
    IRuns I iprog (p2U pM pS eSw dS Dsc) t
      (t.upd 0 (ints (Dl (mzB u bs.length cz) (bgB bs) (List.range bs.length ++ [bs.length])
        (((lay1 (bgB bs) bs.length 0).take bs.length).reverse ++
          (lay1 (bgB bs) bs.length 0).drop bs.length) xs0 0) ++ R))
      ((bs.length + 1) * (⌈cSwV K w u (vol (shP u bs) * cr)⌉₊ + 40 * cU Z) + 30 * cU Z)

Context. The lemma belongs to the part KFUU §2i: phase 2 in IL: p2U computes vol ctB · cr (from vol (shP u bs), U^n and cz = 2 cr) and ⌊n/2⌋, then runs the ⌊n/2⌋ swaps. The main fields are reversed: the layout lay1 bg n 0 becomes rv n (n/2) (lay1 bg n 0).

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.