muon_pred
plain-language theorem explainer
The predicted muon mass in the Recognition Science phi-ladder is defined as the golden ratio raised to the 70th power divided by 4194304000000 in MeV units. Researchers verifying lepton masses against PDG 2024 data would cite this quantity when checking model accuracy. The definition arises by direct substitution of rung index 13 into the general lepton formula with no lemmas or reductions applied.
Claim. The Recognition Science prediction for the muon mass is given by $m_μ = φ^{70} / 4194304000000$ MeV, where $φ$ is the golden ratio from the Constants bundle and the expression follows the lepton formula $m(Lepton, r) = φ^{57+r} / (2^{22} × 10^6)$ at $r = 13$.
background
The Masses.Verification module compares Recognition Science mass predictions to PDG experimental values, treating the latter as imported constants rather than derived quantities. For the lepton sector the formula is $m(Lepton, r) = φ^{57+r} / (2^{22} × 10^6)$ MeV, with the muon assigned to rung $r = 13$. This produces the exponent 70 and the denominator 4194304000000, which equals $2^{22} × 10^6$ times the unit scaling.
proof idea
The declaration is a direct definition with an empty proof body. It encodes the lepton mass formula at rung 13 by explicit exponentiation of the golden ratio followed by division by the normalization factor. No lemmas or tactics are invoked.
why it matters
This definition is referenced by MassVerificationCert to certify that the predicted muon mass lies between 101.49 and 101.57 MeV with relative error under 0.04. It also supports the explicit bounds theorem and the equality to the general rs_mass_MeV function at Lepton 13. In the Recognition framework it realizes the phi-ladder mass formula for the muon, supporting verification against PDG data and instantiating the self-similar fixed point phi from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.