pith. machine review for the scientific record. sign in
theorem proved term proof

unitarity_triangle_valid

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)

 254theorem unitarity_triangle_valid :
 255    wolfenstein_rho^2 + wolfenstein_eta^2 < 1 := by

proof body

Term-mode proof.

 256  unfold wolfenstein_rho wolfenstein_eta; norm_num
 257
 258/-! ## Experimental Verification -/
 259
 260/-- CKM elements are precisely measured:
 261
 262    | Element | Value | Error |
 263    |---------|-------|-------|
 264    | V_ud | 0.97373 | 0.00031 |
 265    | V_us | 0.2243 | 0.0008 |
 266    | V_ub | 0.00382 | 0.00020 |
 267    | V_cd | 0.221 | 0.004 |
 268    | V_cs | 0.975 | 0.006 |
 269    | V_cb | 0.0408 | 0.0014 |
 270    | V_td | 0.0080 | 0.0003 |
 271    | V_ts | 0.0388 | 0.0011 |
 272    | V_tb | 1.013 | 0.030 |
 273
 274    The hierarchy |V_ub| << |V_cb| << |V_us| is evident. -/

depends on (20)

Lean names referenced from this declaration's body.