mass_ref_MeV
plain-language theorem explainer
This supplies the observed electron mass of 0.510998950 MeV as a reference constant for residue extraction in the T9 derivation. Workers on the electron mass formula cite it when computing the logarithmic deviation from the structural prediction on the phi-ladder. The assignment is a direct constant definition drawn from PDG data for diagnostic use only, with no further reduction.
Claim. The reference observed electron mass equals $0.510998950$ MeV.
background
The module isolates core definitions for the T9 electron mass derivation to break import cycles. It relies on the phi-ladder mass formula (yardstick times phi to the power of rung minus 8 plus gap of Z) and the J-cost function from the forcing chain T0-T8. The constant acts as a calibration seam: MeV units are a display convention only, while the RS-native core remains dimensionless. Upstream, the from theorem reduces seven axioms to four structural conditions plus three definitional facts, supplying the primitive distinction layer that underpins all mass topology.
proof idea
Direct constant definition with no lemmas applied and no tactic steps. It assigns the real number 0.510998950 outright to serve as input for the residue computation.
why it matters
This anchors the comparison step in the T9 Electron Mass Formula. It feeds the electron_residue definition, which extracts the logarithmic deviation log_phi(m_obs / m_struct) with audited value -20.70596. The placement supports validation of the phi-ladder prediction against observation and closes the diagnostic loop for the mass formula yardstick and rung parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.