gluonCount
plain-language theorem explainer
The definition sets the gluon count to rankSU3 squared minus one. Gauge theorists working from Recognition Science derivations cite this when counting the adjoint degrees of freedom for the SU(3) factor. It is a direct algebraic substitution of the constant rank value three into the standard formula for the dimension of the adjoint representation.
Claim. Let $N=3$ be the rank of the special unitary group $SU(N)$. The gluon count equals $N^2-1$.
background
The module derives the Standard Model gauge group $SU(3)×SU(2)×U(1)$ from the Recognition Science forcing chain, with ranks 3, 2 and 1 respectively. The rankSU3 definition fixes the first factor at three, matching the spatial dimension $D$ stated in the module documentation. The upstream gluonCount definition in QuantumChromodynamicsFromRS applies the same formula to colorCount, so this declaration specializes the count to the SM rank value.
proof idea
One-line definition that substitutes the rankSU3 constant into the adjoint-dimension expression.
why it matters
This definition supplies the value eight to the QCDCert structure, the gluonCount_eq_8 theorem, and the SMGroupCert certification. It closes the rank-to-carrier count for the color sector, consistent with the module's statement that SU(3) rank equals $D=3$. The downstream gluon_count theorem then asserts the numerical equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.