colorCount_eq_D
plain-language theorem explainer
The declaration equates the RS-derived color count to three, matching the spatial dimension D in the QCD construction. Physicists verifying gauge group structure from the forcing chain would cite this when confirming the SU(3) color factor. The proof reduces immediately to reflexivity on the constant definition of colorCount.
Claim. The number of quark colors equals the spatial dimension: $N_c = D = 3$.
background
In the Quantum Chromodynamics from RS module, colorCount is introduced as the constant natural number 3. This choice implements the framework landmark that the number of colors equals the spatial dimension D (T8). The upstream definition supplies colorCount : ℕ := 3, which the present theorem simply records as an equality.
proof idea
The proof is a one-line wrapper that applies reflexivity (rfl) directly to the defining equation of colorCount.
why it matters
This theorem populates the color_3 field of the downstream qcdCert certificate, which collects the numerical identities (3 colors, 8 gluons, 24 product, 5 phases) required for the RS derivation of QCD. It thereby links the forcing-chain result D = 3 to the color structure and supports the module's claim of zero-sorry status.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.