muon_relative_error
plain-language theorem explainer
The Recognition Science lepton mass prediction at rung 13 lies within 4 percent of the experimental muon mass. Particle physicists auditing discrete mass ladders would cite this result when certifying the phi-ladder against PDG data. The proof rewrites the predicted mass to an auxiliary expression, invokes explicit numerical bounds, and resolves the relative error inequality via linear arithmetic.
Claim. $|m_{RS}(Lepton,13) - 105.6583755| / 105.6583755 < 0.04$, where $m_{RS}(Lepton,13)$ denotes the Recognition Science mass in MeV given by the phi-ladder formula $2^{B_{pow}} phi^{-5} phi^{r_0} phi^{13} / 10^6$ for the lepton sector.
background
The module compares Recognition Science mass predictions to PDG experimental values, importing the latter as constants rather than deriving them. For leptons the formula is $m(Lepton, r) = phi^{57+r} / (2^{22} times 10^6)$ in MeV. The definition rs_mass_MeV implements this expression using powers of the golden ratio phi together with a sector-dependent base-2 exponent and offset rung. Upstream results include the equality muon_pred_eq that identifies the rung-13 case with the auxiliary muon_pred, and the bounds theorem muon_mass_bounds that places muon_pred strictly between 101.49 and 101.57.
proof idea
The tactic proof rewrites the left-hand side with muon_pred_eq to replace rs_mass_MeV .Lepton 13 by muon_pred. It obtains the interval bounds on muon_pred from muon_mass_bounds and establishes positivity of m_mu_exp. The inequality is then rewritten using the division and absolute-value lemmas, after which unfolding the experimental mass and applying nlinarith to the bounds closes both sides of the resulting conjunction.
why it matters
This theorem supplies the muon error bound required by the mass verification certificate and by the overarching phi_ladder_verified statement, which confirms that electron, muon and tau predictions all satisfy their percentage tolerances. It thereby completes one concrete check that the phi-ladder reproduces PDG masses to the declared accuracies in the lepton sector. The result is invoked directly by row_muon_pct to record the four-percent agreement for the muon.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.