def definition def or abbrev

`experimentalStatus`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 209def experimentalStatus : List GenerationFalsifier := [

proof body

Definition body.

 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

depends on (7)

Lean names referenced from this declaration's body.

from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
Z in IndisputableMonolith.Masses.Anchor decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
Z in IndisputableMonolith.Physics.AnchorPolicyCertified decl_use
GenerationFalsifier in IndisputableMonolith.Physics.ThreeGenerations decl_use
width in IndisputableMonolith.Recognition.Certification decl_use