n_colors
plain-language theorem explainer
The number of colors is defined as the fundamental-representation dimension of the SU(3) color gauge layer extracted from Q₃, which is 3. Anyone assembling Standard Model relativistic DOF (quarks per generation, g_★ bookkeeping) cites this alias. The body is a one-line definition pointing at the upstream GaugeLayer record.
Claim. Let $N_c$ be the number of colors. By definition $N_c$ equals the dimension of the fundamental representation of the SU(3) color gauge layer coming from $Q_3$, so $N_c = 3$.
background
The module RelativisticDOF performs textbook high-temperature Standard Model bookkeeping for $g_\star = g_b + (7/8)g_f = 106.75$, valid only for $T \gtrsim T_{\mathrm{EW}}$. Status is bookkeeping over adopted SM content, not a novel RS prediction.
RS supplies the gauge group SU(3)×SU(2)×U(1) from $Q_3$ automorphisms (GaugeFromCube) and the generation count $3 = \mathrm{face_pairs}(3)$ from $D=3$. The color layer is the GaugeLayer record named "SU(3) color" with fundamental-representation dimension 3 and discrete order 6. Matter representation assignments (which fermions sit in which reps, colors per quark) remain imported SM input.
This definition simply names that fundamental dimension so downstream DOF products can write $N_c$ instead of reaching into the layer record.
proof idea
Pure definition: one-line abbreviation equating the natural-number constant to color_layer.fund_rep_dim. No tactics, no lemmas. The numerical content 3 is fixed in the upstream GaugeLayer constructor for the color layer; the companion equality theorem is definitional reflexivity.
why it matters
Pins the color factor in the SM fermionic count that feeds $g_\star$. Downstream, quark DOF per generation is $2$ flavors × $N_c$ × $2$ chiralities × $2$ (particle/antiparticle) = 24; the certificate structure GStarCert records $N_c = 3$ alongside bosonic 28, fermionic 90, and three generations; fermionic_traces_to_Q3 packages the equalities that every fermionic DOF traces to $Q_3$ structure (generations from face pairs, colors from the color layer, total $g_f = 90$).
Framework landmark: the SU(3) factor itself is the RS-derived gauge layer from cube/Q₃ automorphisms (GaugeFromCube), while the use here is honest bookkeeping. Closes no open prediction; it is the named handle for the imported-but-RS-sourced color dimension inside the $g_\star = 106.75$ assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.