muon_pred_eq
plain-language theorem explainer
The muon_pred_eq theorem equates the Recognition Science mass formula for the lepton sector at rung 13 to the explicit closed-form prediction phi^70 divided by 4194304000000 in MeV. A physicist checking the phi-ladder against PDG data would cite this to substitute the prediction into relative-error bounds for the muon. The proof is a one-line wrapper that instantiates the auxiliary lemma lepton_pred_eq_aux at the matching exponent and rung, discharging the arithmetic relation by norm_num.
Claim. The Recognition Science mass in MeV for the lepton sector at rung 13 equals the explicit prediction $phi^{70}/4194304000000$.
background
The Verification module compares RS mass predictions to PDG experimental values. The rs_mass_MeV definition computes (2)^(B_pow s) * phi^(-5) * phi^(r0 s) * phi^r / 10^6, where the lepton sector uses B_pow = -22 and r0 = 62. This specializes to m(Lepton, r) = phi^(57 + r) / (2^22 * 10^6) MeV. The Lepton inductive type tags the electron (rung 2), muon (rung 13), and tau (rung 20) positions on the ladder. The muon_pred definition supplies the closed-form value phi^70 / 4194304000000 directly. The equality rests on the auxiliary lemma lepton_pred_eq_aux, which reduces the general rs_mass_MeV expression to the explicit power once the exponent relation (-5 + 62 + r = n) holds.
proof idea
The proof is a one-line wrapper that applies lepton_pred_eq_aux at n = 70 and r = 13, discharging the hypothesis (-5 + 62 + 13 = 70) by norm_num.
why it matters
This equality is invoked by muon_relative_error to establish the relative-error bound below 0.04 and by phi_ladder_verified to confirm the full lepton ladder matches PDG tolerances within the stated percentages. It supplies the concrete link between the general mass formula and the muon-specific prediction, closing one verification step in the T5-T8 forcing chain for mass spectra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.