predicted_mass_mu
The definition supplies the predicted muon mass by scaling the electron structural mass with phi to the power of the muon residue. Researchers deriving lepton masses from the Recognition Science forcing chain cite it to obtain the numerical interval around 105-107 in native units. It is realized as a direct algebraic product of the precomputed structural mass and the exponential phi term.
claimThe predicted muon mass is defined by $m_μ = m_e^{struct} · ϕ^{r_μ}$, where $m_e^{struct}$ is the electron structural mass $Y · ϕ^{r-8}$ and $r_μ$ is the muon residue combining the gap term with the electron-to-muon step.
background
The T10 lepton generations module isolates core definitions to break import cycles while supplying the mass ladder. The electron structural mass is the lepton yardstick scaled by phi to the power of the rung offset from the octave period. The muon residue is formed from a fixed gap of 1332 minus a refined shift, plus the passive step from electron to muon. Upstream results establish the structural mass via the electron mass module and the residue via the same module's gap and step components.
proof idea
This is a one-line definition that multiplies the electron structural mass by phi raised to the predicted muon residue.
why it matters in Recognition Science
It feeds the bounds theorem establishing the interval (105, 107) and the main T10 theorem lepton_ladder_forced_from_T9, which derives the full lepton ladder from T9 using passive edges E_p = 11, cube faces F = 6, wallpaper groups W = 17, and the fine-structure constant. The definition closes the muon mass prediction inside the Recognition Science phi-ladder and eight-tick octave structure.
scope and limits
- Does not claim exact numerical match to the experimental muon mass without the stated 2% relative error tolerance.
- Does not derive the residue or step values; these are imported from sibling definitions.
- Does not extend the scaling formula to non-lepton particles or higher generations beyond tau.
- Does not incorporate radiative corrections or running couplings beyond the base phi exponent.
formal statement (Lean)
59noncomputable def predicted_mass_mu : ℝ :=
proof body
Definition body.
60 electron_structural_mass * phi ^ predicted_residue_mu
61
62/-- Predicted Tau Mass. -/
used by (22)
-
muon_mass_pred_bounds -
muon_mass_step_hypothesis -
lepton_ladder_forced_from_T9 -
lepton_ladder_forced_from_T9_v2 -
muon_mass_pred_bounds_proven -
muon_mass_pred_bounds_tight -
muon_mass_pred_bounds_v2 -
phi_pow_residue_tau_bounds -
predicted_mass_mu_lower -
predicted_mass_mu_lower_tight -
predicted_mass_mu_lower_v2 -
predicted_mass_mu_upper -
predicted_mass_mu_upper_tight -
predicted_mass_mu_upper_v2 -
muon_mass_pred_bounds -
muon_mass_step_hypothesis -
predicted_mass_mu -
lepton_ladder_forced_from_T9 -
muon_mass_pred_bounds_proven -
phi_pow_residue_tau_bounds -
predicted_mass_mu_lower -
predicted_mass_mu_upper