def
definition
unitarityAngle_beta
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.StandardModel.CKMMatrix on GitHub at line 192.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
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 φ
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