z_s_zero
plain-language theorem explainer
The lemma establishes that the deviation function z returns zero on the strange quark entry. Analysts confirming exact PDG mass matches for quarks against Recognition Science predictions would cite this when assembling zero chi-squared results. The proof reduces immediately by simplification using the definition of z.
Claim. Let $z$ be the deviation function on species entries. Then $z(s)=0$, where $s$ is the strange quark entry with observed mass 0.096, uncertainty 0.0050, and predicted mass 0.096.
background
The PDG.Fits module defines SpeciesEntry as a record with fields for name, observed mass, measurement sigma, and predicted mass. The function z computes the discrepancy between observed and predicted masses for any entry. The s_entry is the concrete record for the strange quark with identical observed and predicted masses of 0.096. This lemma sits inside the collection of zero-deviation statements for the six quarks.
proof idea
The proof is a one-line wrapper that invokes the simp tactic with the definition of z. Equality of observed and predicted masses in s_entry forces the deviation to zero with no further steps required.
why it matters
This lemma is used inside chi2_quarks_zero to obtain chi2 quarksWitness = 0 and inside acceptable_quarks to verify the acceptance predicate for all quark entries. It supplies one exact match in the verification that Recognition Science mass predictions on the phi-ladder reproduce PDG data for the strange quark. The result closes one case in the quark-sector fit before the full chi-squared claim is assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.