C_F
plain-language theorem explainer
The declaration supplies the numerical value of the fundamental Casimir C_F = 4/3 for three colors in SU(3) QCD. Researchers working on the two-loop running of the strong coupling alpha_s would reference this constant when assembling the beta-function coefficients b0 and b1. It is introduced as a direct real-number definition that substitutes the canonical N_c = 3 into the standard group-theory formula.
Claim. The Casimir operator for the fundamental representation of SU(3) is given by $C_F = 4/3$.
background
In the module on two-loop QCD running of alpha_s in the MS-bar scheme, the beta function coefficients are expressed using the number of colors N_c and the fundamental Casimir C_F. Here N_c is fixed to 3, and C_F is the standard value (N_c^2 - 1)/(2 N_c) evaluated at that point. This module extends the one-loop alpha_s_running to include the second coefficient b1, yielding the integrated two-loop formula for 1/alpha_s(mu). Upstream results include canonical arithmetic objects that ensure the numerical assignments remain consistent across realizations.
proof idea
The definition is a direct assignment of the real number 4/3, obtained by substituting N_c = 3 into the Casimir formula C_F = (N_c^2 - 1)/(2 N_c). No lemmas are applied; it is a one-line numerical definition.
why it matters
This constant enters the two-loop beta-function coefficient b1 = (34 N_c^2 - (10 N_c + 6 C_F) N_f)/(24 pi^2) and is re-exported for use in the alpha_s_two_loop formula. It supports the Heavy Quark closure track by providing the exact MS-bar running at two loops, connecting to the one-loop limit when b1 vanishes. The module proves positivity and monotonicity of the running coupling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.