V_ub_match

formal source

 131    Proof: From alpha bounds (0.00729, 0.00731), we get
 132    alpha/2 ∈ (0.003645, 0.003655), and
 133    |0.00365 - 0.00369| = 0.00004 < 0.00011. -/
 134theorem V_ub_match : abs (V_ub_pred - V_ub_exp) < V_ub_err := by
 135  have h_alpha_lower := alpha_lower_bound
 136  have h_alpha_upper := alpha_upper_bound
 137  simp only [V_ub_pred, V_ub_exp, V_ub_err, fine_structure_leakage]
 138  -- alpha/2 ∈ (0.003645, 0.003655)
 139  have h_lower : (0.003645 : ℝ) < Constants.alpha / 2 := by linarith
 140  have h_upper : Constants.alpha / 2 < (0.003655 : ℝ) := by linarith
 141  -- |alpha/2 - 0.00369| ≤ max(|0.003645 - 0.00369|, |0.003655 - 0.00369|)
 142  --                     = max(0.000045, 0.000035) = 0.000045 < 0.00011
 143  rw [abs_lt]
 144  constructor <;> linarith
 145
 146/-- Bounds on phi^(-3) needed for V_us proof.
 147    φ^(-3) ≈ 0.2360679...
 148
 149    These bounds are derived from phi_tight_bounds via antitonicity. -/
 150theorem phi_inv3_lower_bound : (0.2360 : ℝ) < phi ^ (-3 : ℤ) :=
 151  Numerics.phi_inv3_zpow_bounds.1
 152
 153theorem phi_inv3_upper_bound : phi ^ (-3 : ℤ) < (0.2361 : ℝ) :=
 154  Numerics.phi_inv3_zpow_bounds.2
 155
 156/-- V_us matches within 1 sigma.
 157
 158    V_us_pred = φ^(-3) - (3/2)*α
 159              ≈ 0.2360679 - 0.01095
 160              ≈ 0.2251
 161    V_us_exp = 0.22500
 162    |V_us_pred - V_us_exp| ≈ 0.0001 < 0.00067 ✓
 163
 164    Proof: From bounds on φ^(-3) and α, we establish the match. -/