`Delta_p_entry`

definition

show as: view math explainer →

module: IndisputableMonolith.PDG.Fits
domain: PDG
line: 122 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.PDG.Fits on GitHub at line 122.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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]
 150    · subst h; simp [z_Dm_zero]
 151  · simpa using chi2_baryons_zero
 152

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.