gluonCount
plain-language theorem explainer
The definition computes the gluon count as the square of the color count minus one. QCD modelers deriving the Standard Model from Recognition Science cite it to recover the eight gluons of SU(3). It is a direct algebraic definition that inherits the value 3 from the sibling colorCount definition.
Claim. The gluon count $g$ is given by $g = c^2 - 1$, where $c$ denotes the number of colors.
background
In the QuantumChromodynamicsFromRS module, colorCount is defined as 3 to match the spatial dimension D from the forcing chain T8. This gluonCount definition implements the standard count of generators for the SU(3) group, given by N squared minus one for N colors. The upstream result from StandardModelGroupStructure defines an analogous gluonCount via rankSU3 squared minus one, confirming the adjoint representation dimension for the same group.
proof idea
This is a one-line definition that directly applies the arithmetic expression colorCount raised to the power two minus one.
why it matters
It supplies the gluon count used in downstream results such as gluonCount_eq_8, which asserts the value 8, color_times_gluon, and QCDCert, which bundles the color-gluon relations with the five QCD phases. This realizes the Recognition Science landmark that eight gluons arise as 3 squared minus 1 for the SU(3) structure tied to D equals 3 spatial dimensions and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.