phi_inv3_lower_bound

formal source

 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. -/
 165theorem V_us_match : abs (V_us_pred - V_us_exp) < V_us_err := by
 166  have h_alpha_lower := alpha_lower_bound
 167  have h_alpha_upper := alpha_upper_bound
 168  have h_phi3_lower := phi_inv3_lower_bound
 169  have h_phi3_upper := phi_inv3_upper_bound
 170  simp only [V_us_pred, V_us_exp, V_us_err, torsion_overlap, cabibbo_radiative_correction]
 171  -- V_us_pred = phi^(-3) - 1.5*alpha
 172  -- phi^(-3) ∈ (0.2360, 0.2361)
 173  -- 1.5*alpha ∈ (0.010935, 0.010965)
 174  -- V_us_pred ∈ (0.2360 - 0.010965, 0.2361 - 0.010935) = (0.225035, 0.225165)
 175  have h_correction_lower : (0.010935 : ℝ) < (3/2) * Constants.alpha := by linarith
 176  have h_correction_upper : (3/2) * Constants.alpha < (0.010965 : ℝ) := by linarith
 177  have h_pred_lower : (0.225035 : ℝ) < Constants.phi ^ (-3 : ℤ) - (3/2) * Constants.alpha := by linarith
 178  have h_pred_upper : Constants.phi ^ (-3 : ℤ) - (3/2) * Constants.alpha < (0.225165 : ℝ) := by linarith
 179  -- |V_us_pred - 0.22500| ≤ max(|0.225035 - 0.22500|, |0.225165 - 0.22500|)
 180  --                      = max(0.000035, 0.000165) = 0.000165 < 0.00067