predicted_mass_mu
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.