color_times_gluon
plain-language theorem explainer
The product of the number of colors and the number of gluons equals 24 in the RS-derived QCD structure. A physicist assembling the Standard Model group factors within Recognition Science would cite this equality when building the QCD certificate. The proof is a one-line decision procedure that evaluates the constant definitions of three colors and eight gluons.
Claim. The product of the number of quark colors and the number of gluons satisfies $3 times 8 = 24$.
background
In the Quantum Chromodynamics from RS module, the number of colors is fixed at the spatial dimension D from the forcing chain. colorCount is the constant natural number 3. gluonCount is defined as the square of the color count minus one, which evaluates to 8. This matches the upstream definition in StandardModelGroupStructure where gluonCount equals the square of the SU(3) rank minus one, stated as gluon count = N squared minus 1 equals 3 squared minus 1 equals 8 for SU(3). The module sets five QCD phases equal to configDim D equals 5 and notes the product 24 equals the absolute value of B sub 3 over 2.
proof idea
The declaration is a one-line wrapper that applies the decide tactic to evaluate the arithmetic product of the two natural-number definitions.
why it matters
This theorem supplies the product_24 field inside the qcdCert definition that certifies the full QCD structure, including the five phases. It directly connects the forcing-chain result D equals 3 (T8) to the SU(3) adjoint dimension of 8 gluons. The module documentation records that all such equalities hold by decide with zero sorry or axiom, closing one arithmetic link in the RS-to-QCD derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.