m_c_exp
plain-language theorem explainer
The declaration supplies the PDG experimental charm quark mass as a fixed real constant in MeV. Particle physicists comparing Recognition Science phi-ladder predictions to data would cite this value when checking the up-type sector at rung 15. It is introduced by direct numeric assignment with no further computation or derivation.
Claim. The experimental charm quark mass is the constant $m_c^exp = 1270$ (MeV, MS-bar at $m_c$).
background
The QuarkVerification module treats experimental quark masses as quarantined constants imported from PDG 2024 rather than derived inside Recognition Science. For the up-quark sector the mass formula is $m(UpQuark,r) = 2^{-1} phi^{-5} phi^{35} phi^r / 10^6$ MeV, which simplifies to $phi^{30+r}/(2*10^6)$ MeV; charm corresponds to rung $r=15$. The module imports Anchor for the rung integers and Verification for comparison machinery, keeping all six quark experimental values separate from the certified RS surface.
proof idea
Direct definition that assigns the literal value 1270 to the constant.
why it matters
This constant supplies the benchmark for RS mass verification in the charm sector and therefore supports the module-level comparison between phi-ladder predictions and PDG data. It sits downstream of the Anchor rung assignments and upstream of any future verification theorems that would quantify agreement for the up-type quarks. No open scaffolding questions are closed by this definition itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.