vertexTypeCount
plain-language theorem explainer
The declaration proves that the inductive type of vertex types in the Recognition Science model of Feynman diagrams has exactly five elements. A researcher deriving quantum field theory from the J-cost functional equation would reference this to match the five canonical Standard Model vertices. The proof proceeds by a single decision tactic that computes the cardinality directly from the inductive definition.
Claim. The set of vertex types in the Recognition Science derivation of Feynman diagrams has finite cardinality 5, consisting of the three-gluon vertex, four-gluon vertex, quark-gluon vertex, W-fermion vertex, and Higgs-fermion vertex.
background
In the module on Feynman diagrams from Recognition Science, diagrams arise as the perturbative expansion of the S-matrix, with each vertex corresponding to a J-cost coupling event. The five vertex types are defined inductively as three-gluon, four-gluon, quark-gluon, W-fermion, and Higgs-fermion, matching the configuration dimension D equal to 5. This count relies on the non-Abelian nature of SU(3), whose rank equals the spatial dimension D=3 as established in the forcing chain.
proof idea
The proof is a one-line application of the decide tactic. This tactic exhaustively enumerates the five constructors of the inductive type of vertex types and confirms that its Fintype instance has cardinality exactly 5.
why it matters
This result supplies the five_vertices field in the Feynman certification definition, which certifies the overall structure of Feynman diagrams in the Recognition Science framework. It directly supports the module claim that five vertex types arise because SU(3) is non-Abelian with rank equal to D=3. The declaration closes the enumeration step in the A1 QFT depth, linking the phi-ladder and eight-tick octave to perturbative expansions without introducing additional axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.