IndisputableMonolith.Physics.QCDRGE.MassAnomalousDimension
Module supplies the leading coefficient of the quark mass anomalous dimension for QCD renormalization group evolution in the MS-bar scheme. Authors of quark mass scorecards and scheme reconciliation proofs cite it to obtain the one-loop running factor between the Recognition Science anchor scale and experimental scales. Content consists of constant definitions together with positive and anchored variants of mass ratio lemmas that build directly on the imported two-loop alpha_s running.
claimThe leading mass anomalous dimension coefficient $c_0$ enters the leading-order mass ratio as the exponent in $m(m)/m(m_0) = [a_s(m)/a_s(m_0)]^{c_0/(2b_0)}$, where $b_0$ is the first beta-function coefficient.
background
The module sits inside the heavy-quark closure track of QCD RGE. It imports the two-loop alpha_s running whose doc-comment states that it extends the one-loop alpha_s_running to include the second beta-function coefficient b1, giving the standard MS-bar two-loop running formula. The module introduces the leading mass anomalous dimension coefficient c0 along with mass_ratio_leading, mass_ratio_two_loop, m_running and their positive and anchored variants. These objects implement the one-loop contribution to the mass RGE dm/dlog mu = -gamma_m m with gamma_m expanded to first order in alpha_s.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The definitions feed the QuarkSchemeReconciliation module that converts between rs_mass_MeV and massAtAnchor via RGE, and they supply the running factor required by BottomMSBarScoreCard, CharmMSBarScoreCard and TopMSBarScoreCard to place RS rung predictions inside PDG MS-bar bands. They also support ThresholdMatching for NLO heavy-quark threshold corrections. The module therefore closes the link from the structural phi-ladder mass formula to observable scales using the two-loop alpha_s infrastructure.
scope and limits
- Does not derive the numerical value of c0 from Recognition Science axioms.
- Does not implement two-loop or higher corrections to the mass anomalous dimension.
- Does not perform numerical integration of the full RGE differential equation.
- Does not incorporate electroweak or beyond-Standard-Model corrections.
- Does not handle scheme conversion outside the MS-bar scheme.
used by (5)
depends on (1)
declarations in this module (15)
-
def
c0 -
def
c1 -
def
mass_ratio_leading -
def
mass_ratio_two_loop -
theorem
b0_pos_at5 -
theorem
mass_ratio_leading_pos -
theorem
mass_ratio_two_loop_pos -
theorem
mass_ratio_leading_at_anchor -
theorem
mass_ratio_two_loop_at_anchor -
def
m_running -
theorem
m_running_pos -
theorem
m_running_at_anchor -
structure
MassAnomalousDimensionCert -
theorem
c1_at5_pos -
theorem
massAnomalousDimensionCert_holds