223 fun h => by unfold rs_anchor_scale at h; linarith 224 225/-! ## QCD Mass Running (Leading Order) 226 227The QCD mass anomalous dimension governs how quark masses change with 228renormalization scale. At one loop: 229 230 m(μ₂) = m(μ₁) × (α_s(μ₂)/α_s(μ₁))^(γ₀/(2b₀)) 231 232where γ₀ = 8 is the universal one-loop anomalous dimension and b₀ depends 233on the number of active flavors n_f. Flavor thresholds (at m_c, m_b, m_t) 234require matching the running across regions with different n_f. 235 236This infrastructure enables scheme-consistent quark residuals at a common 237scale μ* = 182 GeV, removing the mixed-scheme artifacts that inflate 238the sub-leading mass formula's eta parameter (Item 8). -/ 239 240/-- One-loop QCD mass anomalous dimension: γ₀ = 8 (universal for all quarks). -/
depends on (29)
Lean names referenced from this declaration's body.