revK (KFUU §9a: the passes on managed states)

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

theorem NLogN.KFUU.revK {pM : Fin P} (hM : 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 ℤ) (hxs : xs0.length = vol (shP u bs) * cz) (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)
    (s : IState HS) (F : Fin HS → List ℤ) (l rS rN rZ rW' rU' r2 : List ℤ) (h0 : F 0 = xs0 ++ l)
    (hpS0 : F pS = NLogN.KFUU.zl (shP u bs) ++ rS) (hN : F nR = (bs.length : ℤ) :: rN)
    (hZ : F rCZ = (cz : ℤ) :: rZ) (hW : F rW = (w : ℤ) :: rW') (hUu : F NLogN.KFUU.rU = (u : ℤ) :: rU')
    (h2 : F rU2 = ((2 ^ u : ℕ) : ℤ) :: r2) :
    IRuns I iprog (revU pM pS eSw dS Dsc) (NLogN.KIL.encK s F)
      (NLogN.KIL.encK s (Function.update F 0
        (pull (shP u bs ++ [cz]) ((shP u bs).reverse ++ [cz]) (revH bs.length) 0 xs0 ++ l)))
      (cRevU K u w cz cr bs.length Z (vol (shP u bs)))

Context. The lemma belongs to the part KFUU §9a: the passes on managed states: The pass lemmas (padAllU_runs, unpadAllU_runs, revU_runs, rotsFU_runs, rotsBU_runs) restated on managed states encK s F (data xs ++ l on stack 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.