muon_relative_error
plain-language theorem explainer
The theorem shows the RS mass prediction for the muon at rung 13 deviates from the PDG experimental value by less than 4 percent. It is cited in the muon scorecard row and the overall mass verification certificate. The tactic proof rewrites via the auxiliary prediction equality, pulls the bounding interval, and closes the relative-error form with nlinarith after positivity and abs_lt rewrites.
Claim. Let $m_{\mu,\text{pred}}$ be the Recognition Science mass in MeV for the Lepton sector at rung 13 and let $m_{\mu,\text{exp}} = 105.6583755$ be the experimental muon mass. Then $\frac{|m_{\mu,\text{pred}} - m_{\mu,\text{exp}}|}{m_{\mu,\text{exp}}} < 0.04$.
background
In the Masses.Verification module experimental values are imported constants, not RS-derived. The RS mass function rs_mass_MeV computes $2^{B_{\text{pow}}} \phi^{-5} \phi^{r_0} \phi^r / 10^6$ in MeV for a sector and rung; for leptons this yields the explicit form $\phi^{57+r}/(2^{22}\times 10^6)$. The inductive Lepton type distinguishes the muon case. The auxiliary muon_pred is shown equal to rs_mass_MeV .Lepton 13 by muon_pred_eq, while muon_mass_bounds supplies the concrete interval 101.49 < muon_pred < 101.57.
proof idea
The tactic proof first rewrites the RS mass term via muon_pred_eq. It obtains the interval bounds from muon_mass_bounds and records positivity of m_mu_exp. It then rewrites the target inequality through div_lt_iff₀ and abs_lt, unfolds the experimental constant, and discharges both resulting conjuncts by nlinarith on the supplied bounds.
why it matters
The result populates the muon entry of mass_verification_cert_exists and supplies the middle conjunct of phi_ladder_verified, which asserts that the phi-ladder matches PDG data to the stated tolerances. It is also invoked directly by row_muon_pct. The underlying mass formula rests on the phi fixed point forced at T6 of the unified forcing chain and the eight-tick octave structure. The verification leaves open the origin of the experimental constants themselves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.