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

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

theorem NLogN.KFUU.p2St_zero (t : IState HS) (R : List Item) (u cz cr : ℕ) (bs : List Bool) (xs0 : List ℤ)
    (LA LM LB : List Item) :
    p2St t R u cz cr bs xs0 LA LM LB 0 =
      (((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 rA (.int 1 :: LA)).upd NLogN.KFUU.rM
        (.int (((2 ^ u) ^ bs.length : ℕ) : ℤ) :: LM)).upd NLogN.KFUU.rB
        (.int ((vol (ctB u cz bs) * cr : ℕ) : ℤ) :: LB)

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.