z_H_zero
The lemma shows that the z deviation vanishes exactly on the Higgs entry. Analysts fitting PDG boson masses to Recognition Science predictions would cite it when confirming zero residual for the Higgs in chi-squared sums. The proof is a one-line simplification that unfolds z on the supplied entry data.
claim$z(H) = 0$, where $H$ is the Higgs species entry with observed mass 125.25 and predicted mass 125.25.
background
In the PDG.Fits module, SpeciesEntry is a structure holding particle name, observed mass, sigma uncertainty, and model-predicted mass. The z function computes the normalized residual between observed and predicted masses. H_entry is the concrete definition for the Higgs boson in which the two masses are set equal, forcing the residual to zero. This lemma is the direct dependency of chi2_bosons_zero, which aggregates z contributions over the boson witness.
proof idea
One-line wrapper that applies the simp tactic to the definition of z, which immediately reduces the claim to zero because mass_obs equals mass_pred inside H_entry.
why it matters in Recognition Science
The lemma is used by chi2_bosons_zero to establish that the total chi-squared for the boson sector is exactly zero. This confirms that the Recognition Science mass formula reproduces the PDG values for W, Z, and H without discrepancy, consistent with the phi-ladder construction and T6 self-similar fixed point. No open questions are addressed.
scope and limits
- Does not prove the mass prediction formula.
- Does not apply to leptons or fermions.
- Does not propagate uncertainties across multiple entries.
- Does not address systematic errors in the input data.
formal statement (Lean)
102@[simp] lemma z_H_zero : z H_entry = 0 := by simp [z]
proof body
103