def
definition
wolfenstein_lambda
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.StandardModel.CKMMatrix on GitHub at line 54.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
51 constructor <;> norm_num
52
53/-- The Wolfenstein parameter λ = sin(θ_c) ≈ 0.227. -/
54noncomputable def wolfenstein_lambda : ℝ := cabibboAngle
55
56/-- The Wolfenstein parameter A ≈ 0.82. -/
57noncomputable def wolfenstein_A : ℝ := 0.82
58
59/-- The Wolfenstein parameter ρ ≈ 0.14. -/
60noncomputable def wolfenstein_rho : ℝ := 0.14
61
62/-- The Wolfenstein parameter η ≈ 0.35 (CP violation phase). -/
63noncomputable def wolfenstein_eta : ℝ := 0.35
64
65/-! ## The Wolfenstein Parametrization -/
66
67/-- The CKM matrix in Wolfenstein parametrization (to O(λ³)):
68
69 ⎛ 1 - λ²/2 λ Aλ³(ρ - iη) ⎞
70V = ⎜ -λ 1 - λ²/2 Aλ² ⎟
71 ⎝ Aλ³(1-ρ-iη) -Aλ² 1 ⎠
72-/
73noncomputable def V_ud : ℂ := 1 - wolfenstein_lambda^2 / 2
74noncomputable def V_us : ℂ := wolfenstein_lambda
75noncomputable def V_ub : ℂ := wolfenstein_A * wolfenstein_lambda^3 *
76 (wolfenstein_rho - I * wolfenstein_eta)
77noncomputable def V_cd : ℂ := -wolfenstein_lambda
78noncomputable def V_cs : ℂ := 1 - wolfenstein_lambda^2 / 2
79noncomputable def V_cb : ℂ := wolfenstein_A * wolfenstein_lambda^2
80noncomputable def V_td : ℂ := wolfenstein_A * wolfenstein_lambda^3 *
81 (1 - wolfenstein_rho - I * wolfenstein_eta)
82noncomputable def V_ts : ℂ := -wolfenstein_A * wolfenstein_lambda^2
83noncomputable def V_tb : ℂ := 1
84