muon_mass_bounds
plain-language theorem explainer
The theorem establishes that the Recognition Science muon mass prediction at phi-ladder rung 70 lies strictly between 101.49 and 101.57. Analysts assembling lepton mass checks against PDG data would cite this bound when building verification certificates. The proof reduces the claim to numerical comparisons by unfolding the prediction and chaining pre-established inequalities on phi to the power 70 with direct scaling calculations.
Claim. Let $m = 2^{22} times 10^6$. Let $mu_pred = phi^{70} / m$. Then $101.49 < mu_pred < 101.57$.
background
The module sets out lepton mass predictions via the formula m(Lepton, r) = phi^{57+r} / (2^{22} times 10^6) in MeV for B_pow = -22 and r0 = 62. The muon corresponds to r = 13, producing the exponent 70 and the denominator 4194304000000. Constants.phi supplies the golden-ratio base for this scaling. Upstream, the structure Constants collects CPM parameters with a nonnegativity condition on Knet. The lemmas phi70_gt and phi70_lt supply the concrete bounds 425698000000000 < phi^{70} and phi^{70} < 426011000000000 after rewriting via the golden-ratio identity.
proof idea
The tactic proof unfolds the definition of the prediction to expose the division. Constructor splits the conjunction into two goals. The lower bound rewrites via lt_div_iff, then a calc block shows the scaled 101.49 lies below 425698000000000 which lies below phi^{70} by phi70_gt. The upper bound rewrites via div_lt_iff, then chains phi^{70} below 426011000000000 which lies below the scaled 101.57 by phi70_lt together with norm_num.
why it matters
The bound is invoked inside the mass verification certificate that packages electron, muon and tau intervals, and inside the muon relative error theorem that derives a deviation under 4 percent. It supplies the machine-checked verification step for the muon in the module comparing predictions to PDG 2024 values. In the framework this supports the phi fixed point and the integer-rung mass formula on the ladder without deriving the experimental inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.