predicted_mass_tau
plain-language theorem explainer
The definition computes the predicted tau mass by scaling the electron structural mass by phi to the power of the accumulated tau residue. Researchers verifying T10 lepton ladder predictions against measured values would cite it when propagating bounds from the base electron rung. It is a direct one-line algebraic composition of the structural base with the residue sum from the muon step.
Claim. The predicted tau mass is $m_τ^{pred} = m_e^{struct} ⋅ ϕ^{r_τ}$, where $m_e^{struct}$ is the electron structural mass $Y ⋅ ϕ^{r_e-8}$ and $r_τ$ is the residue obtained by adding the muon-to-tau step to the muon residue.
background
The T10 Lepton Generations Definitions module isolates core mass expressions to break import cycles with theorems. Electron structural mass is the base scale lepton_yardstick ⋅ ϕ^(electron_rung - 8), representing the phi-ladder yardstick shifted by the octave period. Predicted residue tau is defined as predicted residue mu plus step mu tau, accumulating the geometric increments from passive edges, cube faces, and wallpaper groups.
proof idea
One-line definition that multiplies electron structural mass by phi raised to the power of predicted residue tau, where the residue is itself the sum of the muon residue and the muon-to-tau step.
why it matters
This supplies the predicted tau mass used by tau_mass_pred_bounds and tau_mass_step_hypothesis to confirm agreement with 1776.86 MeV within 1% relative error. It is a direct input to the main theorem lepton_ladder_forced_from_T9, which derives the full ladder from T9 via passive edges E_p=11, faces F=6, wallpaper groups W=17, and alpha. In the Recognition Science framework it realizes the T10 mass formula on the phi-ladder for the third generation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.