mass_tau_MeV
plain-language theorem explainer
mass_tau_MeV supplies the CODATA 2022 experimental value of the tau lepton rest mass as a real constant in MeV. Researchers verifying the T10 lepton ladder cite it when checking that the face-symmetry step reproduces observation within one percent relative error. The definition is a direct numeric literal that anchors downstream interval bounds without further computation.
Claim. The tau lepton rest mass is the constant $m_τ = 1776.86$ MeV.
background
The module supplies the core numeric constants for T10 lepton generations, kept separate from theorems to break import cycles. mass_tau_MeV enters comparisons between the structural prediction (built from electron mass, passive edges E_p = 11, cube faces F = 6, wallpaper groups W = 17, and α) and measured data. The upstream CirclePhaseLift.and theorem supplies an explicit log-derivative bound M that converts to an angular Lipschitz constant on the circle, enabling the phase-lift arguments used in related mass derivations.
proof idea
The declaration is a bare literal assignment of the real number 1776.86. No lemmas or tactics are invoked; it functions as the experimental reference value for the interval-propagation theorems that follow.
why it matters
The constant closes the T10 loop by supplying the observed target for tau_mass_pred_bounds and tau_mass_step_hypothesis, which together confirm that the predicted mass lies inside (1768, 1792) with relative error below 1 percent. It is invoked directly in the main results lepton_ladder_forced_from_T9 and lepton_ladder_forced_from_T9_v2, which derive the entire muon and tau masses from T9 structural mass plus the geometric steps (passive edges, faces, wallpaper groups) and α. This supplies the final observational match required by the Recognition Science forcing chain at the T10 stage.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.