mass_charm_exp
The declaration supplies the observed charm quark mass of 1270 MeV as the benchmark constant for quarter-ladder matching calculations. Researchers checking geometric mass predictions in Recognition Science would reference this value to confirm the sub-2% agreement at the charm rung. It is introduced as a direct numerical assignment with no computation or lemmas.
claimThe observed charm quark mass is defined as the real number 1270 (in MeV).
background
The module formalizes quark masses under the Quarter-Ladder Hypothesis, where quarks share the structural base mass with leptons but sit at quarter-integer rungs on the phi-ladder. Charm occupies the position R = -4.50 = -18/4, with the module noting that light-quark discrepancies arise from non-perturbative QCD effects not included in the bare geometric derivation. This definition supplies the empirical anchor used by downstream match certificates.
proof idea
The declaration is a direct constant assignment of the value 1270 with no lemmas applied.
why it matters in Recognition Science
It provides the observed benchmark for the charm_mass_match theorem, which certifies agreement to within 2% against the quarter-ladder prediction of approximately 1245 MeV. The definition anchors the T12 step of the Recognition framework by fixing the empirical value at the R = -18/4 rung. It feeds the hypothesis certificate H_charm_mass_match that records the sub-2% match for top, bottom, and charm sectors.
scope and limits
- Does not derive the numerical value from the phi-ladder equations.
- Does not incorporate QCD corrections for light quarks.
- Does not state units explicitly beyond the module's implicit MeV convention.
formal statement (Lean)
50def mass_charm_exp : ℝ := 1270