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

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

theorem NLogN.KFUU.unpadK {pM : Fin P} (hM : MulOK I iprog pM NLogN.KFUU.MS) {pS pT : Fin HS} (hpS : LS pS)
    (hpT : LS pT) (hST : pS ≠ pT)
    (S T : Shape) (hF : List.Forall₂ (· ≤ ·) S T) (hS : ∀ a ∈ S, 1 ≤ a) (Z : ℕ)
    (hZ : zsz ((vol T : ℕ) : ℤ) ≤ Z) (w : ℕ) (ys : List ℤ) (hys : ys.length = vol T)
    (hb : Bnd w ys) (s : IState HS) (F : Fin HS → List ℤ) (l rS rT rN : List ℤ)
    (h0 : F 0 = ys ++ l) (hpS0 : F pS = (NLogN.KFUU.zl S).reverse ++ rS) (hpT0 : F pT = (NLogN.KFUU.zl T).reverse ++ rT)
    (hN : F nR = (S.length : ℤ) :: rN) :
    IRuns I iprog (unpadAllU pM pS pT) (NLogN.KIL.encK s F)
      (NLogN.KIL.encK s (Function.update F 0 (extract S T 0 ys ++ l)))
      ((S.length + 1) * (2000 * cScan (vol T) w + 25 * cU Z))

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.