Gate classification for the complex network (task 1)

Gate classification for the complex network (task 1). Every scalar gate step of complexIface is either a dyadic atom gate gateMat W_c as (atoms Ok, h ≤ 1, coefficients ±1, targets never sources: KFG.gate_iruns applies) or a diagonal sign gate (-1 on a set of roles, 1 elsewhere: one KFG.UAtom with u = -1 per role of the set).

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

theorem NLogN.KFN.complexIface_gate_class (G : Matrix (Fin P8Lift.Wc) (Fin P8Lift.Wc) ℂ)
    (hm : P8Lift.RStep.gate G ∈ P8Lift.complexIface.net) :
    (∃ as : List KFG.Atom, (∀ a ∈ as, a.Ok P8Lift.Wc ∧ a.h ≤ 1) ∧ KFG.NoTS as ∧
        G = KFG.gateMat P8Lift.Wc as) ∨
      (∃ U : Finset (Fin P8Lift.Wc), G = Matrix.diagonal fun w => if w ∈ U then -1 else 1)

Context. The lemma belongs to the part KFN: classification of the scalar gates of the complex network (task 1).

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.