phi_ladder_verified
plain-language theorem explainer
The phi-ladder lepton mass predictions match PDG experimental values to relative tolerances of 0.3 percent for the electron, 4 percent for the muon, and 3 percent for the tau. Recognition Science mass-model users cite this result to confirm the integer-rung formulas before invoking them in larger calculations. The term proof rewrites each prediction via its defining equality and applies three pre-established relative-error bounds.
Claim. Let $m_e^{\rm pred}=\phi^{59}/(2^{22}\times10^6)$ MeV, $m_\mu^{\rm pred}=\phi^{70}/(2^{22}\times10^6)$ MeV and $m_\tau^{\rm pred}=\phi^{76}/(2^{22}\times10^6)$ MeV be the Recognition-Science predictions at the indicated rungs. Then $|m_e^{\rm pred}-m_e^{\rm exp}|/m_e^{\rm exp}<0.003$, $|m_\mu^{\rm pred}-m_\mu^{\rm exp}|/m_\mu^{\rm exp}<0.04$ and $|m_\tau^{\rm pred}-m_\tau^{\rm exp}|/m_\tau^{\rm exp}<0.03$.
background
The module treats experimental lepton masses as imported constants, quarantined from the certified Recognition-Science surface. The lepton-sector formula is $m({\rm Lepton},r)=\phi^{57+r}/(2^{22}\times10^6)$ MeV. The inductive type Lepton enumerates electron, muon and tau (with the remaining neutrinos unused here). The sibling definitions rs_mass_MeV, electron_pred_eq, muon_pred_eq and tau_pred_eq supply the concrete rung assignments (r=2,13,19) and the equality lemmas that convert the abstract predictions into the numerical expressions appearing in the statement.
proof idea
The term proof first rewrites each of electron_pred, muon_pred and tau_pred by the symmetric form of its defining equality (electron_pred_eq.symm etc.). It then applies the exact constructor to the three pre-proved relative-error inequalities electron_relative_error, muon_relative_error and tau_relative_error.
why it matters
The declaration supplies the direct numerical verification that the phi-ladder model reproduces PDG values inside the stated tolerances, thereby superseding the earlier mass_ladder_assumption. It closes the lepton sector of the Masses.Verification module and stands as a terminal check before any downstream use of the rs_mass_MeV formulas. The result touches the open question of gap-corrected quark masses, which the module explicitly leaves for future RSBridge calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.