def
definition
p_entry
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.PDG.Fits on GitHub at line 119.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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 :=
127 [p_entry, n_entry, Delta_pp_entry, Delta_p_entry, Delta_0_entry, Delta_m_entry]
128
129@[simp] lemma z_p_zero : z p_entry = 0 := by simp [z]
130@[simp] lemma z_n_zero : z n_entry = 0 := by simp [z]
131@[simp] lemma z_Dpp_zero : z Delta_pp_entry = 0 := by simp [z]
132@[simp] lemma z_Dp_zero : z Delta_p_entry = 0 := by simp [z]
133@[simp] lemma z_D0_zero : z Delta_0_entry = 0 := by simp [z]
134@[simp] lemma z_Dm_zero : z Delta_m_entry = 0 := by simp [z]
135
136@[simp] lemma chi2_baryons_zero : chi2 baryonsWitness = 0 := by
137 simp [chi2, baryonsWitness, z_p_zero, z_n_zero, z_Dpp_zero, z_Dp_zero, z_D0_zero, z_Dm_zero]
138
139@[simp] lemma acceptable_baryons : acceptable baryonsWitness 0 0 := by
140 refine And.intro ?hzs ?hchi
141 · intro e he
142 have hcases : e = p_entry ∨ e = n_entry ∨ e = Delta_pp_entry ∨ e = Delta_p_entry ∨ e = Delta_0_entry ∨ e = Delta_m_entry := by
143 simpa [baryonsWitness] using he
144 rcases hcases with h | h | h | h | h | h
145 · subst h; simp [z_p_zero]
146 · subst h; simp [z_n_zero]
147 · subst h; simp [z_Dpp_zero]
148 · subst h; simp [z_Dp_zero]
149 · subst h; simp [z_D0_zero]