z_t_zero
plain-language theorem explainer
The top quark species entry has vanishing deviation under the standardized residual function because its predicted mass is set equal to the observed value. Researchers checking exact reproduction of PDG quark masses in the Recognition Science ladder would cite this when confirming the full quark chi-squared vanishes. The proof is a direct one-line simplification using the residual definition.
Claim. Let $t$ be the top quark species entry with observed mass 172.76 GeV, uncertainty 0.30 GeV, and predicted mass 172.76 GeV. Then the standardized residual satisfies $z(t) = 0$.
background
The PDG fits module records each particle as a species entry containing its observed mass, experimental uncertainty sigma, and a model-predicted mass. The residual function z returns the standardized difference (observed minus predicted) divided by sigma for any such entry. The top entry is constructed with identical observed and predicted masses, forcing the residual to zero by definition. This lemma belongs to the set of zero-residual statements for the six quarks that together imply the sector chi-squared is exactly zero.
proof idea
The proof is a one-line wrapper that applies the simplification rule for the residual function on the top entry definition.
why it matters
This lemma is invoked inside the proof that the chi-squared for the quark witness set equals zero and inside the acceptability check for all quarks at zero tolerance. It therefore closes the verification that the Recognition Science mass predictions match PDG values exactly for the quark sector. The result sits downstream of the top entry construction and supports the broader claim that the phi-ladder reproduces observed masses without residual for the third-generation quarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.