muon_mass_pred_bounds_proven
plain-language theorem explainer
The predicted muon mass satisfies 105 < m_mu_pred < 107 in RS-native units. Researchers deriving lepton hierarchies from the forcing chain cite this to replace an earlier axiom with a derived interval. The proof is a one-line wrapper that pairs the separately proven lower and upper bounds on the product of structural mass and phi to the residue power.
Claim. $105 < m_μ^{pred} < 107$, where $m_μ^{pred} = m_e^{struct} ⋅ φ^{r_μ}$ with $m_e^{struct}$ the electron structural mass from T9 and $r_μ$ the predicted residue for the muon step.
background
The T10 module proves the lepton ladder is forced from T9. Predicted muon mass is defined as electron structural mass times phi to the predicted residue power. Upstream results give structural mass in (10856, 10858) and the relevant phi power in (0.0097, 0.0098), so the product lies in (105.3, 106.4). The module replaces axioms for muon and tau masses using geometric constants: passive edges E_p = 11, cube faces F = 6, wallpaper groups W = 17, and alpha from T6. All steps trace to cube geometry and the eight-tick structure.
proof idea
One-line wrapper that applies conjunction introduction to the lower bound theorem and the upper bound theorem. The lower bound uses structural_mass_bounds together with phi_pow_residue_mu_lower; the upper bound uses the same structural bounds with the matching upper phi power result.
why it matters
This result replaces an axiom and feeds directly into muon_mass_pred_bounds and the main T10 theorem lepton_ladder_forced_from_T9. The latter asserts that muon and tau masses are fixed by electron structural mass, passive edges, cube faces, wallpaper groups, and alpha. It closes part of the necessity argument in the forcing chain after T9, confirming the muon lies on the phi-ladder with relative error under 2 percent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.