m_running_pos
plain-language theorem explainer
The theorem proves that the two-loop running quark mass remains strictly positive whenever the initial mass and the strong couplings at both scales are positive. QCD phenomenologists computing MS-bar masses for charm and bottom quarks cite this result to confirm that evolved masses stay physical under renormalization-group flow. The proof is a one-line wrapper that unfolds the definition of m_running and applies the positivity of multiplication to the initial mass together with the already-established positivity of the two-loop mass ratio.
Claim. Let $m_0 > 0$, $a > 0$, $a_0 > 0$ and $N_f$ a natural number. Then the two-loop running mass satisfies $m(a) > 0$, where $m(a) := m_0 · R(a, a_0, N_f)$ and $R$ is the two-loop mass ratio $R(a, a_0, N_f) = (a/a_0)^{c_0/b_0} · exp[(c_1/b_0 - c_0 b_1/b_0^2)(a - a_0)/(4π)]$.
background
The module supplies the two-loop solution of the quark-mass renormalization-group equation in the MS-bar scheme. The anomalous dimension is expanded as γ_m(a) = c_0 a + c_1 a^2 with c_0 = 1 and c_1 = (101 N_c - 10 N_f)/24 - 5/8 C_F (N_c = 3). The integrated running mass between scales μ and μ_0 is expressed by the auxiliary definition m_running m_0 α_μ α_μ0 N_f := m_0 · mass_ratio_two_loop α_μ α_μ0 N_f, where mass_ratio_two_loop multiplies the leading power-law factor by a two-loop exponential correction involving the beta-function coefficients b_0 and b_1.
proof idea
The proof is a one-line wrapper. It unfolds the definition of m_running, exposing the product m_0 · mass_ratio_two_loop, then applies the lemma mul_pos to the hypothesis 0 < m_0 and the already-proved statement mass_ratio_two_loop_pos α_μ α_μ0 N_f h_α h_α0.
why it matters
m_running_pos is invoked directly by m_b_predicted_pos and m_c_predicted_pos to guarantee that the predicted bottom and charm masses remain positive, and it supplies the running_pos field of the MassAnomalousDimensionCert certificate. Within the Recognition Science framework it closes the positivity step of the two-loop QCD running that feeds the phi-ladder mass formula for light quarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.