padOut_all (KFY 3: generic pieces of the line passes)

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

theorem NLogN.KFY.padOut_all {Pre : List (ℤ × ℤ) → Prop} {f : List (ℤ × ℤ) → List (ℤ × ℤ)} {C : ℕ}
    (sl : LProg M Ctx Pre f C) (K rS rT : Fin HS) (s t Q : ℕ) (hst : s ≤ t)
    (hOK : sl.O ≠ K) (hK56 : K.val < 56) (hS56 : rS.val < 56) (hT56 : rT.val < 56)
    (hQ : zsz ((2 * t : ℕ) : ℤ) ≤ Q) (hstab : Stab Ctx [sl.O])
    (hCS : ∀ st, Ctx st → ∃ L, st.G rS = .int (s : ℤ) :: L)
    (hCT : ∀ st, Ctx st → ∃ L, st.G rT = .int (t : ℤ) :: L)
    (st : IState HS) (x : List (ℤ × ℤ)) (R : List Item) (hC : Ctx st)
    (hx : Pre x) (hI : st.G sl.I = gints x ++ R) :
    (padOutP sl.O K rS rT sl.p).run st =
        (st.upd sl.I R).upd sl.O (gints (f x ++ List.replicate (t - s) (0, 0)) ++ st.G sl.O) ∧
      (padOutP sl.O K rS rT sl.p).ok M st ∧
      (padOutP sl.O K rS rT sl.p).cost M st ≤ C + 100000 * (t + 1) * (Q + 2)

Context. The lemma belongs to the part KFY 3: generic pieces of the line passes.

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.