def
definition
wolfenstein_rho
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 60.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
85/-! ## φ-Connection Hypotheses -/
86
87/-- Hypothesis 1: λ = sin(θ_c) = 1/(2φ)
88
89 1/(2 × 1.618) = 1/3.236 = 0.309
90