cabibboAngle

formal source

  43/-! ## Observed CKM Elements -/
  44
  45/-- The Cabibbo angle θ_c (mixing between 1st and 2nd generation). -/
  46noncomputable def cabibboAngle : ℝ := 0.227  -- sin(θ_c) ≈ 0.227
  47
  48/-- **THEOREM**: sin(θ_c) ≈ 0.227 (the Cabibbo angle). -/
  49theorem cabibbo_value : cabibboAngle > 0.22 ∧ cabibboAngle < 0.23 := by
  50  unfold cabibboAngle
  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)