muon_mass_pred_bounds_v2
plain-language theorem explainer
The theorem shows that the predicted muon mass lies strictly between 105.5 and 105.9. Researchers closing the lepton mass hierarchy from Recognition Science constants would cite this when replacing the muon mass axiom in the T10 necessity argument. The proof is a one-line term that pairs the separately proved lower and upper bounds on the same quantity.
Claim. Let $m_e$ denote the electron structural mass and let $r_μ$ denote the predicted residue for the muon. Then the predicted muon mass $m_μ^pred = m_e · φ^{r_μ}$ satisfies $105.5 < m_μ^pred < 105.9$.
background
The module establishes T10 necessity: the lepton ladder is forced from T9 (electron mass) together with cube geometry and the golden ratio. The quantity predicted_mass_mu is defined as electron_structural_mass multiplied by phi raised to the power of the predicted residue for the muon. Upstream results supply the structural mass bounds from ElectronMass.Necessity and the separate lower and upper inequalities on the phi-power term.
proof idea
The proof is a term-mode constructor that directly supplies the pair consisting of the lower-bound theorem and the upper-bound theorem.
why it matters
This bound is invoked by the parent theorem lepton_ladder_forced_from_T9_v2, which tightens the relative error on both muon and tau predictions to under 0.2 percent. It completes one half of the T10 step that derives the full lepton ladder from T9, the passive-edge count 11, the face count 6, the wallpaper count 17, and alpha. The result therefore removes an axiom that previously stood between the electron mass and the observed muon mass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.