def
definition
acceptable
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 20.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
17def chi2 (L : List SpeciesEntry) : ℝ :=
18 L.foldl (fun acc e => acc + (z e) * (z e)) 0
19
20def acceptable (L : List SpeciesEntry) (zMax χ2Max : ℝ) : Prop :=
21 (∀ e ∈ L, |z e| ≤ zMax) ∧ chi2 L ≤ χ2Max
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