z_e_zero
plain-language theorem explainer
Standardized residual for the electron entry vanishes exactly. PDG lepton fits invoke this to confirm the electron adds nothing to total chi-squared. Proof reduces directly via one-line simplification on the residual definition after unfolding z.
Claim. Let $z$ denote the standardized residual on a species entry. For the electron entry $e$ with identical observed and predicted masses, $z(e)=0$.
background
In the PDG.Fits module species entries record an observed mass, its uncertainty sigma, and a predicted mass. The electron entry is constructed with observed and predicted masses set equal to the same rational value. The function z computes the difference between predicted and observed masses divided by sigma. This supplies the base case for zero-deviation checks on leptons. The upstream definition of the electron entry fixes the numerical values that make the residual vanish.
proof idea
One-line wrapper that applies simp to the definition of z together with the division-as-multiplication identity, which cancels the identical masses to zero.
why it matters
Feeds the proofs that lepton chi-squared totals zero and that the lepton witness set is acceptable at zero deviation. Supports the Recognition Science claim that phi-ladder mass predictions match PDG data for the electron, consistent with T5 J-uniqueness and the mass formula yardstick.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.