d_2_mass_neg
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the coefficient value from a first-principles calculation.
- Does not address terms beyond NLO in the perturbative series.
- Does not specify the choice of matching scale beyond mu_q = m_q^MSbar.
formal statement (Lean)
121theorem d_2_mass_neg : d_2_mass < 0 := by unfold d_2_mass; norm_num
proof body
122