mass_tau_MeV
plain-language theorem explainer
The definition supplies the CODATA 2022 experimental value for the tau lepton mass in MeV units. Researchers verifying the T10 lepton ladder cite it to confirm that the predicted mass from geometric steps lies within 1% of observation. The implementation is a direct numerical assignment with no derivation or lemmas.
Claim. Let $m_τ$ denote the tau lepton mass in MeV. Then $m_τ = 1776.86$.
background
The module isolates numerical anchors for the T10 lepton generations to avoid import cycles with the Necessity theorems. These constants pair with step functions (electron-to-muon via passive edges and spherical geometry, muon-to-tau via cube faces and wallpaper groups) to support relative-error bounds. The upstream CirclePhaseLift.and result supplies explicit log-derivative bounds that tighten the structural mass calculations feeding into the lepton ladder.
proof idea
This is a direct definition that assigns the real constant 1776.86. No tactics or upstream lemmas are invoked; the value is fixed by the CODATA reference.
why it matters
The definition anchors the verification theorems tau_mass_pred_bounds and tau_mass_step_hypothesis, which close the T10 loop by showing the predicted tau mass satisfies the 1% relative-error bound. It is referenced by the main result lepton_ladder_forced_from_T9 that derives both muon and tau masses from the T9 electron mass together with the passive-edge count 11, face count 6, wallpaper count 17, and the fine-structure constant. This supplies the experimental calibration point for the Recognition Science lepton ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.