padS_sp (KIL6: padding stages)

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

theorem NLogN.KIL.padS_sp (s : IState HS) (F : Fin HS → List ℤ) (v : Fin HS → ℕ) {M B : ℕ}
    (hM : zsz (M : ℤ) ≤ B) (hv : ∀ i ∈ regD, v i ≤ M) (x b z t : NE)
    (hx : PadE F v M x) (hb : PadE F v M b) (hz : PadE F v M z) (ht : PadE F v M t)
    {X Fa Fb Y : ℕ} (vx : x.val v = X) (vb : b.val v = Fa * Y) (vz : z.val v = (Fb - Fa) * Y)
    (vt : t.val v = X * (Fb * Y)) (hF : Fa ≤ Fb) (hF1 : 1 ≤ Fb) (hY : 1 ≤ Y)
    (xs : List ℤ) (h0 : F 0 = xs) (h15 : F 15 = []) (h20 : F 20 = []) (h21 : F 21 = [])
    (hxs : xs.length = X * (Fa * Y)) (hbd : Bnd B xs) :
    Sp (padS x b z t) (encK s (regState F v regD))
      (encK s (regState (Function.update F 0 (padL X Fa Fb Y 0 xs)) (padV v X (Fa * Y)
        ((Fb - Fa) * Y) (X * (Fb * Y))) regD))
      ((x.size + b.size + z.size + t.size + 5) * 10 ^ 7 * (B + 2) ^ 2 + cPad (X * (Fb * Y)) B)

Context. The lemma belongs to the part KIL6: padding stages: padS x b z t sets the four padding registers from NE expressions (X, F·Y, (F'-F)·Y, and the total) and runs padP; unpadS likewise runs unpadP. Their specifications on the register file (padS_sp, unpadS_sp) reduce every padding of the main program to arithmetic.

Formalization Note. This lemma belongs to the item-language (IL) layer of the integer-multiplication-kappa campaign: tape-level programs (register programs over 64 item stacks of the NLogN multitape framework, definition bundles IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs8) that implement the data-movement primitives of the OpenAI preprint Integer multiplication below $n\log n$ (field moves, row split/merge, shifts, the uniform Proposition 11 interchange, Lemma 12 with fine $O(1)$-per-element costs, Gaussian record primitives, Proposition 14 pieces) with exact list denotations from the array-model bundles IntMul_Kappa_K_Defs* and explicit cost bounds. All names refer to the definition bundles up to IntMul_Kappa_K_Defs18.