predicted_mass_mu_lower_v2
plain-language theorem explainer
The theorem proves a strict lower bound of 105.5 on the predicted muon mass in MeV units. Researchers deriving lepton spectra from the Recognition Science forcing chain cite it to anchor the muon rung using only the electron structural mass and the golden-ratio residue. The proof rewrites the mass definition then combines the structural-mass lower bound with the phi-power lower bound via a two-step calculation and nlinarith.
Claim. $105.5 < m_μ^{pred}$ where $m_μ^{pred} = m_e^{struct} · φ^{r_μ}$, $m_e^{struct}$ is the electron structural mass, and $r_μ$ is the predicted muon residue.
background
In Recognition Science the lepton ladder is built from the electron structural mass, defined as the lepton yardstick scaled by φ to the electron rung minus the octave period. The predicted muon mass is the product of this structural mass and φ raised to the predicted residue, where the residue adds the electron-to-muon step (derived from 11 passive edges and α) to a base gap term. The module proves the full lepton ladder is forced from T9 by geometric constants: 11 passive edges, 6 cube faces, 17 wallpaper groups, and α, with no free parameters. Upstream, structural_mass_bounds supplies the interval 10856 < electron_structural_mass < 10858, while phi_pow_residue_mu_lower_v2 supplies 0.00972 < φ^{predicted_residue_mu}.
proof idea
The proof simplifies the definition of predicted_mass_mu to expose the product form. It obtains the structural-mass lower bound via structural_mass_bounds and the phi-power lower bound via phi_pow_residue_mu_lower_v2. A calc block first verifies 105.5 < 10856 * 0.00972 by norm_num, then applies nlinarith on the two lower bounds to lift the inequality to the actual electron_structural_mass * φ^{predicted_residue_mu}.
why it matters
This supplies the lower half of the interval in the downstream theorem muon_mass_pred_bounds_v2, which supports the T10 claim that the muon mass is forced from T9 within 2 percent relative error. It closes part of the necessity argument for the lepton ladder using the golden ratio from T4, the electron structural mass from T9, and the exact geometric constants E_passive = 11, cube faces = 6, and wallpaper groups = 17. The result removes one free-parameter axiom in the lepton-generation module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.