predicted_mass_tau
plain-language theorem explainer
The definition computes the predicted tau lepton mass by scaling the electron structural mass by phi to the power of the tau residue. Physicists checking the T10 lepton ladder predictions would cite this when comparing the result to the observed 1776.86 MeV value. It is realized as a direct product of the structural base and the phi exponent term.
Claim. $m_τ^{pred} = m_e^{struct} ⋅ ϕ^{r_τ}$, where $m_e^{struct}$ is the electron structural mass $Y ⋅ ϕ^{r_e - 8}$ and $r_τ$ is the predicted tau residue obtained by adding the muon-tau step to the muon residue.
background
The T10 Lepton Generations Definitions module isolates core mass expressions to break import cycles with necessity theorems. Electron structural mass is the lepton yardstick scaled by phi to the electron rung minus eight, giving the base mass on the phi-ladder. Predicted tau residue is defined as the muon residue plus the step_mu_tau term that encodes cube-face and wallpaper contributions.
proof idea
One-line definition that multiplies electron_structural_mass by phi raised to predicted_residue_tau, where the residue is itself the sum of predicted_residue_mu and step_mu_tau.
why it matters
Supplies the explicit value used by tau_mass_pred_bounds (which places the prediction in (1768, 1792) MeV) and tau_mass_step_hypothesis. It is invoked by the main theorem lepton_ladder_forced_from_T9, which derives the full ladder from T9, passive edges E_p=11, cube faces F=6, wallpaper groups W=17, and alpha. Realizes the Recognition Science mass formula on the lepton phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.