V_cb_from_bridge

formal source

  81
  82This is EXACT — the mixing is the inverse of the dual edge count.
  83-/
  84def V_cb_from_bridge (B : RSBridge L) : ℚ := 1 / B.edgeDual
  85
  86/-- V_cb = 1/24 for canonical bridge -/
  87theorem V_cb_canonical (B : RSBridge L) (hB : B.edgeDual = 24) :
  88    V_cb_from_bridge B = 1 / 24 := by
  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