m_e_exp
plain-language theorem explainer
Experimental electron rest mass fixed at 0.51099895069 MeV (PDG 2024 central value). Anyone checking RS lepton predictions against data cites this constant as the denominator and target of relative-error bounds. It is a bare real literal with no proof obligation.
Claim. The PDG 2024 central value of the electron rest mass is $m_e^{\mathrm{exp}} = 0.51099895069\,\mathrm{MeV}$.
background
The MassComparison module is quarantined from the certified RS surface: it imports external PDG numbers and compares them to mass predictions built on the φ-ladder. The RS formula is $m(\mathrm{species}) = \mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r_{\mathrm{species}}}$, with coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$ and sector yardsticks fixed by cube geometry.
This constant is the electron entry in that comparison table. Sibling literals supply muon, tau, and light-quark experimental masses and their one-sigma widths. Units are MeV throughout; the parenthetical (16) in the doc-comment is the PDG uncertainty and is not stored in the real itself.
proof idea
Definition by numeric literal. No tactics, no lemmas: the real is set equal to 0.51099895069. Downstream proofs unfold the name and discharge inequalities by norm_num.
why it matters
Anchors every electron-facing verification claim. electron_relative_error proves the RS lepton prediction at rung 2 lies within 0.3% of this value. MassVerificationCert packages that percent bound with absolute interval checks. phi_ladder_verified aggregates electron, muon, and tau relative errors to certify the φ-ladder ansatz against PDG. Ratio definitions ratio_mu_e_exp and ratio_tau_e_exp divide the corresponding experimental masses by this constant, so muon/electron and tau/electron bounds inherit it directly.
In the broader framework the electron is the empirical mass anchor on the φ-ladder; matching it at the sub-percent level is the first quantitative check that the T6 self-similar fixed point and the rung integers reproduce real particle data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.