phi_ladder_verified
plain-language theorem explainer
The phi-ladder mass formula reproduces the electron, muon and tau masses to within 0.3 percent, 4 percent and 3 percent of PDG values. Researchers comparing discrete scale models to experiment would reference this numerical check. The term proof rewrites each predicted mass via its defining equation and invokes the corresponding relative-error lemma.
Claim. The relative errors satisfy $|m_e^pred - m_e^exp|/m_e^exp < 0.003$, $|m_μ^pred - m_μ^exp|/m_μ^exp < 0.04$ and $|m_τ^pred - m_τ^exp|/m_τ^exp < 0.03$, where the predictions are given by the Recognition Science lepton mass formula $m(Lepton,r) = φ^{57+r}/(2^{22}×10^6)$ MeV evaluated at rungs 2, 13 and 19.
background
The module treats experimental PDG values as imported constants, quarantined from the certified Recognition Science surface. The lepton-sector formula is $m(Lepton,r) = φ^{57+r}/(2^{22}×10^6)$ MeV, with B_pow = -22 and r0 = 62. The inductive type Lepton enumerates the three charged states; the functions electron_pred, muon_pred and tau_pred are defined via rs_mass_MeV applied to those states at the indicated rungs. Upstream results supply the rung constant, the phi scaling operation, and the structural bridge that packages model state for traceability.
proof idea
The term proof applies three rewrite rules that substitute the explicit definitions of the predicted masses from their equality lemmas (electron_pred_eq, muon_pred_eq, tau_pred_eq), then applies the exact tactic to the triple of pre-established relative-error bounds.
why it matters
This verification closes the lepton sector of the mass ladder and supersedes the earlier mass_ladder_assumption. It confirms that the phi-ladder formula, derived from J-uniqueness and the phi fixed point (T5-T6), reproduces observed lepton masses to the stated precision. No downstream theorems depend on it yet; it serves as a standalone numerical anchor for the Recognition Science mass predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.