z_e_zero

formal source

  33
  34@[simp] def leptonsWitness : List SpeciesEntry := [e_entry, mu_entry, tau_entry]
  35
  36@[simp] lemma z_e_zero : z e_entry = 0 := by
  37  simp [z, div_eq_mul_inv]
  38
  39@[simp] lemma z_mu_zero : z mu_entry = 0 := by
  40  simp [z, div_eq_mul_inv]
  41
  42@[simp] lemma z_tau_zero : z tau_entry = 0 := by
  43  simp [z, div_eq_mul_inv]
  44
  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