unpMB_runs (KFUU §1b: uniform deletion of the padding)

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

theorem NLogN.KFUU.unpMB_runs {pM : Fin P} (hM : MulOK I iprog pM NLogN.KFUU.MS) {pS : Fin HS} (hpS : LS pS)
    (t : IState HS) (X Wk W1 Sk w : ℕ) (hle : Sk * W1 ≤ Wk) (ys : List ℤ)
    (hys : ys.length = X * Wk) (hb : Bnd w ys) (R : List Item) (h0 : t.G 0 = ints ys ++ R)
    {LX LV LT : List Item}
    (hX : t.G pXr = .int (X : ℤ) :: LX) (hV : t.G pV = .int (Wk : ℤ) :: .int (W1 : ℤ) :: LV)
    (hT : t.G NLogN.KFUU.tT = .int (Sk : ℤ) :: LT) :
    IRuns I iprog (unpMB pM pS) t
      (((((t.upd 0 (ints (unpPre (Sk * W1) Wk ys X) ++ R)).upd pV (.int (W1 : ℤ) :: LV)).upd
        pXr (.int ((Sk * X : ℕ) : ℤ) :: LX)).upd NLogN.KFUU.tT LT).upd pS (.int (Sk : ℤ) :: t.G pS))
      (cUMB X Wk W1 Sk w)

Context. The lemma belongs to the part KFUU §1b: uniform deletion of the padding: unpadAllU pM pS pT: ys on the padded shape T becomes extract S T 0 ys (KFU unpadAll_spec with the per-field counts computed at run time from S.reverse on pS, T.reverse on pT and |S| on nR).

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.