acceptable_quarks

formal source

  76@[simp] lemma chi2_quarks_zero : chi2 quarksWitness = 0 := by
  77  simp [chi2, quarksWitness, z_u_zero, z_d_zero, z_s_zero, z_c_zero, z_b_zero, z_t_zero]
  78
  79@[simp] lemma acceptable_quarks : acceptable quarksWitness 0 0 := by
  80  refine And.intro ?hzs ?hchi
  81  · intro e he
  82    have hcases : e = u_entry ∨ e = d_entry ∨ e = s_entry ∨ e = c_entry ∨ e = b_entry ∨ e = t_entry := by
  83      simpa [quarksWitness] using he
  84    rcases hcases with h | h | h | h | h | h
  85    · subst h; simp [z_u_zero]
  86    · subst h; simp [z_d_zero]
  87    · subst h; simp [z_s_zero]
  88    · subst h; simp [z_c_zero]
  89    · subst h; simp [z_b_zero]
  90    · subst h; simp [z_t_zero]
  91  · simpa using chi2_quarks_zero
  92
  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