d_2_mass_neg
plain-language theorem explainer
The NLO mass matching coefficient at heavy quark thresholds is negative. QCD phenomenologists cite the sign when running quark masses downward across flavor thresholds to preserve consistency in the MS-bar scheme. The proof is a one-line wrapper that unfolds the constant definition and applies numerical normalization.
Claim. The NLO mass matching coefficient satisfies $d_2 = -89/432 < 0$.
background
In NLO threshold matching for QCD, the quark mass relation across a heavy flavor threshold at scale mu_q = m_q^MSbar reads m^(n)(mu_q) = m^(n+1)(mu_q) * (1 + sum_k d_k a^k) with d_1 = 0 and d_2 = -89/432 in the MS-bar decoupling scheme. The definition d_2_mass records this standard perturbative coefficient, whose negativity implies a slight downward shift in the matched mass. The module supplies the algebraic infrastructure for both coupling and mass matching when the number of active flavors changes.
proof idea
One-line wrapper that unfolds d_2_mass to the rational constant -89/432 and applies norm_num to verify the strict inequality.
why it matters
The result supplies the d_2_mass_neg field required by the ThresholdMatchingCert structure and is assembled into the master certificate theorem thresholdMatchingCert_holds. It guarantees that the inverse mass matching factor remains positive when applied in the physical direction. In the Recognition framework this supplies a standard QCD ingredient that can be inserted into the phi-ladder mass formulas without introducing sign inconsistencies at flavor thresholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.