tau_mass_step_hypothesis
plain-language theorem explainer
The result shows that the phi-ladder prediction for the tau mass lies inside a 1 percent relative window of the measured value 1776.86 MeV. Researchers deriving lepton masses from topological steps cite it to close the muon-to-tau transition under the Face Symmetry hypothesis. The argument invokes the already-proven interval bounds on the prediction and reduces the relative-error inequality by direct comparison and norm_num arithmetic.
Claim. Let $m_τ^{pred}$ be the tau mass obtained from the structural base mass times $φ$ raised to the predicted residue, and let $m_τ = 1776.86$ MeV. Then $|m_τ^{pred} - m_τ| / m_τ < 1/100$.
background
The module formalizes lepton masses on the phi-ladder: the mass in generation $n$ satisfies $m_n = m_{struct} · φ^{Δ_n}$, where the increments $Δ_{n+1} = Δ_n + S_{n→n+1}$ are fixed by topological steps. For the muon-to-tau step the Face Symmetry hypothesis supplies $S_{μ→τ} = F - (2W+3)α/2$ with $F=6$ and $W=17$, yielding a residue that produces the predicted mass. The upstream theorem tau_mass_pred_bounds supplies the interval (1768, 1792) for that prediction; mass_tau_MeV is the CODATA constant 1776.86.
proof idea
The tactic proof first imports the interval bounds from tau_mass_pred_bounds. It rewrites the absolute difference to obtain |pred - 1776.86| < 16, then divides by the positive experimental mass and compares the resulting quotient against 16/1776.86. A final norm_num step shows that 16/1776.86 is strictly less than 1/100, completing the chain.
why it matters
This theorem supplies the concrete numerical check for the T10 Face Symmetry Step inside the lepton-generation ladder. It sits downstream of the structural-mass and residue definitions and is referenced by the sibling muon-mass results to maintain uniform accuracy claims across generations. Within the Recognition framework it supplies the empirical anchor for the eight-tick octave and phi-ladder mass formula at the third lepton rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.