m_c_PDG_unc_GeV
The declaration supplies the PDG 2024 experimental uncertainty on the charm quark MS-bar mass evaluated at its own scale. Particle physicists comparing Recognition Science mass predictions to collider data would cite this constant when checking whether the RS rung-15 prediction falls inside the measured band after QCD running. The entry is a direct numerical definition with no derivation steps.
claimThe uncertainty in the PDG 2024 value of the charm quark MS-bar mass $m_c(m_c)$ is $0.02$ GeV.
background
The module CharmMSBarScoreCard tabulates the charm quark mass in the MS-bar scheme. It records the PDG central value $m_c(m_c) = 1.27$ GeV together with its uncertainty. The Recognition Science framework predicts the charm mass from the structural rung c = 15 on the phi-ladder using the gap-corrected formula massAtAnchor. Two-loop QCD running via alpha_s and mass anomalous dimension connects the RS anchor scale (typically M_Z) to the low scale m_c. The scorecard then checks whether the evolved RS prediction lies inside the PDG band.
proof idea
The definition directly assigns the constant 0.02 to the real number type, serving as the uncertainty input for subsequent comparisons in the module.
why it matters in Recognition Science
This constant anchors the empirical side of the charm mass scorecard, allowing direct comparison against the RS structural prediction m_c_predicted_via_RS. It supports the certification theorem charmMSBarCert_holds that verifies the prediction sits inside the PDG band after two-loop running. The entry closes the loop between the phi-ladder mass formula and experimental data in the up-type generation-2 sector.
scope and limits
- Does not compute the uncertainty from raw data.
- Does not incorporate future PDG updates.
- Does not specify the correlation with the central value.
- Does not address scheme conversion beyond MS-bar.
formal statement (Lean)
40def m_c_PDG_unc_GeV : ℝ := 0.02
proof body
Definition body.
41