`measurements`

definition

show as: view math explainer →

module: IndisputableMonolith.StandardModel.WeinbergAngle
domain: StandardModel
line: 205 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.StandardModel.WeinbergAngle on GitHub at line 205.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 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
 231end IndisputableMonolith

papers checked against this theorem

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