m_c_PDG_pos
Physicists comparing RS structural predictions to PDG data cite the positivity of the charm MS-bar central value when assembling the full scorecard certificate. The declaration supplies the fact that 1.27 GeV is positive for use in charmMSBarCert_holds. Its proof reduces immediately to unfolding the constant definition and numerical checking.
claimThe central PDG value for the charm quark MS-bar mass at the charm scale satisfies $0 < 1.27$ in GeV units.
background
The Charm Quark MS-bar Mass Scorecard module records the PDG 2024 central value for the charm quark MS-bar mass as 1.27 GeV. Charm is assigned rung 15 in the RS fermion ladder for up-type quarks of generation 2. The upstream definition m_c_PDG_GeV supplies this numerical constant, which is then used to state positivity and to compare against the RS prediction after two-loop QCD running from the M_Z anchor.
proof idea
The term proof unfolds m_c_PDG_GeV to expose the literal value 1.27 and applies norm_num to verify the strict inequality.
why it matters in Recognition Science
The result is invoked by charmMSBarCert_holds to complete the empirical half of the CharmMSBarCert structure. It anchors the comparison between the RS rung-15 prediction and the PDG band in the scorecard that validates the mass formula at the charm sector.
scope and limits
- Does not include the PDG uncertainty of 0.02 GeV.
- Does not derive the value from the phi-ladder or gap corrections.
- Does not address the two-loop running between M_Z and m_c scales.
- Applies strictly to the central value in GeV.
formal statement (Lean)
42theorem m_c_PDG_pos : 0 < m_c_PDG_GeV := by unfold m_c_PDG_GeV; norm_num
proof body
Term-mode proof.
43
44/-! ## RS prediction (structural) -/
45
46/-- RS rung for charm in the sector formula: r = 15 (up-type, generation 2). -/