c_2_alpha_pos
plain-language theorem explainer
The declaration proves that the NLO strong coupling matching coefficient at a heavy quark threshold is positive. QCD phenomenologists constructing decoupling relations for running alpha_s across flavor thresholds cite this result. The proof is a one-line wrapper that unfolds the explicit rational definition and applies norm_num to confirm the inequality.
Claim. The next-to-leading-order coefficient in the matching of the strong coupling across a heavy quark threshold satisfies $0 < 11/72$.
background
The module supplies structural matching infrastructure for QCD couplings and quark masses when the number of active flavors changes at a heavy quark scale mu_q. The NLO alpha_s matching coefficient is the constant 11/72 in the MS-bar scheme, with the matching relation alpha_s^(n)(mu_q) = alpha_s^(n+1)(mu_q) * (1 + sum c_k a^k). Upstream the definition supplies this explicit rational value as the standard perturbative result.
proof idea
The proof is a one-line wrapper that unfolds the definition of the coefficient to the rational 11/72 and invokes norm_num to establish positivity.
why it matters
This positivity result supplies the required field for the ThresholdMatchingCert structure, which certifies the algebraic properties of the matching factors including the inverse factor 1 - c_2 * (a/pi)^2 used in alpha_unmatch. It supports the NLO threshold matching infrastructure in the QCD RGE module for consistent running of couplings in multi-flavor regimes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.