z_n_zero
plain-language theorem explainer
The lemma shows that the normalized deviation z vanishes for the neutron species entry because its observed and predicted masses coincide. PDG baryon fitters in the Recognition Science setting cite it to confirm that the neutron adds nothing to the total chi-squared. The proof is a direct one-line simplification that invokes the definition of z together with the simp attribute on n_entry.
Claim. Let $z$ be the normalized mass-deviation function on species entries. Then $z(n) = 0$, where $n$ denotes the neutron entry whose observed mass equals its predicted mass.
background
The PDG.Fits module records particle data via SpeciesEntry structures that pair an observed mass, an uncertainty sigma, and a predicted mass drawn from the Recognition Science phi-ladder formula. The sibling function z computes the standardized residual (observed minus predicted) scaled by sigma, returning zero precisely when the two masses agree. This lemma depends on the upstream definition of n_entry, which hard-codes both mass_obs and mass_pred to the same numerical value 0.9395654133.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of z, using the simp attribute already attached to n_entry to collapse the equality at once.
why it matters
The result supplies the neutron term inside chi2_baryons_zero and is invoked during the case split of acceptable_baryons. It therefore closes the zero-residual verification for all listed baryons, aligning the PDG data with the mass formula on the phi-ladder (T5 J-uniqueness and T6 self-similar fixed point). It touches the open question of how tightly the Recognition Science predictions reproduce the full PDG baryon spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.