N_c
plain-language theorem explainer
Number of colors N_c is fixed at three for the QCD gauge group. Researchers computing the one-loop beta function for strong coupling running cite this value to establish asymptotic freedom for N_f ≤ 16. The assignment is a direct constant definition with no computational steps or lemmas required.
Claim. The number of colors satisfies $N_c = 3$.
background
The AlphaRunning module implements one-loop renormalization group flow of the strong coupling α_s, starting from the RS-native value 2/17 at the Z-boson mass. The beta coefficient is defined as b_0 = (11 N_c - 2 N_f)/(12 π) and remains positive for N_f ≤ 16, which encodes asymptotic freedom. The upstream definition in TwoLoopAlphaS supplies the identical constant and notes the associated Casimir C_F = (N_c² - 1)/(2 N_c) = 4/3.
proof idea
Direct definition that assigns the natural number 3 to N_c. No lemmas or tactics are applied.
why it matters
This constant is the input to beta0, beta0_pos, and beta0_at_Z that quantify the positive beta function and asymptotic freedom. It also appears in three_colors_from_D3, which resolves P-007 by showing D = 3 forces exactly three color charges. The choice aligns with the T8 forcing step that sets spatial dimension to three in the unified chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.