def
definition
tau_entry
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
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 }