tau_mass_pred_bounds
plain-language theorem explainer
The theorem proves that the RS-predicted tau mass lies in the open interval (1768, 1792) MeV. Researchers deriving lepton masses from the phi-ladder and topological steps would reference this bound to validate the Face Symmetry Step. The proof reduces directly to the interval theorem established in the Necessity submodule via a single term application.
Claim. Let $m_τ^pred$ be the value obtained by scaling the structural electron mass by $ϕ$ to the power of the tau residue. Then $1768 < m_τ^pred < 1792$ (in MeV units).
background
The Lepton Generations module extends the topological ladder from the electron (T9) to higher generations via the mass formula $m_n = m_struct ⋅ ϕ^{Δ_n}$, where each step $S_{n→n+1}$ adds a topological increment to the residue Δ. The predicted tau mass is defined as electron_structural_mass multiplied by phi raised to predicted_residue_tau. The empirical anchor is the constant mass_tau_MeV equal to 1776.86 MeV. Upstream results supply the structural mass from PrimitiveDistinction and phase-lift bounds from CirclePhaseLift that propagate into the residue interval.
proof idea
The proof is a one-line term wrapper that directly invokes the theorem tau_mass_pred_bounds_proven from the Necessity submodule, which constructs the lower and upper estimates via interval propagation on the phi-powered term.
why it matters
This declaration supplies the proven interval that feeds the downstream tau_mass_step_hypothesis, confirming the Face Symmetry Step matches the observed mass to within 1 percent. It completes the T10 lepton-generation chain that begins with the electron structural mass and applies the phi-ladder increments derived from the forcing chain (T5–T8). The result replaces an earlier axiom with a derived bound, tightening the link between the Recognition Composition Law and observable lepton masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.