alpha_match_pos
plain-language theorem explainer
The theorem shows that the NLO matching factor for alpha_s stays positive for 0 < alpha_above < 1. Phenomenologists working on QCD running across flavor thresholds cite it to guarantee no sign flips in the coupling. The proof is a tactic sequence that unfolds the definition, invokes mul_pos, and uses positivity of powers and the explicit positive coefficient 11/72.
Claim. If $0 < alpha < 1$, then $0 < alpha (1 + (11/72) (alpha / pi)^2)$.
background
The module supplies NLO matching infrastructure for the strong coupling and quark masses when the number of active flavors changes at heavy-quark thresholds in the MS-bar scheme. The function alpha_match(alpha_above) is defined as alpha_above multiplied by (1 + c_2_alpha times (alpha_above / pi) squared), where the upstream definition fixes c_2_alpha to the rational 11/72. The module documentation states that this supplies the structural matching with zero sorrys and proves basic algebraic properties under the perturbative regime.
proof idea
The proof unfolds alpha_match to expose the product. It applies mul_pos directly to the hypothesis 0 < alpha_above. Separate steps establish 0 < alpha_above / pi by div_pos and 0 < (alpha_above / pi)^2 by pow_pos. The coefficient c_2_alpha is unfolded and shown positive by norm_num, after which the positivity tactic closes the goal.
why it matters
This result is invoked by thresholdMatchingCert_holds to supply the positivity component of the assembled matching certificate. It completes the NLO positivity requirement inside the heavy-quark threshold matching infrastructure described in the module. In the Recognition Science setting it ensures that perturbative evolution of couplings remains sign-consistent inside the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.