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

experiments

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)

 321def experiments : List String := [

proof body

Definition body.

 322  "DUNE: δ_CP precision",
 323  "Hyper-Kamiokande: θ₂₃, CP violation",
 324  "JUNO: θ₁₂, mass ordering",
 325  "Neutrinoless double beta decay"
 326]
 327
 328/-! ## Falsification Criteria -/
 329
 330/-- The derivation would be falsified if:
 331    1. No φ-connection to any mixing angle
 332    2. Inverted mass ordering confirmed
 333    3. δ_CP far from π (e.g., ~0 or π/2) -/

used by (26)

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

depends on (7)

Lean names referenced from this declaration's body.