running_mass
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 in Recognition Science
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.
scope and limits
- Does not include higher-order loop corrections to the beta function.
- Does not switch active flavor number at mass thresholds.
- Does not evaluate the coupling values α_s at given scales.
- Applies only within a single sector with fixed n_f.
formal statement (Lean)
268noncomputable def running_mass (m_ref α_s_ref α_s_target : ℝ) (n_f : ℕ) : ℝ :=
proof body
Definition body.
269 m_ref * (α_s_target / α_s_ref) ^ (mass_evolution_exp n_f)
270
271/-- **Mass ratios within a sector are RG-invariant at LO** when both masses
272 are evolved from the same reference scale with the same α_s values. -/