pith. machine review for the scientific record. sign in
def definition def or abbrev

experimentalTests

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 188def experimentalTests : List String := [

proof body

Definition body.

 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 -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.