predicted_mass_mu_upper
plain-language theorem explainer
The predicted muon mass, formed as the electron structural mass scaled by phi to the power of the muon residue, is strictly less than 107 in Recognition Science units. Researchers deriving lepton hierarchies from the forcing chain would cite this to close the upper end of the forced interval. The tactic proof unfolds the mass definition then chains the structural mass interval with the phi-power residue bound via nlinarith and norm_num.
Claim. $m_μ^{pred} < 107$, where $m_μ^{pred} = m_{struct} · φ^{r_μ}$, $m_{struct}$ is the electron structural mass, and $r_μ$ is the predicted muon residue.
background
Module T10 proves the lepton ladder is forced from T9 (electron mass) and geometric constants fixed by cube geometry together with the eight-tick octave. The electron structural mass equals the lepton yardstick times phi raised to (electron rung minus octave period) and is a purely geometric constant equal to 2^{-22} · φ^{51}. The predicted muon mass multiplies this structural mass by phi to the power of the predicted residue mu, which combines the gap at 1332, refined shift, and the electron-to-muon step function.
proof idea
The tactic proof first applies simp to unfold predicted_mass_mu into electron_structural_mass * phi ^ predicted_residue_mu. It then obtains the interval (10856, 10858) from structural_mass_bounds and the bound phi ^ predicted_residue_mu < 0.0098 from phi_pow_residue_mu_upper. A calc block with nlinarith combines these to reach the product less than 10858 * 0.0098, after which norm_num confirms the value is below 107.
why it matters
This supplies the upper half of the interval in muon_mass_pred_bounds_proven, which replaces the original axiom for the muon prediction. It advances T10 necessity by showing the muon mass is forced from the electron structural mass (T9) and the phi-ladder fixed by T5-T8, including the Recognition Composition Law and D=3. The parent theorem muon_mass_pred_bounds_proven states that the bounds replace the axiom with proven inequalities after interval propagation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.