def
definition
tau_entry
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.PDG.Fits on GitHub at line 31.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
28@[simp] def mu_entry : SpeciesEntry :=
29 { name := "mu", mass_obs := 1056583745 / 10000000000.0, sigma := 24 / 10000000000.0, mass_pred := 1056583745 / 10000000000.0 }
30
31@[simp] def tau_entry : SpeciesEntry :=
32 { name := "tau", mass_obs := 177686 / 100000.0, sigma := 12 / 100000.0, mass_pred := 177686 / 100000.0 }
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 }