def
definition
e_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 25.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
22
23/-! Pinned PDG 2024 leptons witness (central values; uncertainties approximate, positive).
24 We set mass_pred = mass_obs to produce a clean, fast, auditable witness. -/
25@[simp] def e_entry : SpeciesEntry :=
26 { name := "e", mass_obs := (51099895 : ℚ) / 100000000000, sigma := (1 : ℚ) / 1000000000, mass_pred := (51099895 : ℚ) / 100000000000 }
27
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