padP_fsp (KFE: fine padding loops)

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

theorem NLogN.KFE.padP_fsp (s : IState HS) (f : Fin HS → List ℤ) {X F F' Y : ℕ} (xs rest : List ℤ)
    (hF : F ≤ F') (hF1 : 1 ≤ F') (hY : 1 ≤ Y)
    (hxs : xs.length = X * (F * Y)) (Bb : ℕ) (hb : Bnd 1 xs)
    (hV : zsz ((X * (F' * Y) : ℕ) : ℤ) ≤ Bb)
    (h0 : f 0 = xs ++ rest) (h15 : f 15 = []) (h20 : f 20 = []) (h21 : f 21 = [])
    {L1 L2 L3 L4 : List Item}
    (r1 : (encK s f).G pX = .int (X : ℤ) :: L1) (r2 : (encK s f).G pB = .int ((F * Y : ℕ) : ℤ) :: L2)
    (r3 : (encK s f).G pZ = .int (((F' - F) * Y : ℕ) : ℤ) :: L3)
    (r4 : (encK s f).G pT = .int ((X * (F' * Y) : ℕ) : ℤ) :: L4) :
    FSp padP (encK s f) (encK s (Function.update f 0 (KIL.padL X F F' Y 0 xs ++ rest)))
      (cPadF (X * (F' * Y)) Bb)

Context. The lemma belongs to the part KFE: fine padding loops: padP / unpadP (KIL6Pad) run through KFD.fcode: every counted loop is a unary loop, so the per-element cost is O(1) for bit data and the per-block loop overhead is O(zsz (F'·Y)), bounded by the block length. Result: fine cost cPadF V Bb = 2000 (Bb + 2) + 20000 V (V the padded volume) in place of cPad V Bb = 10^5 (V+1)(Bb+2).

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.