ThresholdMatchingCert
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical values 11/72 or -89/432 from a first-principles calculation.
- Does not extend the matching factors beyond NLO.
- Does not constrain the choice of threshold scale mu_q.
- Assumes alpha remains below 1 so that the perturbative expansion stays positive.
formal statement (Lean)
111structure ThresholdMatchingCert where
112 c_2_alpha_pos : 0 < c_2_alpha
113 d_2_mass_neg : d_2_mass < 0
114 alpha_match_pos_lemma : ∀ alpha_above : ℝ,
115 0 < alpha_above → alpha_above < 1 → 0 < alpha_match alpha_above
116 mass_match_pos_lemma : ∀ mass_above alpha_at_threshold : ℝ,
117 0 < mass_above → 0 < alpha_at_threshold → alpha_at_threshold < 1 →
118 0 < mass_match mass_above alpha_at_threshold
119