  89  simp [V_cb_from_bridge, hB]
  90
  91/-- V_cb as a real number -/
  92noncomputable def V_cb_real (B : RSBridge L) : ℝ := (V_cb_from_bridge B : ℝ)
  93
  94/-- V_ub from fine structure: α/2
  95
  96The smallest CKM element is half the fine structure constant.
  97-/
  98noncomputable def V_ub_from_bridge (B : RSBridge L) : ℝ := B.alphaExponent / 2
  99
 100/-- V_us from golden projection with radiative correction: φ^{-3} - (3/2)α
 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) :

papers checked against this theorem

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