z_Dpp_zero
The lemma shows that the deviation measure z applied to the Delta++ entry is exactly zero. It is invoked when confirming that the baryon sector matches Recognition Science mass predictions with zero residual. The proof reduces immediately by simplification using the definition of z.
claim$z$ applied to the Delta++ species entry equals zero: $z(Delta_{pp}) = 0$.
background
SpeciesEntry is a record holding particle name, observed mass, uncertainty sigma, and predicted mass. The function z computes the normalized residual between observed and predicted masses for each entry. Delta_pp_entry is the concrete record for the Delta++ resonance with both masses fixed at 1.232 and sigma at 0.005. This lemma sits inside the PDG.Fits module, which assembles baryon and lepton entries to test the Recognition Science phi-ladder against PDG data.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of z, which evaluates directly to zero because observed and predicted masses coincide in Delta_pp_entry.
why it matters in Recognition Science
It is used inside chi2_baryons_zero to establish that the total chi-squared for the baryon witness is zero and inside acceptable_baryons to confirm the fit passes acceptance. The result supports exact reproduction of PDG Delta masses by the Recognition Science mass formula on the phi-ladder. It contributes to the PDG verification step that checks zero residuals for the baryon sector.
scope and limits
- Does not derive the mass prediction from the underlying phi-ladder axioms.
- Applies only to the specific numerical values stored in Delta_pp_entry.
- Does not address leptons or other particle sectors.
- Does not incorporate experimental uncertainties beyond the given sigma.
Lean usage
simp [z_Dpp_zero]formal statement (Lean)
131@[simp] lemma z_Dpp_zero : z Delta_pp_entry = 0 := by simp [z]