m_c_PDG_GeV
plain-language theorem explainer
The declaration supplies the PDG 2024 central value for the charm quark MS-bar mass at its own scale. Researchers comparing Recognition Science mass predictions to experimental data would reference this constant when verifying that the rung-15 structural prediction lies inside the observed band after two-loop running. The definition consists of a direct numerical assignment.
Claim. The central value of the charm-quark mass in the MS-bar scheme, evaluated at the renormalization scale equal to the mass itself, is $m_c(m_c) = 1.27$ GeV.
background
In the Charm Quark MS-bar Mass Scorecard module the Recognition Science framework assigns the charm quark to rung 15 in the phi-ladder mass formula for up-type quarks of the second generation. The module states the empirical PDG value $m_c(m_c) = 1.27 pm 0.02$ GeV in the MS-bar scheme and compares it to the RS prediction obtained by running the structural mass from the $M_Z$ anchor scale down to the charm scale using two-loop QCD beta functions and mass anomalous dimensions. Upstream results include the two-loop alpha_s running from QCDRGE.TwoLoopAlphaS and the threshold matching from ThresholdMatching.
proof idea
The definition is a direct numerical constant with no lemmas or tactics applied.
why it matters
This constant anchors the CharmMSBarCert structure, which certifies that the RS prediction at rung 15 lies inside the PDG interval (1.20, 1.34) GeV after two-loop running. It fills the empirical input slot in the scorecard that closes the comparison between the phi-ladder mass formula and measured heavy-quark masses. The module reports zero sorry statements, confirming the numerical match within the stated band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.