m_c_PDG_pos
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.