gluonCount_eq_8
plain-language theorem explainer
The theorem fixes the gluon count at exactly eight once the color count is set to three. Physicists verifying the Recognition Science embedding of SU(3) into the Standard Model would cite it to confirm the adjoint dimension matches the phi-ladder output. The proof is a direct decision on the arithmetic definition gluonCount := colorCount^2 - 1.
Claim. The gluon count satisfies $N_g = 8$, where $N_g = N_c^2 - 1$ and the color count $N_c$ equals the spatial dimension $D = 3$.
background
The module derives QCD properties directly from Recognition Science by setting the number of colors equal to the spatial dimension D. The definition gluonCount : ℕ := colorCount ^ 2 - 1 is the local expression of the SU(3) adjoint dimension. An upstream definition in StandardModelGroupStructure states the same count as rankSU3 ^ 2 - 1, confirming the generator count for SU(3).
proof idea
One-line wrapper that applies the decide tactic to the natural-number definition of gluonCount after colorCount has been fixed at three.
why it matters
The equality supplies the gluon_8 field inside the downstream QCD certificate qcdCert, which bundles color count, gluon count, their product, and the five QCD phases. It realizes the module claim that eight gluons arise as 3² - 1 when D = 3, closing the SU(3) generator count inside the Recognition Science derivation of the Standard Model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.