tau_mass_pred_bounds_v2
plain-language theorem explainer
The predicted tau lepton mass in Recognition Science satisfies 1774 < predicted_mass_tau < 1779. Researchers deriving forced lepton hierarchies from the electron structural mass and phi-ladder steps would cite this to confirm the third-generation bound. The proof is a direct conjunction of the separately established lower and upper inequalities on electron_structural_mass times phi to the tau residue power.
Claim. Let $m_τ^{pred} = m_e^{struct} ⋅ ϕ^{r_τ}$ denote the predicted tau mass. Then $1774 < m_τ^{pred} < 1779$.
background
The module on T10 Necessity derives the lepton ladder from the electron structural mass (from ElectronMass.Necessity) via phi-powered steps fixed by cube geometry, alpha, and pi. The predicted tau mass is defined as electron_structural_mass multiplied by phi raised to the predicted tau residue. Upstream results include the Lepton inductive type distinguishing the three charged generations and the separate lower and upper bound theorems that invoke structural_mass_bounds together with phi power inequalities for the tau residue.
proof idea
This is a one-line wrapper that applies the pair constructor to the lower bound theorem for the predicted tau mass and the upper bound theorem for the predicted tau mass.
why it matters
The bound is invoked by the main theorem lepton_ladder_forced_from_T9_v2, which states the full step functions from electron to muon and muon to tau together with relative errors below 0.2 percent. It advances the T10 necessity program by replacing an axiom with a proven inequality derived from T9 electron mass and the phi-ladder. The result connects to framework landmarks including the eight-tick octave and D equals 3 through the geometric constants used in the residue calculation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.