predicted_mass_mu
plain-language theorem explainer
The predicted muon mass is defined as the electron structural mass scaled by phi to the power of the predicted muon residue. Researchers deriving lepton hierarchies from the Recognition Science phi-ladder cite this when checking consistency with the observed muon mass. The definition is a direct algebraic scaling with no additional steps.
Claim. The predicted muon mass is given by $m_μ^{pred} = m_e^{struct} · φ^{r_μ}$, where $m_e^{struct}$ is the electron structural mass on the phi-ladder and $r_μ$ is the predicted muon residue.
background
The T10 Lepton Generations module isolates core definitions to break import cycles. Electron structural mass is the lepton yardstick times phi to the power (electron rung minus 8), giving the base mass on the phi-ladder. Predicted muon residue is the gap term (1332 minus refined shift) plus the electron-to-muon step. Mass is the real numbers in RS-native units.
proof idea
One-line definition that multiplies electron structural mass by phi raised to the predicted muon residue.
why it matters
This definition supplies the predicted muon mass for the bounds theorem muon_mass_pred_bounds and the main T10 result lepton_ladder_forced_from_T9, which derives the lepton ladder from T9 via passive edges, cube geometry, wallpaper groups, and alpha. It implements the mass formula yardstick times phi to the rung on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.