def
definition
H_entry
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.PDG.Fits on GitHub at line 96.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
93/-! Boson witnesses (approximate PDG central values, GeV). -/
94@[simp] def W_entry : SpeciesEntry := { name := "W", mass_obs := 80.379, sigma := 0.012, mass_pred := 80.379 }
95@[simp] def Z_entry : SpeciesEntry := { name := "Z", mass_obs := 91.1876, sigma := 0.0021, mass_pred := 91.1876 }
96@[simp] def H_entry : SpeciesEntry := { name := "H", mass_obs := 125.25, sigma := 0.17, mass_pred := 125.25 }
97
98@[simp] def bosonsWitness : List SpeciesEntry := [W_entry, Z_entry, H_entry]
99
100@[simp] lemma z_W_zero : z W_entry = 0 := by simp [z]
101@[simp] lemma z_Z_zero : z Z_entry = 0 := by simp [z]
102@[simp] lemma z_H_zero : z H_entry = 0 := by simp [z]
103
104@[simp] lemma chi2_bosons_zero : chi2 bosonsWitness = 0 := by
105 simp [chi2, bosonsWitness, z_W_zero, z_Z_zero, z_H_zero]
106
107@[simp] lemma acceptable_bosons : acceptable bosonsWitness 0 0 := by
108 refine And.intro ?hzs ?hchi
109 · intro e he
110 rcases he with he | he | he
111 · simp [z_W_zero]
112 · cases he with
113 | inl h => simp [h, z_Z_zero]
114 | inr h => cases h
115 · cases he
116 · simpa using chi2_bosons_zero
117
118/‑! Baryon witnesses (approximate PDG central values, GeV). -/
119@[simp] def p_entry : SpeciesEntry := { name := "p", mass_obs := 0.9382720813, sigma := 1e-6, mass_pred := 0.9382720813 }
120@[simp] def n_entry : SpeciesEntry := { name := "n", mass_obs := 0.9395654133, sigma := 1e-6, mass_pred := 0.9395654133 }
121@[simp] def Delta_pp_entry : SpeciesEntry := { name := "Delta_pp", mass_obs := 1.232, sigma := 0.005, mass_pred := 1.232 }
122@[simp] def Delta_p_entry : SpeciesEntry := { name := "Delta_p", mass_obs := 1.232, sigma := 0.005, mass_pred := 1.232 }
123@[simp] def Delta_0_entry : SpeciesEntry := { name := "Delta_0", mass_obs := 1.232, sigma := 0.005, mass_pred := 1.232 }
124@[simp] def Delta_m_entry : SpeciesEntry := { name := "Delta_m", mass_obs := 1.232, sigma := 0.005, mass_pred := 1.232 }
125
126@[simp] def baryonsWitness : List SpeciesEntry :=