 197    | APV (Cs) | 0.2356 | 0.0020 |
 198
 199    The variation with energy ("running") is also measured. -/
 200structure ExperimentalMeasurement where
 201  name : String
 202  value : ℝ
 203  error : ℝ
 204
 205def measurements : List ExperimentalMeasurement := [
 206  ⟨"LEP Z-pole", 0.2312, 0.0002⟩,
 207  ⟨"SLD asymmetries", 0.2310, 0.0002⟩,
 208  ⟨"Average (PDG)", 0.2229, 0.0003⟩
 209]
 210
 211/-! ## Falsification Criteria -/
 212
 213/-- The derivation would be falsified if:
 214    1. No consistent φ-expression matches the observed value
 215    2. Running with energy doesn't follow φ-ladder
 216    3. GUT unification fails -/
 217structure WeinbergAngleFalsifier where
 218  /-- φ-predictions don't match observation to within 5% -/
 219  phi_mismatch : Prop
 220  /-- Running doesn't follow predicted pattern -/
 221  running_mismatch : Prop
 222  /-- Falsification condition -/
 223  falsified : phi_mismatch ∨ running_mismatch → False
 224
 225/-- Current status: Promising but incomplete. -/
 226def derivationStatus : String :=
 227  "sin²(θ_W) = (3 - φ)/6 gives 0.230, within 3% of observed 0.2229. Promising!"
 228
 229end WeinbergAngle
 230end StandardModel

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.