def
definition
V_us_from_bridge
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RecogSpec.RSBridge on GitHub at line 104.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
101
102The Cabibbo angle is a golden projection minus electromagnetic correction.
103-/
104noncomputable def V_us_from_bridge (B : RSBridge L) (φ : ℝ) : ℝ :=
105 φ ^ B.phiProj - B.radCoeff * B.alphaExponent
106
107/-! ## The Canonical RSBridge -/
108
109/-- The canonical RS bridge with standard geometric parameters -/
110noncomputable def canonicalRSBridge (L : RSLedger) : RSBridge L where
111 toBridge := { dummy := () }
112 edgeDual := 24
113 alphaExponent := alphaLock -- The RS fine structure formula
114 phiProj := -3
115 radCoeff := 3/2
116
117/-- The canonical bridge has edge dual = 24 -/
118@[simp] theorem canonicalRSBridge_edgeDual (L : RSLedger) :
119 (canonicalRSBridge L).edgeDual = 24 := rfl
120
121/-- The canonical bridge has alpha from ILG -/
122@[simp] theorem canonicalRSBridge_alpha (L : RSLedger) :
123 (canonicalRSBridge L).alphaExponent = alphaLock := rfl
124
125/-! ## Canonical Mixing Angle Values -/
126
127/-- V_cb = 1/24 for canonical bridge -/
128theorem canonical_V_cb (L : RSLedger) :
129 V_cb_from_bridge (canonicalRSBridge L) = 1 / 24 := by
130 simp [V_cb_from_bridge, canonicalRSBridge]
131
132/-- V_ub = alphaLock/2 for canonical bridge -/
133theorem canonical_V_ub (L : RSLedger) :
134 V_ub_from_bridge (canonicalRSBridge L) = alphaLock / 2 := by