running_mass
plain-language theorem explainer
running_mass supplies the leading-order QCD running mass at a target scale from a reference mass via the coupling ratio raised to the mass evolution exponent. Particle physicists tracking quark masses under RS renormalization group flow cite it for scale dependence in asymptotic freedom calculations. It is a direct algebraic definition multiplying the reference mass by the powered alpha_s ratio.
Claim. $m(m_2) = m(m_1) (α_s(m_2)/α_s(m_1))^{γ_0/(2b_0(n_f))}$ where the exponent is the mass anomalous dimension divided by twice the one-loop QCD beta coefficient for $n_f$ active flavors.
background
The module derives renormalization group flow from the RS φ-ladder, with the anchor scale μ* a stationarity point and β(g) = (1/ln φ) dg/dr. Mass is the real number type from RSNativeUnits. The mass_evolution_exp definition computes γ_0/(2b_0) using b0_qcd(n_f) from the QCD beta structure. The PrimitiveDistinction.from theorem supplies the axiomatic grounding for these structural conditions.
proof idea
One-line definition that multiplies the reference mass by the ratio of couplings raised to the power returned by mass_evolution_exp.
why it matters
It supplies the explicit mass-running formula used by mass_ratio_rg_invariant to prove ratios are RG-invariant at leading order and by transport_mass_through for multi-threshold transport. This implements the running mass piece of the RS renormalization paper, consistent with the forced asymptotic freedom for n_f ≤ 16 from the φ-ladder derivative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.