mass_charm_exp
plain-language theorem explainer
This definition supplies the PDG experimental charm quark mass of 1270 MeV as the target for quarter-ladder matching. Researchers verifying geometric predictions against observation cite it when checking the charm rung at R = -4.50. It is introduced by direct numeric assignment with no computation or proof steps.
Claim. The experimental mass of the charm quark is defined as $1270$ MeV.
background
The QuarkMasses module formalizes the quarter-ladder hypothesis in which quarks occupy quarter-integer rungs on the phi-ladder while sharing the structural base mass with leptons. Charm is assigned rung R = -4.50. The module documentation states that discrepancies for light quarks arise from non-perturbative QCD effects not yet included in the bare geometric derivation. This definition provides the observed mass target used in subsequent match checks. The upstream result is the identical constant definition appearing in the RRF.Physics.QuarkMasses module.
proof idea
One-line definition by direct assignment of the numeric value 1270.
why it matters
It anchors the charm_mass_match theorem, which confirms the quarter-ladder prediction lies within 2 percent of the experimental value, and feeds the hypothesis certificate H_charm_mass_match. This supports the T12 quark-mass derivation in the Recognition Science framework, where the phi-ladder yields acceptable matches for top, bottom, and charm. The module documentation flags that full reconciliation with the parameter-free core mass model layer remains open pending explicit equivalence proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.