mass_evolution_exp_pos
plain-language theorem explainer
Mass evolution exponent γ₀/(2b₀) is positive for every n_f ≤ 16 active flavors. QCD phenomenologists analyzing renormalization-group mass running would cite this to fix the sign of quark-mass evolution under the RS φ-ladder. The proof unfolds the definition and applies the div_pos lemma to the product of the positive anomalous dimension and the positive b₀ coefficient.
Claim. For every natural number $n_f ≤ 16$, the mass evolution exponent satisfies $γ_0 / (2 b_0(n_f)) > 0$, where $γ_0$ is the mass anomalous dimension and $b_0(n_f)$ is the leading coefficient of the QCD β-function.
background
The module derives renormalization-group flows from the RS φ-ladder. The RS anchor scale μ* = 182.201 GeV is a stationarity point of the flow, and the β-function sign is fixed by the ladder derivative of the coupling. Asymptotic freedom holds for n_f ≤ 16 flavors, which determines the sign of b₀_qcd.
proof idea
The proof is a one-line wrapper. It unfolds the definition mass_evolution_exp = mass_anomalous_dim / (2 * b0_qcd n_f), then applies div_pos to the positive numerator mass_anomalous_dim_pos and the positive denominator factor (2 * b0_qcd n_f) supplied by asymptotic_freedom_criterion.
why it matters
This theorem fixes the sign of mass running inside the asymptotic-freedom window n_f ≤ 16, directly supporting the module's running-coupling formulas and the paper claim that β_QCD < 0 for n_f ≤ 16. It closes the positivity step required for the RS renormalization results listed in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.