thresholdMatchingCert_holds
The theorem establishes that the NLO heavy-quark threshold matching certificate holds by direct assembly of four positivity results. QCD phenomenologists running couplings and masses across flavor thresholds would cite it to confirm structural consistency of the matching factors. The proof is a term-mode record construction that populates the certificate fields from the sibling lemmas on coefficient signs and matching positivity.
claimThe NLO heavy-quark threshold matching certificate holds: the coupling coefficient satisfies $0 < c_2$, the mass coefficient satisfies $d_2 < 0$, the coupling matching factor is positive for all $0 < a < 1$, and the mass matching factor is positive for all $m > 0$ and $0 < a < 1$.
background
The module treats NLO matching of the strong coupling and quark masses when the number of active flavors changes at a heavy-quark threshold scale, typically set to the MS-bar mass. The matching relations are multiplicative perturbations whose NLO coefficients are $c_2 = 11/72$ for the coupling and $d_2 = -89/432$ for the mass; the certificate structure packages the algebraic properties needed to keep the factors positive and invertible in the perturbative regime. ThresholdMatchingCert is defined as the structure containing exactly these four fields: positivity of $c_2$, negativity of $d_2$, and the two universal positivity lemmas for the matching functions. The upstream lemmas alpha_match_pos and mass_match_pos establish the positivity statements by unfolding the explicit multiplicative definitions and applying elementary inequalities on positive reals less than one.
proof idea
The proof is a one-line term-mode record construction that supplies the four fields of ThresholdMatchingCert directly from the sibling theorems c_2_alpha_pos, d_2_mass_neg, alpha_match_pos, and mass_match_pos.
why it matters in Recognition Science
This declaration supplies the master certificate for the entire ThresholdMatching module and thereby certifies the structural integrity of NLO decoupling in the QCD RGE implementation. It closes the local proof obligations for the matching infrastructure without introducing new hypotheses, providing a verified foundation that downstream running procedures can invoke when crossing heavy-quark thresholds. In the broader Recognition Science setting it contributes the concrete QCD matching layer required for consistent extraction of low-energy parameters from the high-scale theory.
scope and limits
- Does not derive the numerical values of the matching coefficients from first principles.
- Does not extend the matching to orders beyond NLO.
- Does not treat light-quark thresholds or schemes other than MS-bar.
- Does not supply numerical running algorithms or integration routines.
formal statement (Lean)
123theorem thresholdMatchingCert_holds : ThresholdMatchingCert :=
proof body
Term-mode proof.
124 { c_2_alpha_pos := c_2_alpha_pos
125 d_2_mass_neg := d_2_mass_neg
126 alpha_match_pos_lemma := alpha_match_pos
127 mass_match_pos_lemma := mass_match_pos }
128
129end
130
131end IndisputableMonolith.Physics.QCDRGE.ThresholdMatching