W_entry
plain-language theorem explainer
W_entry supplies the PDG record for the W boson with observed mass 80.379 GeV, uncertainty 0.012 GeV, and predicted mass set equal to the observed value. Particle physicists assembling boson lists for mass fits in the Recognition Science PDG module cite this entry when constructing bosonsWitness for deviation checks. The definition proceeds by direct record construction of the SpeciesEntry structure with no further computation.
Claim. Let SpeciesEntry denote the structure with fields name : String, mass_obs : ℝ, sigma : ℝ, mass_pred : ℝ. The W boson entry is the instance with name = ``W'', mass_obs = 80.379, sigma = 0.012, mass_pred = 80.379.
background
The PDG.Fits module introduces SpeciesEntry as a record structure that holds a particle species name as a string, its observed mass as a real number, the experimental uncertainty as a real sigma, and a predicted mass as a real for later comparison. This W_entry populates the record specifically for the W boson using PDG numerical values where prediction matches observation. Upstream results include the SpeciesEntry structure definition itself along with unrelated W abbreviations in mass topology and lepton modules that denote wallpaper groups or spatial dimension counts; the sigma field here is the uncertainty, distinct from sigma-charge or sum-of-divisors functions in other modules.
proof idea
The declaration is a direct definition that constructs the SpeciesEntry record literal with the four hardcoded fields for the W boson. No lemmas or tactics are applied; it is a one-line record instantiation.
why it matters
W_entry feeds bosonsWitness, which assembles the list of W, Z, and H entries, and the lemma z_W_zero, which shows the deviation function z returns zero on this entry. It supports PDG mass fits inside the Recognition framework by supplying a data point where observed and predicted W masses coincide, consistent with the phi-ladder mass formula when the gap term vanishes. This closes a concrete data interface for boson comparisons without invoking the full forcing chain or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.