`experimentalValues`

definition

show as: view math explainer →

module: IndisputableMonolith.StandardModel.CKMMatrix
domain: StandardModel
line: 275 · 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 275.

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

 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:
 285    1. No φ-connection to λ (Cabibbo angle)
 286    2. CP violation has different origin than 8-tick
 287    3. Unitarity violated -/
 288structure CKMFalsifier where
 289  no_phi_lambda : Prop
 290  different_cp_origin : Prop
 291  unitarity_violated : Prop
 292  falsified : no_phi_lambda ∧ different_cp_origin ∧ unitarity_violated → False
 293
 294end CKMMatrix
 295end StandardModel
 296end IndisputableMonolith

papers checked against this theorem

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