m_running
plain-language theorem explainer
The definition supplies the two-loop evolved MS-bar quark mass at scale mu given its value m_0 at reference scale mu_0. Heavy-quark phenomenology calculations cite it when converting Z-pole inputs to masses at the quark's own scale. It is realized as a direct multiplication of the reference mass by the two-loop ratio function.
Claim. The evolved mass at renormalization scale $mu$ is $m(mu) = m_0 times R(alpha_s(mu), alpha_s(mu_0), N_f)$, where $R$ denotes the two-loop mass ratio obtained by solving the renormalization-group equation for the quark-mass anomalous dimension to order $alpha_s^2$.
background
In the MS-bar scheme the quark-mass anomalous dimension gamma_m(alpha_s) governs scale dependence through d log m / d log mu^2 = -gamma_m(alpha_s). To two loops this expands as gamma_m(a) = c_0 a + c_1 a^2 + O(a^3) with a = alpha_s / pi, c_0 = 1 (universal) and c_1 = (101 N_c - 10 N_f)/24 - 5/8 C_F for N_c = 3. The module solves the RGE explicitly, producing the closed ratio m(mu)/m(mu_0) = (alpha_s(mu)/alpha_s(mu_0))^(c_0/b_0) times an exponential correction that encodes the two-loop term involving beta-function coefficients b_0 and b_1.
proof idea
One-line wrapper that multiplies the reference mass by the two-loop ratio supplied by mass_ratio_two_loop.
why it matters
This definition supplies the numerical engine called by m_b_predicted and m_c_predicted to obtain predicted MS-bar masses at the bottom and charm scales after two-loop running from Z-pole inputs. It closes the two-loop mass anomalous-dimension sector of the QCD RGE module and is recorded inside the MassAnomalousDimensionCert structure that asserts positivity and c_0 = 1. Within the Recognition Science framework it implements the two-loop solution of the mass RGE that feeds the heavy-quark mass ladder used for the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.