d_2_mass
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.