desc4_sp (KIL6: the middle part)

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

theorem NLogN.KIL.desc4_sp (s : IState HS) (F : Fin HS → List ℤ) {M B : ℕ} (hM : zsz (M : ℤ) ≤ B)
    {W K R : ℕ} (hW : 1 ≤ W) (v : Fin HS → ℕ) (hv : ∀ i ∈ regD, v i ≤ M)
    (vK : v aK = K) (vR : v aQR = R) (hF23 : F 23 = []) (hWK : W ^ K ≤ R) (hRM : 2 * R ≤ M)
    (hWM : W ≤ M) :
    ∃ v', (∀ i, i ∉ [aWK, aRp] → v' i = v i) ∧ v' aWK = W ^ K ∧ v' aRp = padRows W K R ∧
      Sp (desc4 W) (encK s (regState F v regD)) (encK s (regState F v' regD))
        (100 * (K + 1) * 10 ^ 7 * (B + 2) ^ 2)

Context. The lemma belongs to the part KIL6: the middle part: When digits remain (n = e - r ≥ 1): compute W^Kp and the padded row count R' = padRows W Kp (q^r) (desc4), pad the rows (padR), run all piece calls (piecesI), and remove the row padding (unpadR). mid_run: this realises l12mid.

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.