`unitarity_triangle_valid`

proved

show as: view math explainer →

module: IndisputableMonolith.StandardModel.CKMMatrix
domain: StandardModel
line: 254 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.StandardModel.CKMMatrix on GitHub at line 254.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 251  unfold wolfenstein_rho; constructor <;> norm_num
 252
 253/-- The unitarity constraint ρ̄² + η̄² < 1 holds (required for V unitary). -/
 254theorem unitarity_triangle_valid :
 255    wolfenstein_rho^2 + wolfenstein_eta^2 < 1 := by
 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. -/
 275def experimentalValues : List (String × ℝ × ℝ) := [
 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:

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.