electron_pred
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value of phi from the functional equation.
- Does not incorporate experimental uncertainty into the prediction itself.
- Does not extend to baryon or other non-lepton mass predictions.
- Does not claim exact equality with the measured electron mass.
formal statement (Lean)
48noncomputable def electron_pred : ℝ := Constants.phi ^ (59 : ℕ) / 4194304000000