def
definition
wolfenstein_eta
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.StandardModel.CKMMatrix on GitHub at line 63.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
91 Too large compared to observed 0.227. -/
92noncomputable def hypothesis1 : ℝ := 1 / (2 * phi)
93