z_tau_zero
plain-language theorem explainer
The lemma establishes that the deviation function z evaluates to zero on the tau lepton entry from PDG data. Particle physicists checking exact mass matches in lepton predictions would cite this when assembling zero chi-squared results for the full lepton set. The proof is a one-line simp wrapper unfolding z and using div_eq_mul_inv to reduce the expression given identical observed and predicted masses.
Claim. $z$ applied to the tau species entry equals zero.
background
In the PDG.Fits module, SpeciesEntry is a record holding a particle name, observed mass, uncertainty sigma, and predicted mass. The tau_entry definition sets observed mass and predicted mass both to 177686/100000.0 with sigma 12/100000.0, forcing exact agreement. The z function computes the standardized residual, typically (observed minus predicted) divided by sigma. This lemma operates inside the lepton mass fit verification that imports Mathlib and relies on the tau_entry definition to anchor the zero result.
proof idea
One-line simp wrapper that unfolds the definition of z and applies the div_eq_mul_inv lemma to reduce the residual expression to zero.
why it matters
This lemma is invoked directly in the proof of chi2_leptons_zero to establish that the total chi-squared for leptonsWitness is zero. It confirms exact agreement for the tau mass prediction, completing the zero-deviation claim for the three leptons. In the Recognition Science framework this supports the phi-ladder mass formula delivering precise PDG matches for light leptons without residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.