acceptable_leptons

formal source

  45@[simp] lemma chi2_leptons_zero : chi2 leptonsWitness = 0 := by
  46  simp [chi2, leptonsWitness, z_e_zero, z_mu_zero, z_tau_zero]
  47
  48@[simp] lemma acceptable_leptons : acceptable leptonsWitness 0 0 := by
  49  refine And.intro ?hzs ?hchi
  50  · intro e he
  51    rcases he with he | he | he
  52    · simp [z_e_zero]
  53    · cases he with
  54      | inl h => simp [h, z_mu_zero]
  55      | inr h => cases h
  56    · cases he
  57  · simpa using chi2_leptons_zero
  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