swapsF_runs (KFE: fine binary embedding / extraction and fine high-digit swaps)

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

theorem NLogN.KFE.swapsF_runs {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp} (s : IState HS) (f : Fin HS → List ℤ) (Pre G Suf : Shape) {q e r : ℕ}
    (xs rest : List ℤ) (hq : 2 ≤ q) (hP : 1 ≤ vol Pre) (hG : 1 ≤ vol G) (hS : 1 ≤ vol Suf)
    (hre : r ≤ e) (hxs : xs.length = vol (qShape Pre G Suf q e)) (Bb : ℕ) (hb : Bnd 1 xs) (hB1 : 1 ≤ Bb)
    (hV : zsz ((vol (qShape Pre G Suf q e) : ℕ) : ℤ) ≤ Bb)
    {lP lG lS l1 l2 lR : List ℤ}
    (h0 : f 0 = xs ++ rest) (h24 : f 24 = []) (hfP : f kP = (vol Pre : ℤ) :: lP)
    (hfG : f kG = (vol G : ℤ) :: lG) (hfS : f NLogN.KIL.kS = (vol Suf : ℤ) :: lS)
    (hfQt : f kQt = ((q ^ 0 : ℕ) : ℤ) :: l1) (hfQr : f kQr = ((q ^ (e - 0) / q : ℕ) : ℤ) :: l2)
    (hfR : f kR = (r : ℤ) :: lR) :
    IRuns I iprog (NLogN.KFE.swapsF q) (encK s f)
      (encK s (swF f (qShape Pre G Suf q e) Pre.length (Pre.length + e + G.length) q e xs rest
        l1 l2 r))
      ((r + 1) * (cSw1F q (vol (qShape Pre G Suf q e)) Bb + 10 ^ 4 * (Bb + 2)))

Context. The lemma belongs to the part KFE: fine binary embedding / extraction and fine high-digit swaps.

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.