V_cb_exp

formal source

  48def V_us_exp : ℝ := 0.22500
  49def V_us_err : ℝ := 0.00067
  50
  51def V_cb_exp : ℝ := 0.04182
  52def V_cb_err : ℝ := 0.00085
  53
  54def V_ub_exp : ℝ := 0.00369
  55def V_ub_err : ℝ := 0.00011
  56
  57/-! ## Theoretical Predictions -/
  58
  59/-- V_ub is half the fine-structure constant (fine_structure_leakage). -/
  60noncomputable def V_ub_pred : ℝ := fine_structure_leakage
  61
  62/-- V_cb geometric ratio: 1/vertex_edge_slots = 1/24. -/
  63def V_cb_geom : ℚ := edge_dual_ratio
  64
  65/-- V_cb is the inverse of twice the total edge count (1/24). -/
  66noncomputable def V_cb_pred : ℝ := (V_cb_geom : ℝ)
  67
  68/-- V_us is the golden projection (torsion_overlap) minus a radiative correction. -/
  69noncomputable def V_us_pred : ℝ := torsion_overlap - cabibbo_radiative_correction
  70
  71/-! ## Geometric Derivation -/
  72
  73/-- V_cb derives from cube edge geometry: 1/(2 * 12) = 1/24. -/
  74theorem V_cb_from_cube_edges :
  75    V_cb_geom = 1 / (2 * cube_edges 3) := by
  76  simp only [V_cb_geom, edge_dual_ratio, cube_edges]
  77  norm_num
  78
  79/-! ## Verification Theorems -/
  80
  81/-- V_cb matches within 1 sigma.