m_p_exp
plain-language theorem explainer
The definition supplies the PDG experimental proton mass of 938.272 MeV as a numeric constant for comparison. It is cited by the proton_relative_error theorem that bounds the discrepancy with the RS phi-ladder prediction at rung 48. The definition is a bare literal assignment with no reduction steps or lemmas.
Claim. The experimental proton mass is defined as $m_p^exp = 938.272$ MeV.
background
The Masses.Verification module imports experimental PDG values as constants quarantined from the certified RS surface. These anchors enable direct numerical comparison with predictions derived from the phi-ladder mass formula, where the proton is treated as binding-dominated near rung 48. The module references PDG 2024 for the source datum and notes that lepton predictions follow the explicit form $m(Lepton,r) = phi^{57+r} / (2^{22} times 10^6)$ MeV while the proton case incorporates non-perturbative QCD effects between rungs.
proof idea
This is a direct constant definition with no lemmas applied and no tactics executed.
why it matters
The constant anchors the proton_relative_error theorem, which shows the RS prediction at rung 48 lies within 3.5 percent of experiment after accounting for binding. It supports the framework claim that masses sit on the phi-ladder with integer rungs and small corrections, consistent with T6 self-similar fixed point and T8 D=3. The module doc flags these values as non-derived, leaving open the question of a fully RS-internal derivation of the proton mass scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.