su3Rank_eq_D
plain-language theorem explainer
The equality between the SU(3) rank and spatial dimension 3 shows that non-Abelian gauge symmetries fit naturally into three-dimensional space in Recognition Science. Researchers deriving Feynman diagrams from J-cost vertices reference it to justify the triple-gluon and quartic-gluon interactions. The proof consists of a direct reflexivity step on the rank definition.
Claim. The rank of SU(3) equals the spatial dimension 3.
background
Feynman diagrams arise as the perturbative expansion of the S-matrix in Recognition Science, with each vertex corresponding to a J-cost coupling event. The module identifies five canonical vertex types for the Standard Model, matching a configuration dimension of D = 5. Non-Abelian vertices such as the 3-gluon and 4-gluon exist because the rank of SU(3) equals D, allowing non-commutativity in dimensions at least 2. The upstream result defines su3Rank as the natural number 3, with documentation stating that this value equals D = 3.
proof idea
The declaration is a one-line wrapper that applies reflexivity to the definition of su3Rank.
why it matters
This theorem supplies the su3_rank_D field required by the feynmanCert definition, which assembles the complete certification of vertex types and non-Abelian character. It fills the framework requirement that D = 3 spatial dimensions, as per the eight-tick octave and T8, forces the color group to be non-Abelian. The module documentation confirms zero sorries and zero axioms in the Lean development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.