electron_pred_eq
The equality shows that the Recognition Science mass formula for leptons at rung 2 reproduces the explicit phi-power expression used for the electron. Researchers checking the phi-ladder against PDG data cite this to justify direct substitution in relative-error bounds. The proof is a one-line wrapper that feeds the exponent 59 and rung 2 into the auxiliary lemma, with norm_num discharging the arithmetic check.
claimThe Recognition Science mass formula applied to the lepton sector at rung 2 equals the explicit prediction: $2^{-22} phi^{59} / 10^6$ in MeV, or equivalently $phi^{59}/(2^{22} times 10^6)$.
background
The module verifies mass predictions against PDG 2024 values while treating experimental masses as imported constants. The general mass formula rs_mass_MeV(s, r) expands to 2 to the B_pow(s) times phi to the -5 times phi to the r0(s) times phi to the r, all divided by 10^6. For the lepton sector the constants are B_pow = -22 and r0 = 62, so the formula simplifies to phi to the power 57 plus r over 2^22 times 10^6 in MeV. The explicit electron prediction is the r = 2 case, phi^59 over 4194304000000. The Lepton inductive type enumerates electron, muon, tau and neutrinos.
proof idea
The proof is a one-line wrapper that applies the auxiliary lemma lepton_pred_eq_aux to the concrete values 59 for the combined exponent and 2 for the rung, then uses norm_num to confirm -5 + 62 + 2 equals 59.
why it matters in Recognition Science
It supplies the substitution step required by the downstream theorems electron_relative_error and phi_ladder_verified, which bound the relative deviation of the predicted electron mass from the experimental value. The declaration therefore closes the explicit-to-general link inside the lepton-sector verification block of the Masses module. Within the Recognition Science framework it supports checking the phi-ladder mass formula (T6 fixed point, T7 eight-tick octave) against external data while leaving the experimental inputs quarantined.
scope and limits
- Does not derive the experimental electron mass from Recognition Science axioms.
- Applies only to rung 2 in the lepton sector.
- Does not cover hadrons or other sectors without further lemmas.
- Does not itself compute or state error bounds.
Lean usage
rw [electron_pred_eq]formal statement (Lean)
73theorem electron_pred_eq : rs_mass_MeV .Lepton 2 = electron_pred :=
proof body
One-line wrapper that applies lepton_pred_eq_aux.
74 lepton_pred_eq_aux 59 2 (by norm_num)
75