predicted_mass_mu_upper_v2
plain-language theorem explainer
The theorem establishes that the muon mass predicted from the electron structural mass scaled by a golden-ratio power is strictly less than 105.9 in the project's units. Researchers deriving lepton spectra from the Recognition forcing chain would cite it to confirm the muon prediction lies inside the observed window. The proof reduces the claim to a product of two independently bounded factors via linear arithmetic and then checks the numerical threshold.
Claim. The predicted muon mass satisfies $m_μ^{pred} < 105.9$, where $m_μ^{pred} := m_e^{struct} · φ^{r_μ}$ with $m_e^{struct}$ the structural electron mass and $r_μ$ the predicted muon residue.
background
Module T10 proves the lepton ladder is forced from the electron structural mass (T9) and geometric constants obtained from cube geometry together with the eight-tick octave. The structural mass is defined as the lepton yardstick times φ raised to (electron rung minus octave period) and equals 2^{-22} · φ^{51} in closed form. The predicted muon mass is the product of this structural mass and φ raised to the muon residue, where the residue combines a gap term with a step function derived from E_passive, cube faces, and wallpaper count W.
proof idea
The tactic proof first rewrites the predicted mass to the explicit product of electron structural mass and φ to the muon-residue power. It invokes the structural-mass upper bound (less than 10858) and the phi-power upper bound (less than 0.00975), then applies nlinarith to obtain the product less than 10858 · 0.00975. A final norm_num step confirms the product lies below 105.9.
why it matters
This supplies the upper half of the muon-mass interval assembled in the downstream theorem muon_mass_pred_bounds_v2. It advances the T10 program of replacing the original lepton axioms with proven inequalities that rest only on the electron structural mass, the golden-ratio fixed point (T6), the eight-tick period (T7), and the Recognition Composition Law. The result therefore closes one link in the chain from T0 forcing through T8 spatial dimension to concrete lepton masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.