V_cb_from_cube_edges

formal source

  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.
  82
  83    pred = 1/24 ≈ 0.04166666...
  84    obs  = 0.04182
  85    err  = 0.00085
  86    |pred - obs| = |0.04166 - 0.04182| = 0.00016 < 0.00085 ✓
  87
  88    This is now PROVEN, not axiomatized. -/
  89theorem V_cb_match : abs (V_cb_pred - V_cb_exp) < V_cb_err := by
  90  simp only [V_cb_pred, V_cb_geom, V_cb_exp, V_cb_err, edge_dual_ratio]
  91  norm_num
  92
  93/-- Bounds on alpha needed for CKM proofs.
  94    alphaInv ≈ 137.036 so alpha ≈ 0.00730
  95    NOTE: These bounds are verified numerically but require transcendental
  96    computation (involving π and ln(φ)) that norm_num cannot handle. -/
  97theorem alpha_lower_bound : (0.00729 : ℝ) < Constants.alpha := by
  98  -- From the rigorous interval proof: alphaInv < 137.039 ⇒ 1/137.039 < alpha
  99  have h_inv_lt : Constants.alphaInv < (137.039 : ℝ) := by
 100    simpa [Constants.alphaInv] using (IndisputableMonolith.Numerics.alphaInv_lt)
 101  have h_inv_pos : (0 : ℝ) < Constants.alphaInv := by
 102    have h := IndisputableMonolith.Numerics.alphaInv_gt
 103    linarith
 104  -- Invert inequality (antitone on positive reals).