V_us_match

formal source

 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
 181  rw [abs_lt]
 182  constructor <;> linarith
 183
 184/-! ## Certificate -/
 185
 186/-- T11 Certificate: V_cb from cube edge geometry. -/
 187structure T11Cert where
 188  /-- V_cb = 1/(2*12) = 1/24 from cube edges. -/
 189  geometric_origin : V_cb_geom = 1 / (2 * cube_edges 3)
 190  /-- The prediction matches experiment within uncertainty. -/
 191  matches_pdg : abs (V_cb_pred - V_cb_exp) < V_cb_err
 192
 193/-- The T11 certificate (for V_cb) is verified. -/
 194def t11_V_cb_verified : T11Cert where
 195  geometric_origin := V_cb_from_cube_edges