pole_factor_pos_top
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove positivity for N_l other than 5.
- Does not extend to alpha_s >= 0.5.
- Does not include O(alpha_s^3) or higher terms.
- Does not address the inverse MS-bar to pole map.
Lean usage
theorem use_example (alpha_s : ℝ) (h_pos : 0 < alpha_s) (h_lt : alpha_s < 0.5) : 0 < pole_factor alpha_s 5 := pole_factor_pos_top alpha_s h_pos h_ltformal statement (Lean)
49theorem pole_factor_pos_top (alpha_s : ℝ)
50 (h_alpha_pos : 0 < alpha_s) (h_alpha_lt : alpha_s < 0.5) :
51 0 < pole_factor alpha_s 5 := by
proof body
Tactic-mode proof.
52 unfold pole_factor K_1 K_2
53 have h_a_pos : 0 < alpha_s / Real.pi := div_pos h_alpha_pos Real.pi_pos
54 have h_a_sq_pos : 0 < (alpha_s / Real.pi) ^ 2 := pow_pos h_a_pos 2
55 have h_K2_at5_pos : 0 < (11.1 - 1.04 * (5 : ℝ)) := by norm_num
56 -- 1 + positive + positive > 0 trivially
57 have h1 : 0 < 1 + (4 / 3) * (alpha_s / Real.pi) := by
58 have : 0 < (4 / 3) * (alpha_s / Real.pi) := mul_pos (by norm_num) h_a_pos
59 linarith
60 nlinarith [h_K2_at5_pos, h_a_sq_pos]
61