mass_match_pos
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.