tau_mass_pred_bounds_tight
plain-language theorem explainer
The theorem establishes that the Recognition Science prediction for the tau lepton mass lies strictly between 1768.4 and 1791.6. Researchers deriving the three lepton generations from the electron mass plus cube geometry and wallpaper-group counts would cite this result. The proof is a direct term pairing of the lower-bound and upper-bound lemmas already established for the same quantity.
Claim. The predicted tau mass satisfies $1768.4 < m_τ^pred < 1791.6$.
background
In the Recognition Science setting the lepton ladder is constructed from the electron structural mass (T9), the passive-edge count E_passive = 11, the wallpaper-group count W = 17, the cube-face count F = 6, the fine-structure constant α, and the golden ratio φ. The Anchor.tau definition supplies the generation torsion: τ(0) = 0, τ(1) = 11, τ(2) = 17. The module replaces two earlier axioms with proven inequalities that close the necessity argument for T10.
proof idea
The proof is a one-line term wrapper that applies the lemmas predicted_mass_tau_lower_tight and predicted_mass_tau_upper_tight to obtain the required conjunction.
why it matters
This result supplies the concrete numerical bounds required by the main T10 theorem that the muon and tau masses are forced from T9 together with the geometric constants E_passive, W, α and φ. It therefore completes the necessity half of the lepton-ladder derivation inside the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.