predicted_mass_mu_lower
plain-language theorem explainer
predicted_mass_mu_lower proves that the predicted muon mass exceeds 105 MeV in the Recognition Science lepton ladder. A physicist deriving forced lepton masses from geometric constants would cite this to anchor the muon prediction above the threshold. The short tactic proof unfolds the mass definition then chains the structural mass interval with a phi-power residue lower bound via calc and nlinarith.
Claim. Let $m_ {struct}$ be the electron structural mass and $r_ {mu}$ the predicted muon residue. Then $105 < m_{struct} · φ^{r_{mu}}$.
background
The RRF.Physics.LeptonGenerations.Necessity module addresses T10, proving the lepton ladder is forced from the T9 electron mass result and geometric constants derived earlier. The predicted muon mass is defined as the product of the electron structural mass and φ raised to the predicted residue power. The structural mass equals the lepton yardstick times φ to the power of (electron rung minus the octave period of 8). The residue combines a gap term with the electron-to-muon step function from cube geometry and α.
proof idea
The proof first simplifies the definition of predicted_mass_mu. It invokes structural_mass_bounds to obtain the interval 10856 < m_struct < 10858 and phi_pow_residue_mu_lower to obtain 0.0097 < φ^residue_mu. A calc block establishes 105 < 10856 * 0.0097, after which nlinarith combines the two interval facts to conclude the target inequality.
why it matters
This result is used directly in muon_mass_pred_bounds_proven, which replaces an earlier axiom for the muon mass prediction. It forms part of the T10 necessity proofs showing muon and tau masses follow from the electron structural mass, cube geometry constants, and the golden ratio fixed point. The framework derives these from the eight-tick octave structure. Current intervals give (105.3, 106.4), wider than the observed 105.658 MeV, leaving an open question on tighter phi bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.