acceptable_bosons

formal source

 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 :=
 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]