IndisputableMonolith.Data.Import

   1import Mathlib.Data.List.Basic
   2import Mathlib.Data.Real.Basic
   3
   4namespace IndisputableMonolith.Data
   5
   6structure Measurement where
   7  name : String
   8  value : ℝ
   9  error : ℝ
  10
  11/-- Hardcoded measurements for now (JSON parsing blocked by Mathlib version). -/
  12def import_measurements : List Measurement :=
  13  [
  14    { name := "AlphaInvPrediction", value := (137.035999084 : ℝ), error := (0.000000084 : ℝ) },
  15    { name := "Sin2ThetaW_at_MZ", value := (0.23121 : ℝ), error := (0.00004 : ℝ) },
  16    { name := "AlphaS_at_MZ", value := (0.1179 : ℝ), error := (0.0009 : ℝ) },
  17    { name := "ElectronG2", value := (0.00115965218073 : ℝ), error := (2.8e-13 : ℝ) },
  18    { name := "MuonG2", value := (0.00116592062 : ℝ), error := (4.1e-10 : ℝ) },
  19    { name := "MW_over_MZ", value := (0.88153 : ℝ), error := (0.00018 : ℝ) }
  20  ]
  21
  22end IndisputableMonolith.Data
  23