d_2_mass
d_2_mass supplies the NLO quark mass matching coefficient at heavy quark thresholds as the constant -89/432. QCD calculations that match running masses between n and n+1 flavor schemes at mu equal to the MS-bar quark mass cite this value for the quadratic correction. The declaration is a direct numerical assignment with no lemmas or computation steps.
claimThe NLO coefficient $d_2$ in the mass matching relation $m^{(n)} (mu_q) = m^{(n+1)} (mu_q) (1 + d_2 (alpha_s / pi)^2)$ at the threshold $mu_q = m_q^{MSbar}$ equals $-89/432$.
background
The ThresholdMatching module implements NLO matching conditions for QCD couplings and masses when the active flavor count changes at heavy quark thresholds. The mass relation is $m^{(n)}(mu_q) = m^{(n+1)}(mu_q) (1 + sum d_k a^k)$ with $a = alpha_s / pi$, where $d_1 = 0$ and $d_2 = -89/432$ in the MS-bar scheme; this pairs with the coupling coefficient $c_2_alpha = 11/72$. The module supplies the structural matching factors and their positivity properties. Upstream results include the scale function defined as $phi^k$ and the self-reference structure recording meta-realization axioms.
proof idea
The declaration is a direct definition that assigns the rational constant -89/432. No lemmas are applied and no tactics are used; it functions as the constant input to the mass matching expression.
why it matters in Recognition Science
This definition supplies the mass correction coefficient required by mass_match and ThresholdMatchingCert, which collects positivity lemmas for both coupling and mass factors. It completes the NLO coefficient pair with c_2_alpha, enabling algebraic verification of matching properties inside the Recognition Science QCD layer and supporting consistent parameter running across flavor thresholds.
scope and limits
- Does not derive the numerical value from loop integrals.
- Does not include O(a^3) or higher matching terms.
- Does not vary the threshold scale beyond mu = m_q.
- Does not address renormalization schemes other than MS-bar.
Lean usage
mass_match mass_above alpha_at_thresholdformal statement (Lean)
45def d_2_mass : ℝ := -89 / 432
proof body
Definition body.
46
47/-- Matching factor for alpha_s at threshold (NLO accuracy).
48 Returns alpha_s^(n) given alpha_s^(n+1) at the threshold scale. -/