mass_ratio_leading
plain-language theorem explainer
The leading-logarithmic quark mass running ratio between renormalization scales mu and mu_0, expressed as the ratio of strong couplings raised to c0 over b0(N_f). QCD phenomenologists cite this when evolving MS-bar masses across scales at one-loop accuracy. The definition is a direct transcription of the integrated renormalization group equation using the universal coefficient c0 equal to one.
Claim. The leading-log mass ratio is defined by $m(mu)/m(mu_0) = (alpha_s(mu)/alpha_s(mu_0))^{c_0 / b_0(N_f)}$ where $c_0 = 1$ and $b_0(N_f) = (11 N_c - 2 N_f)/(12 pi)$.
background
In the MS-bar scheme the quark mass anomalous dimension expands as gamma_m(a) = c_0 a + c_1 a^2 + O(a^3) with a = alpha_s / pi. The coefficient c0 is the universal constant 1. The one-loop beta coefficient is b0(N_f) = (11 N_c - 2 N_f)/(12 pi) with N_c = 3. The module solves the renormalization group equation d log m / d log mu^2 = - gamma_m(alpha_s) to obtain the leading power-law running between scales.
proof idea
Direct definition via the real power function applied to the ratio of couplings with exponent c0 divided by b0(N_f). It references the sibling definition c0 and the imported b0 from TwoLoopAlphaS.
why it matters
Supplies the leading term inside the two-loop mass ratio definition mass_ratio_two_loop and the positivity theorem mass_ratio_leading_pos. It also anchors the normalization case mass_ratio_leading_at_anchor. The expression implements the one-loop accurate part of the mass running formula stated in the module documentation, linking the anomalous dimension directly to the alpha_s beta function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.