c1
plain-language theorem explainer
The two-loop coefficient in the MS-bar quark mass anomalous dimension for QCD with three colors is the explicit rational function 67/12 minus 5 N_f over 18. QCD phenomenologists who solve the renormalization-group equation for running quark masses between scales cite this closed form. The declaration is a direct algebraic definition that performs the arithmetic in real numbers with no lemmas or tactics.
Claim. The two-loop coefficient in the mass anomalous dimension is given by $c_1(N_f) = 67/12 - 5 N_f/18$, where $N_f$ denotes the number of active quark flavors.
background
The module treats the MS-bar quark mass anomalous dimension in the two-loop approximation. With $a = alpha_s / pi$ the expansion reads gamma_m(a) = c_0 a + c_1 a^2 + O(a^3), where c_0 is fixed to 1 and c_1 takes the canonical N_c = 3 value 67/12 - 5 N_f /18. The resulting running-mass ratio between scales appears in the two-loop solution that multiplies the leading (alpha_s(mu)/alpha_s(mu_0)) power by a subleading correction factor R.
proof idea
The declaration is a direct definition that evaluates the rational expression 67/12 - 5*(N_f : Real)/18. No upstream lemmas are invoked; the four depends_on edges supply only the unit elements required for the integer and rational literals inside the arithmetic.
why it matters
The coefficient supplies the explicit two-loop term required by the running-mass formula that is referenced from JCostPerturbation and ModalGeometry. It therefore links the Recognition Science phi-ladder mass formula to standard QCD renormalization-group evolution. The module documentation records zero sorrys, thereby closing the two-loop RGE scaffolding for the mass anomalous dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.