predicted_mass_mu_upper_tight
plain-language theorem explainer
predicted_mass_mu_upper_tight shows the predicted muon mass lies strictly below 106.5 in Recognition Science units. Researchers deriving lepton masses from the phi-ladder and electron structural mass cite it to close the upper end of the muon interval. The proof unfolds the mass definition then chains the structural-mass upper bound with the phi-residue power bound via nlinarith and norm_num.
Claim. $m_μ^pred < 106.5$, where $m_μ^pred = m_struct · φ^{r_μ}$, $m_struct$ is the electron structural mass (bounded 10856 to 10858), and $r_μ$ is the predicted muon residue.
background
The module proves T10 necessity results for the lepton ladder, replacing axioms with derived inequalities that force muon and tau masses from the electron mass (T9) and geometric constants. electron_structural_mass is defined as lepton_yardstick · φ^(electron_rung − octave_period) and satisfies 10856 < electron_structural_mass < 10858 by structural_mass_bounds. predicted_mass_mu equals electron_structural_mass · φ^predicted_residue_mu, with the residue built from gap(1332), refined_shift, and step_e_mu.
proof idea
The tactic proof first applies simp to unfold predicted_mass_mu. It then obtains the structural-mass upper bound from structural_mass_bounds and the phi-power upper bound from phi_pow_residue_mu_upper. A calc block bounds the product below 10858 · 0.0098 by nlinarith on those two facts, after which norm_num confirms the result is less than 106.5.
why it matters
This supplies the upper half of the interval used by muon_mass_pred_bounds_tight to obtain the tight range (105.3, 106.5). It advances the T10 necessity argument that the lepton ladder is forced from the electron structural mass, phi (T6), and cube-derived steps, closing one link in the chain from T0–T8 forcing to observable lepton masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.