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

experimentalValues

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)

 275def experimentalValues : List (String × ℝ × ℝ) := [

proof body

Definition body.

 276  ("V_ud", 0.97373, 0.00031),
 277  ("V_us", 0.2243, 0.0008),
 278  ("V_ub", 0.00382, 0.0002),
 279  ("V_cb", 0.0408, 0.0014)
 280]
 281
 282/-! ## Falsification Criteria -/
 283
 284/-- The derivation would be falsified if:
 285    1. No φ-connection to λ (Cabibbo angle)
 286    2. CP violation has different origin than 8-tick
 287    3. Unitarity violated -/

depends on (11)

Lean names referenced from this declaration's body.