n_colors_eq
plain-language theorem explainer
The number of QCD colors equals 3 by definitional equality with the fundamental representation dimension of the color layer. Anyone assembling the high-T Standard Model g_* count cites this to pin the color multiplicity in fermionic bookkeeping. The proof is a one-line reflexivity check against the upstream color-layer definition.
Claim. The number of colors equals $3$: $N_c = 3$, where $N_c$ is the dimension of the fundamental representation of the color factor (SU(3) from the $Q_3$ gauge construction).
background
This module performs textbook high-temperature Standard Model degree-of-freedom bookkeeping: $g_* = g_b + (7/8)g_f = 106.75$, valid only for $T \gtrsim T_{\mathrm{EW}}$. The module status is explicit bookkeeping over adopted SM content, not a novel RS prediction.
RS supplies the gauge group SU(3)×SU(2)×U(1) from $Q_3$ cube automorphisms (GaugeFromCube) and the generation count $3$ from $D=3$ face pairs (ParticleGenerations). The color count itself is the fundamental-rep dimension of the color layer: n_colors is defined as that dimension. The companion constant chiralities is the left-plus-right factor $2$.
Matter representations (which fermions sit in which reps, colors per quark) remain imported SM input; only the group and generation count are RS-sourced upstream.
proof idea
One-line term proof by reflexivity (rfl). The definition n_colors := color_layer.fund_rep_dim reduces definitionally to $3$, so the equality holds by computation with no lemmas or tactics beyond the kernel's definitional equality.
why it matters
Feeds the certificate record gStarCert, which packages the exact rational $g_*$ assembly: bosonic and fermionic DOF equalities, generation count, color count, and gluon DOF. Without $N_c = 3$ pinned, the fermionic tally (quarks × colors × chiralities × particle/antiparticle × generations) cannot close to the textbook $g_f = 90$.
In the RS forcing chain this sits downstream of T8 ($D=3$) and the GaugeFromCube derivation of SU(3): the color factor is not postulated ad hoc but inherited from the cube automorphism group, and this lemma records that the fundamental dimension is three. It does not invent new physics; it locks the bookkeeping input so the certified $g_* = 427/4$ path stays fully checked in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.