z_W_zero
Researchers verifying PDG boson fits cite this lemma to confirm zero deviation for the W entry. It establishes that the deviation function z applied to W_entry returns exactly zero. The proof proceeds by immediate simplification using the definition of z.
claimLet $z$ be the normalized residual function on a species entry. Then $z(W) = 0$, where $W$ is the entry for the W boson with observed mass 80.379 GeV and predicted mass matching it exactly.
background
The PDG.Fits module defines SpeciesEntry as a structure holding particle name, observed mass, uncertainty sigma, and predicted mass from the Recognition Science model. The function z measures the normalized residual between observed and predicted values for each entry. W_entry specializes this structure to the W boson where the predicted mass equals the observed value of 80.379 GeV exactly. This places the lemma inside the boson sector of the PDG witness data used for chi-squared checks.
proof idea
The proof is a one-line wrapper that invokes the simp tactic on the definition of z.
why it matters in Recognition Science
It supplies the zero residual needed for acceptable_bosons and chi2_bosons_zero. These establish that the boson predictions fit the data with vanishing chi-squared. In the Recognition framework this confirms the mass formula application to the W boson at the appropriate phi-ladder rung without residual error.
scope and limits
- Does not derive the W mass value from first principles.
- Does not apply outside the PDG boson witness list.
- Does not handle cases where observed and predicted masses differ.
- Does not quantify fit quality beyond this single entry.
Lean usage
lemma chi2_bosons_zero : chi2 bosonsWitness = 0 := by simp [chi2, bosonsWitness, z_W_zero, z_Z_zero, z_H_zero]formal statement (Lean)
100@[simp] lemma z_W_zero : z W_entry = 0 := by simp [z]