A role permutation

A role permutation.

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

theorem NLogN.KFG.perm_fsp {W L : ℕ} (σ : Equiv.Perm (Fin W)) (s : IState HS) (l0 : List ℤ) (w Z : ℕ)
    (hZ : zsz ((2 * (W * L) : ℕ) : ℤ) ≤ Z) (e : ℕ → ℕ) (f : Fin HS → List ℤ) (zs : List GI)
    (y : ℕ → ℕ → ℂ) (hx : Enc W L e zs y) (h0 : f 0 = gflat zs ++ l0) (hC : ClP f) (hb : NLogN.KFB.GB w zs) :
    Enc W L (e ∘ pf σ⁻¹) (swapsL L (permSw σ) zs) (fun v => y (pf σ⁻¹ v)) ∧
      NLogN.KFB.GB w (swapsL L (permSw σ) zs) ∧
      FSp (swapsP L (permSw σ)) (encK s f)
        (encK s (Function.update f 0 (gflat (swapsL L (permSw σ) zs) ++ l0)))
        (W * 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_Defs18.