`triangle_sum`

proved

show as: view math explainer →

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

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

 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 φ
 207    3. η/ρ ≈ φ (possible?)
 208    4. Unitarity triangle angles ≈ φ-related
 209
 210    These would be profound if verified! -/
 211def predictions : List String := [
 212  "λ ≈ (φ - 1)²/φ ≈ 0.236",
 213  "A might be φ-related",
 214  "CP phase η from 8-tick asymmetry",
 215  "Unitarity angles constrained by φ"
 216]
 217
 218/-! ## RS Derivation of ρ̄ and η̄ from Jarlskog Invariant
 219
 220The Wolfenstein parameters ρ̄, η̄ parametrize the unitarity triangle:
 221  ρ̄ + iη̄ = −V_ud V_ub* / (V_cd V_cb*)
 222
 223With δ_CKM = π/2 (proved in CPPhaseDerivation), both ρ̄ and η̄ are positive.
 224
 225The Jarlskog invariant J_CP = A²λ⁶η̄(1 − λ²/2)² ≈ A²λ⁶η̄.
 226With A = 9/11, λ ≈ 0.236, J_CP ≈ 3.05 × 10⁻⁵:

papers checked against this theorem

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