theorem
proved
phi_inv3_upper_bound
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.CKMGeometry on GitHub at line 153.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
181 rw [abs_lt]
182 constructor <;> linarith
183