feynmanCert
plain-language theorem explainer
feynmanCert defines a concrete certificate asserting five vertex types, SU(3) rank equal to three, and two non-Abelian vertices in the Recognition Science derivation of Feynman diagrams. Researchers reconstructing the Standard Model perturbative expansion from the J-cost functional equation would cite this record. The definition assembles the structure by direct assignment from vertex cardinality and rank theorems, with reflexivity for the final field.
Claim. The Feynman certificate is the structure satisfying $Fintype.card(VertexType)=5$, $su3Rank=3$, and $nonAbelianVertices=2$.
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 identifies five canonical vertex types (3-gluon, 4-gluon, quark-gluon, W-fermion, Higgs-fermion) matching configuration dimension D=5, with the two non-Abelian vertices (3-gluon and 4-gluon) arising because SU(3) rank equals spatial dimension D=3 and non-commutativity holds for D greater than or equal to 2. The FeynmanCert structure packages these three properties as a single record. Upstream, vertexTypeCount establishes the cardinality equals 5 by decision, while su3Rank_eq_D establishes the rank equals 3 by reflexivity.
proof idea
The definition constructs the FeynmanCert record by assigning five_vertices to vertexTypeCount, su3_rank_D to su3Rank_eq_D, and non_abelian to reflexivity.
why it matters
This definition supplies the explicit certificate that Recognition Science reproduces the five vertex types and non-Abelian structure of Standard Model Feynman diagrams, with SU(3) non-Abelian precisely because its rank matches D=3 from the eight-tick octave and T8. It closes the local construction in the FeynmanDiagramsFromRS module, confirming that non-Abelian vertices emerge from the framework without additional assumptions. No downstream theorems are listed, leaving open whether this certificate feeds into a full S-matrix derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.