mass_ratio_two_loop
plain-language theorem explainer
Quark mass running between renormalization scales at two-loop accuracy in QCD is given by this closed expression. Particle physicists computing physical quark masses from high-scale anchors cite it when integrating the anomalous dimension to two loops. The definition multiplies the one-loop power-law factor by an exponential of the integrated two-loop correction involving c1, b0 and b1.
Claim. The two-loop MS-bar quark mass running ratio is $m(mu)/m(mu_0) = (alpha_s(mu)/alpha_s(mu_0))^{1/b_0(N_f)} * exp[ ((c_1(N_f)/b_0(N_f) - b_1(N_f)/[b_0(N_f)]^2) * (alpha_s(mu) - alpha_s(mu_0))/(4 pi)) ]$, where $c_1(N_f) = 67/12 - 5 N_f/18$, and $b_0(N_f)$, $b_1(N_f)$ are the one- and two-loop beta coefficients.
background
The MS-bar 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 c_0 equals 1 by definition and c_1(N_f) equals 67/12 - 5 N_f/18 for N_c=3. The beta coefficients are b_0(N_f) = (11*3 - 2 N_f)/(12 pi) and b_1(N_f) = (102 - 38 N_f/3)/(8 pi^2). The module integrates d log m / d log mu^2 = -gamma_m(alpha_s) to two loops, producing the mass ratio as the product of a leading power and a subleading exponential. It assembles the form from the imported definitions of c0, c1, mass_ratio_leading, b0 and b1.
proof idea
The definition is a direct one-line algebraic composition. It multiplies the leading-log ratio mass_ratio_leading by Real.exp of the two-loop correction factor (c1 N_f / b0 N_f - c0 * b1 N_f / (b0 N_f)^2) times (alpha_mu - alpha_mu_0)/(4 pi).
why it matters
This supplies the explicit two-loop mass running formula used to certify positivity in MassAnomalousDimensionCert and to equate the gap correction to the integrated running residual in GapEqualsRunningHypothesis. It is applied in m_c_at_MZ_pos for running the charm mass from M_Z and in QuarkSchemeReconciliation for down-type gap positivity. In the Recognition framework it provides the QCD running engine required to relate high-scale mass anchors to physical values on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.