VertexType
plain-language theorem explainer
VertexType enumerates the five canonical Standard Model vertices reinterpreted as J-cost coupling events. Physicists deriving perturbative QFT from the RS forcing chain cite it to fix the vertex count at five for D = 5. The declaration is a direct inductive definition with five constructors that automatically derives Fintype, DecidableEq, and related instances.
Claim. Let $V$ be the set of vertex types consisting of the three-gluon vertex, the four-gluon vertex, the quark-gluon vertex, the W-fermion vertex, and the Higgs-fermion vertex.
background
In Recognition Science, Feynman diagrams are the perturbative expansion of the S-matrix where each vertex is a J-cost coupling event. The module sets five vertex types equal to the configuration dimension D = 5, with the three-gluon and four-gluon vertices arising because SU(3) is non-Abelian of rank 3. This rank equals D follows from the spatial dimension fixed by the unified forcing chain at T8.
proof idea
The declaration is a direct inductive definition that introduces the five constructors threeGluon, fourGluon, quarkGluon, wFermion, higgsFermion and derives the instances DecidableEq, Repr, BEq, Fintype by the deriving clause.
why it matters
VertexType supplies the enumeration required by the downstream FeynmanCert structure, which records five_vertices : Fintype.card VertexType = 5 together with su3_rank_D = 3 and non_abelian = 2. It completes the A1 QFT depth step by tying the non-Abelian gauge vertices to D = 3 from the forcing chain and the phi-ladder mass formula. The result supports the claim that Standard Model vertex content is fixed once the Recognition Composition Law and eight-tick octave are in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.