module module moderate

`IndisputableMonolith.Physics.QCDRGE.MassAnomalousDimension`

This module defines the leading coefficient of the quark mass anomalous dimension in the MS-bar scheme and supplies the associated mass-ratio functions at one- and two-loop order. It is imported by the heavy-quark MS-bar scorecards and the scheme-reconciliation layer that converts RS structural masses to running masses. The module consists of constant definitions and algebraic identities that extend the two-loop alpha_s running imported from its sole dependency.

claimThe leading mass anomalous dimension coefficient is denoted $c_0$; the module also supplies the one-loop mass ratio $m(m_1)/m(m_2)$ and its two-loop extension together with the positive-definite variants evaluated at the anchor scale.

background

The module sits inside the QCD renormalization-group track for heavy quarks. It imports the two-loop alpha_s running whose doc-comment states that it extends the one-loop formula by the second beta-function coefficient b1. The local definitions (c0, c1, mass_ratio_leading, mass_ratio_two_loop, m_running, etc.) implement the standard expansion of the mass anomalous dimension gamma_m in powers of alpha_s. The setting is the MS-bar scheme with running between an RS anchor scale (typically M_Z) and the individual quark scales.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the coefficient required by QuarkSchemeReconciliation to convert rs_mass_MeV to massAtAnchor and by the three MS-bar scorecards (charm, bottom, top) to place the RS rung predictions inside empirical bands after two-loop running. It therefore closes the loop between the structural phi-ladder masses and the PDG MS-bar values quoted in the downstream scorecards.

scope and limits

Does not derive the anomalous dimension from a Lagrangian.
Does not contain threshold-matching coefficients.
Does not evaluate numerical running for specific quark flavors.
Does not address higher than two-loop terms.

used by (5)

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

IndisputableMonolith.Masses.QuarkSchemeReconciliation module_import
IndisputableMonolith.Physics.BottomMSBarScoreCard module_import
IndisputableMonolith.Physics.CharmMSBarScoreCard module_import
IndisputableMonolith.Physics.QCDRGE.ThresholdMatching module_import
IndisputableMonolith.Physics.TopMSBarScoreCard module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS module_import

declarations in this module (15)

def c0 L37
def c1 L40
def mass_ratio_leading L43
def mass_ratio_two_loop L47
theorem b0_pos_at5 L54
theorem mass_ratio_leading_pos L56
theorem mass_ratio_two_loop_pos L62
theorem mass_ratio_leading_at_anchor L72
theorem mass_ratio_two_loop_at_anchor L79
def m_running L92
theorem m_running_pos L95
theorem m_running_at_anchor L102
structure MassAnomalousDimensionCert L111
theorem c1_at5_pos L125
theorem massAnomalousDimensionCert_holds L127