tau_mass_step_hypothesis
plain-language theorem explainer
The theorem establishes that the tau mass predicted from the phi-ladder residue after the Face Symmetry Step lies within 1% of the measured value 1776.86 MeV. Physicists deriving lepton masses via topological steps would cite this to close the T10 generation sequence. The proof obtains the interval (1768, 1792) from the upstream bounds theorem, bounds the absolute deviation by 16, and verifies the relative error by division and numerical comparison.
Claim. Let $p$ be the tau mass predicted as structural mass scaled by the residue exponent on the phi ladder. Then $|p - 1776.86| / 1776.86 < 0.01$.
background
The module derives muon and tau masses by extending the electron structural mass (T9) along the phi ladder with two topological steps. The Face Symmetry Step for muon to tau is $S = 6 - (2W + 3)alpha/2$ with $W = 17$, yielding residue approximately 5.8657. mass_tau_MeV is the CODATA value 1776.86 MeV. predicted_mass_tau is defined as electron_structural_mass times phi to the power of the predicted residue for tau.
proof idea
The proof calls tau_mass_pred_bounds to obtain the interval (1768, 1792). It rewrites the absolute deviation bound via abs_lt and applies linarith to show the deviation is less than 16. Division by the positive mass value 1776.86 produces a strict inequality, which norm_num then compares to 1/100.
why it matters
This result completes T10 in the lepton generation sequence, confirming the Face Symmetry Step after the electron structural mass from T9. It supplies the parent bound used by the RRF mirror declaration and supports the phi-ladder mass formula together with the eight-tick octave. The accuracy note records that the bound was relaxed to 1% after interval correction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.