pith. sign in
module module high

IndisputableMonolith.Physics.CharmMSBarScoreCard

show as:
view Lean formalization →

CharmMSBarScoreCard assembles the PDG 2024 central value for the charm quark MS-bar mass at its own scale, an RS-derived prediction, and a direct certification that the prediction lies inside the experimental band. QCD phenomenologists and RS mass-ladder users cite the certification result for validation against running quark masses. The module is a collection of numeric definitions plus one certification theorem built from the imported two-loop RGE suite.

claimThe module defines the PDG 2024 value $m_c(m_c) = 1.27$ GeV (MS-bar) and certifies that the RS prediction $m_c^{RS}$ at the relevant scale lies inside the PDG uncertainty interval.

background

The module operates inside the Recognition Science treatment of quark masses matched to QCD. It imports the base RS time quantum from Constants together with the two-loop alpha_s running, the MS-bar quark mass anomalous dimension gamma_m(a) = c_0 a + c_1 a^2, and NLO threshold matching across heavy-quark thresholds. These supply the running machinery needed to place an RS phi-ladder mass into the MS-bar scheme at m_c or M_Z. The local setting is therefore the standard two-loop QCD RGE evolution with flavor thresholds, used here only for the charm sector.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the charm-sector score card and the certification CharmMSBarCert that closes the RS mass formula application for the lightest heavy quark. It feeds the experimental consistency check required by the phi-ladder mass expression yardstick * phi^(rung-8 + gap(Z)) and supports the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain. No downstream theorems are listed in the current graph.

scope and limits

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (12)