p1L_runs (KFUU §2c: phase 1 of the uniform reversal)

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

theorem NLogN.KFUU.p1L_runs {pM : Fin P} (hM : MulOK I iprog pM NLogN.KFUU.MS) {pS : Fin HS} (hpS : LS pS)
    (u cz : ℕ) (bs : List Bool) (hcz : 1 ≤ cz) (w : ℕ) (xs0 : List ℤ) (hx : Bnd w xs0) (Z : ℕ)
    (hVZ : zsz ((vol (shP u bs) * cz : ℕ) : ℤ) ≤ Z) (hZ2 : 2 ≤ 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 bs.length) xs0 0) ++ R)
    {RV RB RtS RS LZ LU LN : List Item}
    (hV : t.G pV = ints (sufV (shP u bs).reverse 1) ++ RV)
    (htS : t.G tS = ints (NLogN.KFUU.zl (shP u bs).reverse) ++ RtS) (hpS0 : t.G pS = RS)
    (hB : t.G NLogN.KFUU.qB = .int 1 :: RB)
    (hZ : t.G NLogN.KFUU.qZ = .int (cz : ℤ) :: LZ) (hU : t.G rU2 = .int ((2 ^ u : ℕ) : ℤ) :: LU)
    (hN : t.G nR = .int (bs.length : ℤ) :: LN) :
    IRuns I iprog (p1L pM pS) 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) xs0 0) ++ R)).upd pV RV).upd NLogN.KFUU.qB
        (.int (vol (shP u bs) : ℤ) :: RB)).upd tS RtS |>.upd pS (ints (NLogN.KFUU.zl (shP u bs)) ++ RS))
      ((bs.length + 1) * (KFU.cMv (vol (shP u bs) * cz) w + 40 * cU Z + 76 * Z + 3000))

Context. The lemma belongs to the part KFUU §2c: phase 1 of the uniform reversal: p1U pM pS (sizes S = shP u bs on pS in order, n = |bs| on nR, 2^u on rU2, cz on rCZ) moves every extra bit behind the main atoms: Dl (lay1 n) ↦ Dl (lay1 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.