def
definition
canonicalRSBridge
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RecogSpec.RSBridge on GitHub at line 110.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
135 simp [V_ub_from_bridge, canonicalRSBridge]
136
137/-- V_us formula for canonical bridge -/
138theorem canonical_V_us (L : RSLedger) :
139 V_us_from_bridge (canonicalRSBridge L) phi =
140 phi ^ (-3 : ℤ) - (3/2 : ℚ) * alphaLock := by