`experimentalTests`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.ThreeGenerations
domain: Physics
line: 188 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.ThreeGenerations on GitHub at line 188.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 185    2. Precision measurement of Z → νν̄ (gives N_ν ≈ 3)
 186    3. Check if mass ratios follow φ^n pattern
 187    4. Test CKM/PMNS structure against RS predictions -/
 188def experimentalTests : List String := [
 189  "LEP Z-width: N_ν = 2.984 ± 0.008",
 190  "LHC: No 4th generation quarks up to TeV scale",
 191  "Mass ratios approximately follow φ^n",
 192  "CKM unitarity verified to 10⁻⁴"
 193]
 194
 195/-! ## Falsification Criteria -/
 196
 197/-- The 3-generation derivation would be falsified by:
 198    1. Discovery of a 4th generation
 199    2. Z-width giving N_ν ≠ 3
 200    3. Mass ratios not following φ-pattern
 201    4. Alternative derivation giving different number -/
 202structure GenerationFalsifier where
 203  /-- Type of potential falsification. -/
 204  falsifier : String
 205  /-- Current experimental status. -/
 206  status : String
 207
 208/-- Current experimental status strongly supports 3 generations. -/
 209def experimentalStatus : List GenerationFalsifier := [
 210  ⟨"4th generation search", "Ruled out for SM-like particles"⟩,
 211  ⟨"Z-width measurement", "N_ν = 2.984 ± 0.008 ≈ 3"⟩,
 212  ⟨"Cosmological bounds", "N_eff ≈ 3 from BBN and CMB"⟩
 213]
 214
 215end ThreeGenerations
 216end Physics
 217end IndisputableMonolith

papers checked against this theorem

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