IndisputableMonolith.PDG.Fits

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace PDG
   5namespace Fits
   6
   7structure SpeciesEntry where
   8  name : String
   9  mass_obs : ℝ
  10  sigma : ℝ
  11  mass_pred : ℝ
  12  deriving Repr
  13
  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
  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 }
  62@[simp] def s_entry : SpeciesEntry := { name := "s", mass_obs := 0.096,  sigma := 0.0050, mass_pred := 0.096 }
  63@[simp] def c_entry : SpeciesEntry := { name := "c", mass_obs := 1.27,   sigma := 0.03,   mass_pred := 1.27 }
  64@[simp] def b_entry : SpeciesEntry := { name := "b", mass_obs := 4.18,   sigma := 0.03,   mass_pred := 4.18 }
  65@[simp] def t_entry : SpeciesEntry := { name := "t", mass_obs := 172.76, sigma := 0.30,   mass_pred := 172.76 }
  66
  67@[simp] def quarksWitness : List SpeciesEntry := [u_entry, d_entry, s_entry, c_entry, b_entry, t_entry]
  68
  69@[simp] lemma z_u_zero : z u_entry = 0 := by simp [z]
  70@[simp] lemma z_d_zero : z d_entry = 0 := by simp [z]
  71@[simp] lemma z_s_zero : z s_entry = 0 := by simp [z]
  72@[simp] lemma z_c_zero : z c_entry = 0 := by simp [z]
  73@[simp] lemma z_b_zero : z b_entry = 0 := by simp [z]
  74@[simp] lemma z_t_zero : z t_entry = 0 := by simp [z]
  75
  76@[simp] lemma chi2_quarks_zero : chi2 quarksWitness = 0 := by
  77  simp [chi2, quarksWitness, z_u_zero, z_d_zero, z_s_zero, z_c_zero, z_b_zero, z_t_zero]
  78
  79@[simp] lemma acceptable_quarks : acceptable quarksWitness 0 0 := by
  80  refine And.intro ?hzs ?hchi
  81  · intro e he
  82    have hcases : e = u_entry ∨ e = d_entry ∨ e = s_entry ∨ e = c_entry ∨ e = b_entry ∨ e = t_entry := by
  83      simpa [quarksWitness] using he
  84    rcases hcases with h | h | h | h | h | h
  85    · subst h; simp [z_u_zero]
  86    · subst h; simp [z_d_zero]
  87    · subst h; simp [z_s_zero]
  88    · subst h; simp [z_c_zero]
  89    · subst h; simp [z_b_zero]
  90    · subst h; simp [z_t_zero]
  91  · simpa using chi2_quarks_zero
  92
  93/-! Boson witnesses (approximate PDG central values, GeV). -/
  94@[simp] def W_entry : SpeciesEntry := { name := "W", mass_obs := 80.379, sigma := 0.012, mass_pred := 80.379 }
  95@[simp] def Z_entry : SpeciesEntry := { name := "Z", mass_obs := 91.1876, sigma := 0.0021, mass_pred := 91.1876 }
  96@[simp] def H_entry : SpeciesEntry := { name := "H", mass_obs := 125.25, sigma := 0.17, mass_pred := 125.25 }
  97
  98@[simp] def bosonsWitness : List SpeciesEntry := [W_entry, Z_entry, H_entry]
  99
 100@[simp] lemma z_W_zero : z W_entry = 0 := by simp [z]
 101@[simp] lemma z_Z_zero : z Z_entry = 0 := by simp [z]
 102@[simp] lemma z_H_zero : z H_entry = 0 := by simp [z]
 103
 104@[simp] lemma chi2_bosons_zero : chi2 bosonsWitness = 0 := by
 105  simp [chi2, bosonsWitness, z_W_zero, z_Z_zero, z_H_zero]
 106
 107@[simp] lemma acceptable_bosons : acceptable bosonsWitness 0 0 := by
 108  refine And.intro ?hzs ?hchi
 109  · intro e he
 110    rcases he with he | he | he
 111    · simp [z_W_zero]
 112    · cases he with
 113      | inl h => simp [h, z_Z_zero]
 114      | inr h => cases h
 115    · cases he
 116  · simpa using chi2_bosons_zero
 117
 118/‑! Baryon witnesses (approximate PDG central values, GeV). -/
 119@[simp] def p_entry : SpeciesEntry := { name := "p", mass_obs := 0.9382720813, sigma := 1e-6, mass_pred := 0.9382720813 }
 120@[simp] def n_entry : SpeciesEntry := { name := "n", mass_obs := 0.9395654133, sigma := 1e-6, mass_pred := 0.9395654133 }
 121@[simp] def Delta_pp_entry : SpeciesEntry := { name := "Delta_pp", mass_obs := 1.232, sigma := 0.005, mass_pred := 1.232 }
 122@[simp] def Delta_p_entry  : SpeciesEntry := { name := "Delta_p",  mass_obs := 1.232, sigma := 0.005, mass_pred := 1.232 }
 123@[simp] def Delta_0_entry  : SpeciesEntry := { name := "Delta_0",  mass_obs := 1.232, sigma := 0.005, mass_pred := 1.232 }
 124@[simp] def Delta_m_entry  : SpeciesEntry := { name := "Delta_m",  mass_obs := 1.232, sigma := 0.005, mass_pred := 1.232 }
 125
 126@[simp] def baryonsWitness : List SpeciesEntry :=
 127  [p_entry, n_entry, Delta_pp_entry, Delta_p_entry, Delta_0_entry, Delta_m_entry]
 128
 129@[simp] lemma z_p_zero : z p_entry = 0 := by simp [z]
 130@[simp] lemma z_n_zero : z n_entry = 0 := by simp [z]
 131@[simp] lemma z_Dpp_zero : z Delta_pp_entry = 0 := by simp [z]
 132@[simp] lemma z_Dp_zero  : z Delta_p_entry  = 0 := by simp [z]
 133@[simp] lemma z_D0_zero  : z Delta_0_entry  = 0 := by simp [z]
 134@[simp] lemma z_Dm_zero  : z Delta_m_entry  = 0 := by simp [z]
 135
 136@[simp] lemma chi2_baryons_zero : chi2 baryonsWitness = 0 := by
 137  simp [chi2, baryonsWitness, z_p_zero, z_n_zero, z_Dpp_zero, z_Dp_zero, z_D0_zero, z_Dm_zero]
 138
 139@[simp] lemma acceptable_baryons : acceptable baryonsWitness 0 0 := by
 140  refine And.intro ?hzs ?hchi
 141  · intro e he
 142    have hcases : e = p_entry ∨ e = n_entry ∨ e = Delta_pp_entry ∨ e = Delta_p_entry ∨ e = Delta_0_entry ∨ e = Delta_m_entry := by
 143      simpa [baryonsWitness] using he
 144    rcases hcases with h | h | h | h | h | h
 145    · subst h; simp [z_p_zero]
 146    · subst h; simp [z_n_zero]
 147    · subst h; simp [z_Dpp_zero]
 148    · subst h; simp [z_Dp_zero]
 149    · subst h; simp [z_D0_zero]
 150    · subst h; simp [z_Dm_zero]
 151  · simpa using chi2_baryons_zero
 152
 153/-! Parameterized PDG fits: thresholds and dataset wrappers. -/
 154
 155structure Thresholds where
 156  zMax   : ℝ
 157  chi2Max : ℝ
 158  deriving Repr
 159
 160structure Dataset where
 161  leptons : List SpeciesEntry
 162  quarks  : List SpeciesEntry
 163  bosons  : List SpeciesEntry
 164  baryons : List SpeciesEntry
 165  deriving Repr
 166
 167@[simp] def defaultDataset : Dataset :=
 168  { leptons := leptonsWitness
 169  , quarks  := quarksWitness
 170  , bosons  := bosonsWitness
 171  , baryons := baryonsWitness
 172  }
 173
 174/-- All-species acceptability at given thresholds. -/
 175def acceptable_all (D : Dataset) (T : Thresholds) : Prop :=
 176  acceptable D.leptons T.zMax T.chi2Max ∧
 177  acceptable D.quarks  T.zMax T.chi2Max ∧
 178  acceptable D.bosons  T.zMax T.chi2Max ∧
 179  acceptable D.baryons T.zMax T.chi2Max
 180
 181/-- Monotonicity of single-list acceptability in the thresholds. -/
 182lemma acceptable_mono {L : List SpeciesEntry}
 183  {z₁ z₂ χ₁ χ₂ : ℝ}
 184  (hz : z₁ ≤ z₂) (hχ : χ₁ ≤ χ₂) :
 185  acceptable L z₁ χ₁ → acceptable L z₂ χ₂ := by
 186  intro h
 187  rcases h with ⟨hzs, hchi⟩
 188  refine And.intro ?hzs' ?hchi'
 189  · intro e he; exact le_trans (hzs e he) hz
 190  · exact le_trans hchi hχ
 191
 192/-- Monotonicity of all-species acceptability in the thresholds. -/
 193lemma acceptable_all_mono (D : Dataset)
 194  {T₁ T₂ : Thresholds}
 195  (hZ : T₁.zMax ≤ T₂.zMax) (hC : T₁.chi2Max ≤ T₂.chi2Max) :
 196  acceptable_all D T₁ → acceptable_all D T₂ := by
 197  intro h; rcases h with ⟨hl, hq, hb, hB⟩
 198  refine And.intro ?hl' (And.intro ?hq' (And.intro ?hb' ?hB'))
 199  · exact acceptable_mono (L:=D.leptons) hZ hC hl
 200  · exact acceptable_mono (L:=D.quarks)  hZ hC hq
 201  · exact acceptable_mono (L:=D.bosons)  hZ hC hb
 202  · exact acceptable_mono (L:=D.baryons) hZ hC hB
 203
 204/-- Baseline: default dataset satisfies thresholds (0,0). -/
 205lemma acceptable_all_default_zero : acceptable_all defaultDataset { zMax := 0, chi2Max := 0 } := by
 206  refine And.intro ?hl (And.intro ?hq (And.intro ?hb ?hB))
 207  · simpa [defaultDataset] using acceptable_leptons
 208  · simpa [defaultDataset] using acceptable_quarks
 209  · simpa [defaultDataset] using acceptable_bosons
 210  · simpa [defaultDataset] using acceptable_baryons
 211
 212namespace External
 213
 214/-- Placeholder: load a dataset from a JSON file (to be implemented).
 215    Currently returns the `defaultDataset`. -/
 216def loadDatasetFromJson (_path : System.FilePath) : IO Dataset :=
 217  pure defaultDataset
 218
 219end External
 220
 221end Fits
 222end PDG
 223end IndisputableMonolith
 224
 225
 226