color_gluon_is_b3half
plain-language theorem explainer
The product of color count and gluon count equals 24 in the Recognition Science derivation of QCD. Physicists confirming the SU(3) embedding of the Standard Model cite this arithmetic identity. The proof is a one-line decision procedure that evaluates the equality after substituting the definitions colorCount := 3 and gluonCount := 3 squared minus 1.
Claim. Let $c = 3$ be the number of colors and $g = c^2 - 1$ the number of gluons. Then $c g = 24$.
background
In the Quantum Chromodynamics from RS module, colorCount is defined as the constant 3, matching the spatial dimension D. gluonCount is defined as colorCount squared minus 1, which yields 8 and aligns with the SU(3) generator count. A parallel definition appears in the Standard Model group structure module, stating gluon count equals rank squared minus 1 for rank 3.
proof idea
The proof applies the decide tactic, which automatically confirms the numerical equality 3 times (3 squared minus 1) equals 24 after unfolding the two upstream definitions.
why it matters
This identity supplies the basic count check for the QCD embedding, confirming 3 colors times 8 gluons equals 24 and matching the module note that this equals |B3|/2. It supports sibling results on QCDPhase and qcdCert. In the framework it instantiates T8 (D equals 3) together with the eight-tick octave generator count for SU(3).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.