z_c_zero

formal source

  69@[simp] lemma z_u_zero : z u_entry = 0 := by simp [z]
  70@[simp] lemma z_d_zero : z d_entry = 0 := by simp [z]
  71@[simp] lemma z_s_zero : z s_entry = 0 := by simp [z]
  72@[simp] lemma z_c_zero : z c_entry = 0 := by simp [z]
  73@[simp] lemma z_b_zero : z b_entry = 0 := by simp [z]
  74@[simp] lemma z_t_zero : z t_entry = 0 := by simp [z]
  75
  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]