nonAbelianVertices
plain-language theorem explainer
The definition assigns the integer 2 to the count of non-Abelian vertices, corresponding to the three-gluon and four-gluon vertices. A physicist deriving the Standard Model Feynman rules from the Recognition Science forcing chain would cite this count when verifying the five-vertex structure. It is introduced by direct assignment of the constant 2 with no computation.
Claim. The number of non-Abelian vertices is $2$.
background
Feynman diagrams arise as the perturbative expansion of the S-matrix, with each vertex a J-cost coupling event. The module identifies five canonical vertex types in the Standard Model: three-gluon, four-gluon, quark-gluon, W-fermion, and Higgs-fermion, for a configuration dimension of 5. The two non-Abelian vertices exist because SU(3) is non-Abelian, which follows from its rank equaling the spatial dimension D = 3.
proof idea
This is a one-line definition that directly assigns the constant value 2 to the non-Abelian vertex count.
why it matters
This definition supplies the non-Abelian vertex count required by the FeynmanCert structure, which also records the five-vertex total and the SU(3) rank equaling D. It is used by the totalVertices theorem to prove the sum equals 5. Within the framework it instantiates the consequence of T8 that D = 3 forces non-Abelian gauge groups such as SU(3), enabling the 3-gluon and 4-gluon vertices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.