z_p_zero
plain-language theorem explainer
The lemma establishes that the proton species entry yields zero deviation under the z function. PDG mass-fit verifiers in the Recognition Science setting would cite this when confirming exact matches for the baryon sector. The proof is a direct simplification that unfolds the definition of z on p_entry.
Claim. Let $p$ be the proton entry with observed mass $0.9382720813$ and predicted mass $0.9382720813$. Then $z(p)=0$.
background
In PDG.Fits, SpeciesEntry packages a particle name, observed mass, uncertainty sigma, and predicted mass. The function z extracts the deviation between observed and predicted masses for any such entry. p_entry is the concrete definition that sets both masses equal for the proton, providing the base case for baryon checks.
proof idea
The proof is a one-line wrapper that applies simp to the definition of z.
why it matters
z_p_zero is invoked inside chi2_baryons_zero to obtain zero chi-squared for baryonsWitness and inside acceptable_baryons to discharge the zero-deviation case for the proton. It supplies the proton base case for PDG fits that test the phi-ladder mass formula against data, consistent with the T6 fixed-point and mass-rung construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.