pith. sign in
module module high

IndisputableMonolith.Physics.QCDRGE.ThresholdMatching

show as:
view Lean formalization →

This module supplies the NLO threshold matching coefficients for alpha_s and quark masses in the MS-bar scheme when the renormalization scale crosses a heavy quark mass. It is used by downstream calculations that evolve QCD parameters across flavor thresholds, notably the charm mass scorecard. The module consists of direct definitions of standard results such as c_2_alpha = 11/72 together with the associated match and unmatch functions.

claimThe NLO coefficient for the strong coupling matching at the heavy-quark threshold is $c_2^alpha = 11/72$. The module also defines the matching functions $alpha_match$ and $mass_match$ that incorporate the two-loop beta function and the mass anomalous dimension $gamma_m(a) = c_0 a + c_1 a^2$.

background

The module belongs to the QCD RGE track and imports the two-loop alpha_s running from TwoLoopAlphaS (which adds the b_1 coefficient to the beta function) together with the two-loop quark mass anomalous dimension from MassAnomalousDimension. In that upstream module the running of the MS-bar mass is governed by d log m / d log mu^2 = -gamma_m(alpha_s) with gamma_m(a) = c_0 a + c_1 a^2 + O(a^3). Threshold matching supplies the finite corrections that arise when a heavy quark is decoupled at mu = m_q^MSbar.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds CharmMSBarScoreCard, which combines the RS structural prediction placing charm at rung 15 with the two-loop running from the M_Z anchor to the m_c scale. It supplies the NLO coefficients required to convert the RS mass formula into the empirical MS-bar value m_c(m_c) = 1.27 +- 0.02 GeV.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (11)