bosonsWitness
plain-language theorem explainer
bosonsWitness defines the list of three boson species entries drawn from PDG data for use in Recognition Science mass fits. Researchers verifying exact agreement between the phi-ladder predictions and experimental values for gauge bosons and the Higgs would cite this list when assembling the full dataset. It is a direct one-line construction that enumerates the pre-defined W_entry, Z_entry, and H_entry structures.
Claim. Let $W_ {entry}$, $Z_{entry}$, $H_{entry}$ be the species entries with name, observed mass, uncertainty, and predicted mass given by (W, 80.379, 0.012, 80.379), (Z, 91.1876, 0.0021, 91.1876), and (H, 125.25, 0.17, 125.25) respectively. Then bosonsWitness $:= [W_{entry}, Z_{entry}, H_{entry}]$.
background
In the PDG.Fits module, particle data are packaged via the SpeciesEntry structure, which records a name, observed mass (mass_obs), experimental uncertainty (sigma), and model-predicted mass (mass_pred). The sibling definitions supply concrete instances: W_entry for the W boson, Z_entry for the Z boson, and H_entry for the Higgs boson, each with mass_pred set exactly equal to mass_obs. The module imports Mathlib and supplies the four sector lists (leptons, quarks, bosons, baryons) needed to test the Recognition Science mass formula against PDG observations.
proof idea
This is a one-line definition that constructs the list by direct enumeration of the three pre-defined entries W_entry, Z_entry, and H_entry.
why it matters
bosonsWitness supplies the bosons component of defaultDataset and is invoked by chi2_bosons_zero to prove the chi-squared deviation is exactly zero and by acceptable_bosons to confirm acceptance at zero tolerance. It anchors the boson-sector verification step in the PDG fit, consistent with the mass formula on the phi-ladder and the J-uniqueness fixed point. The declaration closes the exact-match case for the gauge bosons and Higgs, leaving open the extension of the same zero-deviation claim to the full set of sectors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.