z_u_zero
plain-language theorem explainer
The lemma establishes that the deviation function z evaluates to zero on the up-quark PDG entry. It is cited in chi-squared calculations for the full quark set and in acceptability checks for the quark witness. The proof is a direct one-line simplification that unfolds z on the u-entry record.
Claim. The standardized deviation for the up-quark species entry is zero: $z$ (up-quark entry) $= 0$.
background
In the PDG fits module, a SpeciesEntry is a record holding a name, observed mass, uncertainty sigma, and predicted mass. The up-quark entry sets observed and predicted masses equal at 0.0022 with sigma 0.0005. The z function computes the normalized residual between observed and predicted mass. This lemma is the direct prerequisite for showing the chi-squared statistic over the quark witness set equals zero.
proof idea
This is a one-line simp wrapper. The tactic unfolds the definition of z on the up-quark entry record; because observed and predicted masses match exactly, the residual is zero.
why it matters
It feeds the zero chi-squared result for quarks and the acceptability lemma for the quark witness set. The result verifies exact agreement between predicted and observed mass for the up quark, supporting the PDG fit verification step in the Recognition Science mass ladder. It closes one residual check in the quark sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.