chi2

formal source

  14def z (e : SpeciesEntry) : ℝ :=
  15  (e.mass_pred - e.mass_obs) / e.sigma
  16
  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