pith. machine review for the scientific record. sign in
theorem proved term proof

triangle_sum

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 196theorem triangle_sum :
 197    unitarityAngle_alpha + unitarityAngle_beta + unitarityAngle_gamma = 180 := by

proof body

Term-mode proof.

 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! -/

depends on (7)

Lean names referenced from this declaration's body.