`cp_violation_small`

proved

show as: view math explainer →

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

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

 173noncomputable def jarlskogInvariant : ℝ := 3e-5
 174
 175/-- **THEOREM**: CP violation is small but nonzero. -/
 176theorem cp_violation_small :
 177    jarlskogInvariant > 0 ∧ jarlskogInvariant < 1e-4 := by
 178  unfold jarlskogInvariant
 179  constructor <;> norm_num
 180
 181/-! ## Unitarity Triangle -/
 182
 183/-- The unitarity of the CKM matrix gives constraints:
 184
 185    V_ud V_ub* + V_cd V_cb* + V_td V_tb* = 0
 186
 187    This forms a triangle in the complex plane.
 188    The angles α, β, γ are related to CP violation.
 189
 190    RS predicts these angles are φ-related. -/
 191noncomputable def unitarityAngle_alpha : ℝ := 85  -- degrees
 192noncomputable def unitarityAngle_beta : ℝ := 22   -- degrees
 193noncomputable def unitarityAngle_gamma : ℝ := 73  -- degrees
 194
 195/-- **THEOREM**: Unitarity triangle angles sum to 180°. -/
 196theorem triangle_sum :
 197    unitarityAngle_alpha + unitarityAngle_beta + unitarityAngle_gamma = 180 := by
 198  unfold unitarityAngle_alpha unitarityAngle_beta unitarityAngle_gamma
 199  norm_num
 200
 201/-! ## φ-Predictions for CKM -/
 202
 203/-- RS predictions for CKM parameters:
 204
 205    1. λ ≈ (φ - 1)² / φ ≈ 0.236 (vs observed 0.227)
 206    2. A ≈ related to φ

papers checked against this theorem

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