m_c_exp
plain-language theorem explainer
Defines the PDG 2024 experimental charm-quark mass as 1270 MeV (MS-bar scheme at the charm scale). Used in the quarantined mass-comparison module to benchmark Recognition Science φ-ladder predictions against measured values. Pure numeric constant; no proof content.
Claim. The experimental charm-quark mass is the real constant $m_c^{\mathrm{exp}} = 1270$ (in MeV), corresponding to $1.27(2)\,\mathrm{GeV}$ in the $\overline{\mathrm{MS}}$ scheme evaluated at the charm scale.
background
The module MassComparison sits in the Verification domain and is explicitly quarantined from the certified RS surface: it imports external PDG 2024 numbers and compares them to RS mass predictions that depend on the φ-ladder anchor system.
RS predicts species masses via $m = \mathrm{yardstick}(\mathrm{sector}) \times \varphi^{r_0 + r_{\mathrm{species}}}$, with coherence energy $E_{\mathrm{coh}} = \varphi^{-5}$ and sector yardsticks built from cube-geometry integers. Experimental anchors such as this charm mass are not derived inside RS; they serve only as comparison targets.
Sibling constants supply the other light-quark and lepton experimental masses (and their quoted uncertainties) in the same MeV convention.
proof idea
No proof. The declaration is a one-line definition binding the real constant 1270, taken from the PDG 2024 charm mass $1.27(2),\mathrm{GeV}$ converted to MeV in the MS-bar scheme at $m_c$.
why it matters
Supplies the experimental charm reference point for machine-checked residual tables that compare RS φ-ladder mass predictions against PDG 2024. The module is quarantined precisely because these numbers are external; they do not enter the forcing chain (T0–T8), the Recognition Composition Law, or the derivation of constants. Downstream comparison lemmas (when present) use this constant only as a numeric benchmark, not as an RS-derived input. Closes no open theoretical gap; it is bookkeeping for verification reports.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.