ThresholdMatchingCert
plain-language theorem explainer
ThresholdMatchingCert packages the NLO positivity conditions on the QCD threshold matching coefficients together with the positivity of the resulting alpha_s and mass matching factors in the physical range. QCD running analyses that cross heavy-quark thresholds cite the certificate to guarantee that the multiplicative corrections preserve positivity. The declaration is a plain record constructor that assembles four already-proved fields.
Claim. A structure containing four fields: $0 < c_2^alpha$, $d_2^m < 0$, the lemma that $0 < alpha_match(alpha_above)$ for all $alpha_above in (0,1)$, and the lemma that $0 < mass_match(m_above, alpha_at_threshold)$ for all $m_above > 0$ and $alpha_at_threshold in (0,1)$, where $c_2^alpha = 11/72$, $d_2^m = -89/432$, $alpha_match(alpha) = alpha (1 + c_2^alpha (alpha/pi)^2)$, and $mass_match(m,alpha) = m (1 + d_2^m (alpha/pi)^2)$.
background
The module supplies the NLO matching infrastructure for QCD couplings and quark masses when the number of active flavors changes at a heavy-quark threshold. Standard MS-bar results give the finite coefficients $c_2^alpha = 11/72$ and $d_2^m = -89/432$; the matching maps are then defined by the multiplicative factors $alpha_match(alpha_above) = alpha_above (1 + c_2^alpha (alpha_above/pi)^2)$ and $mass_match(m_above, alpha) = m_above (1 + d_2^m (alpha/pi)^2)$. The upstream definitions alpha_match, mass_match, c_2_alpha and d_2_mass together with their positivity theorems c_2_alpha_pos and d_2_mass_neg supply the concrete values and sign statements that the certificate records.
proof idea
The declaration is a structure definition whose body simply lists the four fields. Each field is filled by a direct reference to an existing theorem or definition in the same module: c_2_alpha_pos for the first, d_2_mass_neg for the second, and the two forall lemmas alpha_match_pos and mass_match_pos for the last two.
why it matters
thresholdMatchingCert_holds instantiates the structure to produce a single object that asserts the NLO matching relations preserve positivity. The certificate therefore closes the algebraic part of the threshold-matching step inside the QCD RGE infrastructure, allowing consistent running of alpha_s and masses across flavor thresholds without sign violations. The module doc-comment records that the entire file contains zero sorrys, so the certificate is fully discharged at NLO.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.