mass_match
plain-language theorem explainer
mass_match supplies the NLO factor converting the (n+1)-flavor quark mass to the n-flavor mass at the heavy-quark threshold scale. QCD phenomenologists running couplings across b or c thresholds cite the factor when matching MS-bar masses. The implementation is a direct one-line multiplication by the correction term built from the pre-defined d_2_mass coefficient.
Claim. The NLO mass matching at threshold reads $m^{(n)} = m^{(n+1)} (1 + d_2 (alpha_s / pi)^2)$, where $m^{(n+1)}$ is the mass above threshold, $alpha_s$ is the strong coupling evaluated at the threshold, and $d_2$ is the NLO coefficient in the MS-bar scheme.
background
Heavy-quark threshold matching arises when the number of active QCD flavors changes at the scale mu_q equal to the quark mass. The module states that the mass relation takes the form m^(n)(mu_q) = m^(n+1)(mu_q) * (1 + sum d_k a^k) with d_1 = 0 and d_2 negative at NLO; the supplied definition encodes exactly this leading correction. Upstream structures from PhiForcingDerived and SpectralEmergence embed the SU(3) gauge sector and three-generation content into the phi-ladder, while the alpha constant from Constants.Alpha supplies the coupling value used in the correction term.
proof idea
The definition is a one-line algebraic expression that multiplies mass_above by (1 + d_2_mass * (alpha_at_threshold / pi)^2). No lemmas or tactics are applied; the body directly transcribes the NLO formula given in the module documentation.
why it matters
mass_match is invoked by mass_match_pos to prove positivity of the corrected mass and by ThresholdMatchingCert to certify the full set of NLO matching factors. It completes the structural infrastructure for consistent RGE running of alpha_s and masses across flavor thresholds inside the Recognition Science phi-ladder treatment of the QCD sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.