z_H_zero
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.