tau_entry
plain-language theorem explainer
tau_entry supplies the SpeciesEntry record for the tau lepton using observed mass 1.77686, uncertainty 0.00012, and matching predicted mass. Researchers assembling lepton data for deviation checks in PDG fits cite it when forming the leptonsWitness list. The definition is a direct record construction matching the SpeciesEntry structure with these numerical values.
Claim. The tau lepton entry is the SpeciesEntry record with name ``tau'', observed mass $1.77686$, uncertainty $0.00012$, and predicted mass $1.77686$.
background
SpeciesEntry is the structure with fields name : String, mass_obs : ℝ, sigma : ℝ, mass_pred : ℝ. In the PDG.Fits module these records hold empirical lepton data for comparison against Recognition Science predictions. Upstream, the tau function from Masses.Anchor supplies generation torsion (τ(2) = 17 for the third generation) while the sigma abbrev from ArithmeticFunctions is the sum-of-divisors function; this entry instead hard-codes PDG numerical values.
proof idea
Direct definition that constructs the SpeciesEntry record literal with the string name and the three real-number field values.
why it matters
tau_entry populates leptonsWitness and enables the z_tau_zero lemma that shows zero deviation. It supplies the empirical tau mass for the third lepton generation, connecting to the mass formula yardstick * phi^(rung - 8 + gap(Z)) and the T7 eight-tick octave. This supports checks against the alpha inverse band and Berry creation threshold in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.