chi2_bosons_zero
plain-language theorem explainer
The chi-squared statistic over the boson witness list evaluates to zero. PDG fits cite this to confirm zero defect for the W, Z, and Higgs entries. The proof is a one-line simp wrapper that unfolds chi2 and the witness list then applies the three individual z-zero lemmas.
Claim. $chi^2([W_{entry}, Z_{entry}, H_{entry}]) = 0$, where $chi^2(L) := sum_{e in L} z(e)^2$.
background
In the PDG.Fits module chi2 is the fold that accumulates the square of the z function over a list of species entries. bosonsWitness is the concrete list containing the W, Z, and Higgs entries. Three upstream lemmas establish that z vanishes on each of those entries by direct simplification of the z definition.
proof idea
The proof is a one-line simp wrapper. It unfolds the definitions of chi2 and bosonsWitness, then applies the simp lemmas z_W_zero, z_Z_zero, and z_H_zero to reduce every term to zero.
why it matters
This lemma is invoked by acceptable_bosons to discharge the chi2 component of the boson acceptance test. It closes the zero-defect verification for the gauge bosons and Higgs within the PDG data set. In the Recognition framework it supplies the boson half of the particle-spectrum consistency check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.