A role permutation as a fine IL run on the scaled encoding (scales permuted along)

A role permutation as a fine IL run on the scaled encoding (scales permuted along).

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

theorem NLogN.KFG.perm_iruns {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}
    {W m n : ℕ} (T : Butterfly.Op (Fin n)) (σ : Equiv.Perm (Fin W)) (e : ℕ → ℕ) (s : IState HS)
    (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ) (x : Fin W × (Fin m × Fin n → Fin 2) → ℂ)
    (hx : ScRep e zs x) (h0 : f 0 = gflat zs ++ l) (hC : ClP f) (wb Z : ℕ) (hb : NLogN.KFB.GB wb zs)
    (hZ : zsz ((2 * (W * 2 ^ (m * n)) : ℕ) : ℤ) ≤ Z) :
    ∃ zs', ScRep (e ∘ pf σ⁻¹) zs'
        ((P8Lift.RStep.den T (P8Lift.RStep.perm (m := m) σ)).mulVec x) ∧ NLogN.KFB.GB wb zs' ∧
      IRuns I iprog (fcode (swapsP (2 ^ (m * n)) (permSw σ))) (encK s f)
        (encK s (Function.update f 0 (gflat zs' ++ l))) (W * cAtom wb 0 (2 ^ (m * n)) W Z + 1)

Context. The lemma belongs to the part KFG: the steps gate and perm as RStep.den on the (scaled) state encoding: ScRep e zs x: role-major Gaussian array zs (role length 2^{mn}, address index aidx) encodes the state x with per-role scale 2^{-e w}: toC zs[w 2^{mn} + aidx b] = 2^{e w} x(w,b) (ScRep 0 = KFB.Rep, scRep_zero).

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.