electron_mass_bounds
plain-language theorem explainer
The RS lepton mass prediction for the electron, given by phi^59 divided by 2^22 times 10^6 in MeV, lies strictly between 0.5098 and 0.5102. Researchers checking the phi-ladder mass formulas against PDG data would cite this result when building verification certificates. The proof unfolds the definition, splits the conjunction, and reduces each side via division lemmas plus the pre-proved phi^59 bounds.
Claim. $0.5098 < {phi^{59}} / (2^{22} times 10^{6}) < 0.5102$, where $phi$ is the golden ratio and the denominator implements the lepton-sector normalization with rung offset 2.
background
The module compares RS mass predictions for leptons to PDG 2024 experimental values. The lepton formula is m(Lepton, r) = phi^{57+r} / (2^{22} times 10^6) MeV. For the electron at r=2 this produces the electron_pred definition as Constants.phi^59 / 4194304000000.
proof idea
Unfold electron_pred then apply constructor. Rewrite the left inequality with lt_div_iff_0 and finish via a calc block that invokes norm_num followed by phi59_gt. The right inequality is symmetric: rewrite with div_lt_iff_0, apply phi59_lt, and close with norm_num.
why it matters
This bound supplies the electron_in_range field for mass_verification_cert_exists and for muRatioScoreCardCert_holds. It also feeds electron_pred_pos, mu_pred_lower, and mu_pred_upper. The result closes the electron rung verification on the phi-ladder inside the lepton sector (B_pow = -22), consistent with the T6 self-similar fixed point and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.