pole_factor_pos_top
plain-language theorem explainer
The theorem shows that the two-loop pole-to-MS-bar conversion factor stays positive for alpha_s in (0, 0.5) when N_l equals 5. QCD phenomenologists converting top-quark masses between pole and MS-bar schemes cite it to guarantee the factor does not flip sign inside the perturbative window. The proof unfolds the explicit quadratic expression, verifies each coefficient positive by norm_num and mul_pos, then closes with nlinarith.
Claim. Let $K_1 = 4/3$ and $K_2(N_l) = 11.1 - 1.04 N_l$. For real $a$ with $0 < a < 0.5$, $0 < 1 + K_1 (a/π) + K_2(5) (a/π)^2$.
background
The module supplies the two-loop relation m_pole = m_MS(m_MS) * (1 + (4/3)(alpha_s/π) + K_2 (alpha_s/π)^2) with K_2(N_l) = 11.1 - 1.04 N_l. K_1 is the universal one-loop coefficient 4/3. pole_factor(alpha_s, N_l) is the explicit quadratic 1 + K_1 (alpha_s/π) + K_2(N_l) (alpha_s/π)^2. The local setting is the perturbative conversion needed to compare RS mass predictions with PDG values for the top quark at N_l = 5.
proof idea
Unfold pole_factor, K_1 and K_2. Establish positivity of alpha_s/π and its square by div_pos and pow_pos. Compute K_2(5) > 0 by norm_num. Prove the linear term 1 + (4/3)(alpha_s/π) > 0 by mul_pos followed by linarith. Close the quadratic inequality with nlinarith on the three positive summands.
why it matters
It is invoked directly by m_pole_from_MS_pos_top to obtain positivity of the pole mass from a positive MS-bar mass, and by poleToMSbarCert_holds to populate the certificate record. The result therefore supplies the concrete positivity lemma required for the top-quark case inside the two-loop conversion. It closes the perturbative positivity step for N_l = 5 without introducing extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.