A gate (list of atoms) on the encoding and as a fine run

A gate (list of atoms) on the encoding and as a fine run.

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

theorem NLogN.KFG.gate_fsp {W L : ℕ} (s : IState HS) (l : List ℤ) (Z : ℕ)
    (hZ : zsz ((2 * (W * L) : ℕ) : ℤ) ≤ Z) :
    ∀ (as : List Atom), (∀ a ∈ as, a.Ok W) → NoTS as →
    ∀ (e : ℕ → ℕ) (f : Fin HS → List ℤ) (zs : List GI) (y : ℕ → ℕ → ℂ) (w : ℕ),
      Enc W L e zs y → f 0 = gflat zs ++ l → ClP f → NLogN.KFB.GB w zs →
      Enc W L (gateE as e) (gateL as e L zs) (gateY as y) ∧ NLogN.KFB.GB (gateW as e w) (gateL as e L zs) ∧
      FSp (gateP as e L) (encK s f) (encK s (Function.update f 0 (gflat (gateL as e L zs) ++ l)))
        (cGate as e w L W Z)

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.