mass_match_pos
The theorem shows that the NLO mass matching factor across a heavy quark threshold stays positive whenever the input mass is positive and the strong coupling lies in (0,1). QCD phenomenologists running quark masses through flavor thresholds cite the result to guarantee the output mass remains physical. The proof unfolds mass_match, reduces positivity to a bound on the correction term via mul_pos, establishes d_2_mass in (-1,0) and (alpha/pi)^2 in (0,1) by norm_num and linarith, then closes with nlinarith and linarith.
claimLet $m>0$ and $0<α<1$. Then the NLO-matched mass $m'=m(1+d_2(α/π)^2)$ satisfies $m'>0$, where $d_2=-89/432$ is the two-loop mass matching coefficient in the MS-bar scheme.
background
In QCD renormalization-group evolution the number of active flavors changes at each heavy-quark threshold μ_q=m_q. The mass matching condition reads m^(n)(μ_q)=m^(n+1)(μ_q)(1+∑d_k a^k) with d_1=0 and d_2=-89/432 in the MS-bar decoupling scheme. The module supplies the structural definitions of the finite matching coefficients and proves their basic algebraic properties, including sign constraints needed for physical consistency.
proof idea
The proof unfolds the definition of mass_match and applies mul_pos to reduce the claim to positivity of the correction 1+d_2_mass·(α/π)^2. It then proves d_2_mass>-1 and d_2_mass<0 by norm_num, shows 0<(α/π)^2<1 from the hypothesis α<1 together with π>1, combines the bounds with nlinarith to obtain d_2_mass·(α/π)^2>-1, and finishes with linarith.
why it matters in Recognition Science
The lemma is assembled into ThresholdMatchingCert via thresholdMatchingCert_holds, which packages all positivity and matching facts for the NLO QCD threshold infrastructure. It supplies the algebraic guarantee required by the module's heavy-quark decoupling scheme and supports integration of standard QCD running into the Recognition Science phi-ladder mass formulas and forcing chain.
scope and limits
- Does not derive the numerical value of d_2_mass from Recognition Science axioms.
- Does not treat orders higher than NLO.
- Does not prove the corresponding positivity statement for the coupling matching factor.
- Does not apply when α≥1 or when the input mass is non-positive.
- Does not address threshold matching for the strong coupling itself.
Lean usage
theorem thresholdMatchingCert_holds : ThresholdMatchingCert := { c_2_alpha_pos := c_2_alpha_pos, d_2_mass_neg := d_2_mass_neg, alpha_match_pos_lemma := alpha_match_pos, mass_match_pos_lemma := mass_match_pos }formal statement (Lean)
76theorem mass_match_pos (mass_above alpha_at_threshold : ℝ)
77 (h_mass_pos : 0 < mass_above) (h_alpha_pos : 0 < alpha_at_threshold)
78 (h_alpha_small : alpha_at_threshold < 1) :
79 0 < mass_match mass_above alpha_at_threshold := by
proof body
Tactic-mode proof.
80 unfold mass_match
81 apply mul_pos h_mass_pos
82 -- d_2_mass = -89/432 ≈ -0.206. We bound (a/π)^2 < 1, so the correction is > -1.
83 have h_d_gt : (-1 : ℝ) < d_2_mass := by unfold d_2_mass; norm_num
84 have h_d_neg : d_2_mass < 0 := by unfold d_2_mass; norm_num
85 have h_a_pos : 0 < alpha_at_threshold / Real.pi := div_pos h_alpha_pos Real.pi_pos
86 have h_a_sq_pos : 0 < (alpha_at_threshold / Real.pi) ^ 2 := pow_pos h_a_pos 2
87 -- Bound (a/π)^2 < 1: a < 1 and π > 1, so a/π < 1, so (a/π)^2 < 1.
88 have h_pi_gt_one : (1 : ℝ) < Real.pi := by
89 linarith [Real.pi_gt_three]
90 have h_a_over_pi_lt_one : alpha_at_threshold / Real.pi < 1 := by
91 rw [div_lt_one Real.pi_pos]; linarith
92 have h_a_sq_lt_one : (alpha_at_threshold / Real.pi) ^ 2 < 1 := by
93 have : (alpha_at_threshold / Real.pi) ^ 2 < 1 ^ 2 := by
94 apply sq_lt_sq' <;> nlinarith [h_a_pos]
95 simpa using this
96 -- d_2_mass * x where x ∈ (0, 1), d_2_mass ∈ (-1, 0), so product ∈ (-1, 0).
97 have h_prod_gt : -1 < d_2_mass * (alpha_at_threshold / Real.pi) ^ 2 := by
98 nlinarith [h_d_gt, h_d_neg, h_a_sq_pos, h_a_sq_lt_one]
99 linarith
100
101/-! ## Round-trip: matching plus its inverse is the identity to leading order -/
102
103/-- The matching at any threshold is a multiplicative perturbation; its inverse
104 factor at NLO is `1 - c_2_alpha * (a/pi)^2 + O(a^4)`. We expose this as a
105 structural definition rather than re-proving the perturbative inverse. -/