swaps_fsp (KFG: dyadic gate atoms, dyadic gates, unit scalings, role swaps and role permuta)

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

theorem NLogN.KFG.swaps_fsp {W L : ℕ} (s : IState HS) (l0 : List ℤ) (w Z : ℕ)
    (hZ : zsz ((2 * (W * L) : ℕ) : ℤ) ≤ Z) :
    ∀ (l : List (ℕ × ℕ)), (∀ p ∈ l, p.1 < p.2 ∧ p.2 < W) →
    ∀ (e : ℕ → ℕ) (f : Fin HS → List ℤ) (zs : List GI) (y : ℕ → ℕ → ℂ),
      Enc W L e zs y → f 0 = gflat zs ++ l0 → ClP f → NLogN.KFB.GB w zs →
      Enc W L (e ∘ NLogN.KFG.swapsF l) (swapsL L l zs) (fun v => y (NLogN.KFG.swapsF l v)) ∧ NLogN.KFB.GB w (swapsL L l zs) ∧
      FSp (swapsP L l) (encK s f) (encK s (Function.update f 0 (gflat (swapsL L l zs) ++ l0)))
        (l.length * cAtom w 0 L W Z + 1)

Context. The lemma belongs to the part KFG: dyadic gate atoms, dyadic gates, unit scalings, role swaps and role permutations: All steps are pair passes (pairW) on the scaled encoding Enc.

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_Defs20.