d_entry

formal source

  58
  59/-! Quark witnesses (approximate PDG central values, GeV). -/
  60@[simp] def u_entry : SpeciesEntry := { name := "u", mass_obs := 0.0022, sigma := 0.0005, mass_pred := 0.0022 }
  61@[simp] def d_entry : SpeciesEntry := { name := "d", mass_obs := 0.0047, sigma := 0.0010, mass_pred := 0.0047 }
  62@[simp] def s_entry : SpeciesEntry := { name := "s", mass_obs := 0.096,  sigma := 0.0050, mass_pred := 0.096 }
  63@[simp] def c_entry : SpeciesEntry := { name := "c", mass_obs := 1.27,   sigma := 0.03,   mass_pred := 1.27 }
  64@[simp] def b_entry : SpeciesEntry := { name := "b", mass_obs := 4.18,   sigma := 0.03,   mass_pred := 4.18 }
  65@[simp] def t_entry : SpeciesEntry := { name := "t", mass_obs := 172.76, sigma := 0.30,   mass_pred := 172.76 }
  66
  67@[simp] def quarksWitness : List SpeciesEntry := [u_entry, d_entry, s_entry, c_entry, b_entry, t_entry]
  68
  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