m_c_PDG_GeV
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value from the Recognition Science forcing chain.
- Does not incorporate the PDG uncertainty of 0.02 GeV.
- Does not perform the two-loop running calculation itself.
- Does not specify the renormalization scheme beyond the MS-bar label.
formal statement (Lean)
37def m_c_PDG_GeV : ℝ := 1.27
proof body
Definition body.
38
39/-- PDG 2024 m_c(m_c) MS-bar uncertainty, in GeV. -/