mass_ratio_leading_pos
plain-language theorem explainer
The theorem establishes that the leading logarithmic quark mass running ratio in the MS-bar scheme stays strictly positive whenever the strong couplings at both scales are positive. Perturbative QCD and lattice practitioners would cite it when confirming that running masses remain positive under the one-loop RGE solution. The proof is a one-line term wrapper that unfolds the ratio definition and applies the real-power positivity lemma to the positive coupling quotient.
Claim. If $0 < α_s(μ)$ and $0 < α_s(μ_0)$, then the leading mass ratio $(α_s(μ)/α_s(μ_0))^{c_0 / b_0(N_f)} > 0$, where $c_0 = 1$ is the universal leading coefficient of the mass anomalous dimension and $b_0(N_f)$ is the leading beta-function coefficient.
background
The module derives the two-loop MS-bar running of quark masses from the renormalization-group equation d log m / d log μ² = −γ_m(α_s) with γ_m(a) = c_0 a + c_1 a² + O(a³) and a = α_s/π. The leading term integrates to the pure power-law ratio m(μ)/m(μ_0) = (α_s(μ)/α_s(μ_0))^{c_0/b_0(N_f)}. The upstream definition mass_ratio_leading encodes exactly this expression via Real.rpow (α_μ / α_μ₀) (c_0 / b_0 N_f). The module documentation states that the full two-loop solution multiplies this leading factor by a subleading correction R.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of mass_ratio_leading, exposing a real power whose base is the positive quotient α_μ / α_μ₀. The library lemma Real.rpow_pos_of_pos is then applied directly to that quotient and the arbitrary real exponent.
why it matters
This result supplies the positivity anchor for the leading term in the mass-running formula. It is invoked by the sibling theorem mass_ratio_two_loop_pos, which establishes positivity of the full two-loop ratio by multiplying the leading factor by a positive correction. The module documentation presents the closed-form running mass as the product of the leading power and the two-loop remainder R, so the theorem closes the leading-order positivity step required for physical applications of the RGE.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.