electron_pred
plain-language theorem explainer
electron_pred supplies the Recognition Science prediction for the electron mass as a concrete real number on the phi-ladder. Particle physicists verifying lepton mass ratios against experimental data cite this definition when constructing the muon-to-electron ratio bounds. The definition directly encodes the general lepton mass formula m(Lepton, r) = φ^{57+r} / (2^{22} × 10^6) evaluated at rung 59.
Claim. The predicted electron mass is given by $m_e^pred = φ^{59} / (2^{22} × 10^6)$ in MeV, where φ is the golden ratio supplied by the Recognition Science constants bundle.
background
The module Masses.Verification quarantines experimental PDG values as imported constants and focuses on machine-verified comparisons of RS predictions. For leptons the mass formula is m(Lepton, r) = φ^{57+r} / (2^{22} × 10^6) in MeV, with the electron corresponding to rung 59. The upstream Constants structure from LawOfExistence bundles the phi value along with other CPM constants such as Knet.
proof idea
This is a direct noncomputable definition that instantiates Constants.phi raised to the 59th power and divides by the fixed denominator 4194304000000. No lemmas are applied; the expression matches the lepton sector formula exactly.
why it matters
electron_pred is the base input for the muon ratio predictions in MuRatioScoreCard, including the certified bounds 1898 < mu_pred < 1904 and the error check against mu_codata. It realizes the phi-ladder mass formula (T6 phi fixed point, T7 eight-tick octave) for the lightest lepton, enabling the D=3 spatial dimension consistency checks in the Recognition framework. The definition closes the verification path for the electron mass prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.