mass_ratio_two_loop_pos
plain-language theorem explainer
The theorem proves positivity of the two-loop quark mass running ratio whenever the strong couplings at both scales are positive. QCD phenomenologists and lattice analysts would cite it to bound running masses in the MS-bar scheme without sign flips. The proof is a one-line wrapper that factors the ratio into its leading power-law term and an exponential correction then invokes positivity of each factor separately.
Claim. If $0 < alpha_s(mu)$ and $0 < alpha_s(mu_0)$, then the two-loop mass ratio $m(mu)/m(mu_0) > 0$, where the ratio equals the leading power-law term times the exponential of the two-loop correction involving coefficients $c_0$, $c_1$, $b_0$, $b_1$.
background
The module solves the two-loop renormalization-group equation for the MS-bar quark mass. The anomalous dimension is gamma_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). Integration yields the running ratio m(mu)/m(mu_0) = (alpha_s(mu)/alpha_s(mu_0))^{c_0/b_0} times an exponential factor R that encodes the two-loop correction (c_1/b_0 - c_0 b_1/b_0^2) (alpha_mu - alpha_mu_0)/(4 pi).
proof idea
The proof unfolds the definition of mass_ratio_two_loop to expose the product of mass_ratio_leading and Real.exp of the two-loop coefficient times the coupling difference. It then applies mul_pos, supplying the already-proved positivity of the leading term via mass_ratio_leading_pos and the universal positivity of the exponential via Real.exp_pos.
why it matters
The result is invoked inside massAnomalousDimensionCert_holds to certify the full two-loop mass anomalous dimension and inside m_running_pos to guarantee that the running mass itself stays positive. It completes the positivity closure for the perturbative mass running in the Recognition Science QCD module, ensuring the derived running parameters remain consistent with the framework's core functional equation and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.