predicted_mass_mu_lower
plain-language theorem explainer
Lower bound 105 on the predicted muon mass follows from the electron structural mass interval and the phi-residue power lower bound. Lepton mass derivations in Recognition Science cite this to replace the muon axiom with a forced inequality. The proof unfolds the mass definition then chains the two upstream bounds inside a calc block with norm_num and nlinarith.
Claim. $105 < m_μ^pred$ where $m_μ^pred = m_struct · φ^{r_μ}$, $m_struct$ is the electron structural mass, and $r_μ$ is the predicted muon residue.
background
The T10 Necessity module forces the lepton ladder from the electron mass (T9) and geometric constants. Electron structural mass equals lepton yardstick times φ to the (electron rung minus 8), equivalently 2^{-22} φ^{51}, with proven bounds 10856 < m_struct < 10858. Predicted muon mass is this scale multiplied by φ to the power of the muon residue, where the residue is gap(1332) minus refined shift plus the electron-to-muon step.
proof idea
The tactic proof first simplifies predicted_mass_mu to the product of electron_structural_mass and phi^predicted_residue_mu. It pulls in structural_mass_bounds for the m_struct interval and phi_pow_residue_mu_lower for the 0.0097 lower bound on the phi power. A calc block then uses norm_num to verify 105 < 10856 * 0.0097, followed by nlinarith to conclude the product exceeds 105.
why it matters
This result is invoked by muon_mass_pred_bounds_proven to supply the full (105,107) interval that replaces the original axiom. It advances the T10 goal of deriving lepton masses from prior geometric results, including phi from T5 and the eight-tick octave. The interval stays wider than the observed 105.658 MeV because of residue propagation, leaving tighter residue bounds as an open refinement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.