theorem
proved
tau_relative_error
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Masses.Verification on GitHub at line 154.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
151 calc Constants.phi ^ 76 < (7646046000000000 : ℝ) := phi76_lt
152 _ < (1823 : ℝ) * 4194304000000 := by norm_num
153
154theorem tau_relative_error :
155 |rs_mass_MeV .Lepton 19 - m_tau_exp| / m_tau_exp < 0.03 := by
156 rw [tau_pred_eq]
157 have hb := tau_mass_bounds
158 have hexp_pos : (0 : ℝ) < m_tau_exp := by unfold m_tau_exp; norm_num
159 rw [div_lt_iff₀ hexp_pos, abs_lt]
160 unfold m_tau_exp
161 constructor <;> nlinarith [hb.1, hb.2]
162
163/-! ## Mass Ratio Verification -/
164
165noncomputable def ratio_mu_e_exp : ℝ := m_mu_exp / m_e_exp
166noncomputable def ratio_tau_e_exp : ℝ := m_tau_exp / m_e_exp
167
168theorem ratio_mu_e_exp_bounds :
169 (206.76 : ℝ) < ratio_mu_e_exp ∧ ratio_mu_e_exp < (206.77 : ℝ) := by
170 unfold ratio_mu_e_exp m_mu_exp m_e_exp; constructor <;> norm_num
171
172theorem ratio_tau_e_exp_bounds :
173 (3477 : ℝ) < ratio_tau_e_exp ∧ ratio_tau_e_exp < (3478 : ℝ) := by
174 unfold ratio_tau_e_exp m_tau_exp m_e_exp; constructor <;> norm_num
175
176private lemma phi11_gt : (198.9 : ℝ) < Constants.phi ^ (11 : ℕ) := by
177 rw [phi_eq_goldenRatio]
178 have h8 := Numerics.phi_pow8_gt
179 have h3 := Numerics.phi_cubed_gt
180 have hpos : (0 : ℝ) < Real.goldenRatio ^ 8 := by positivity
181 have heq : Real.goldenRatio ^ 11 = Real.goldenRatio ^ 8 * Real.goldenRatio ^ 3 := by ring_nf
182 rw [heq]
183 calc (198.9 : ℝ) < (46.97 : ℝ) * (4.236 : ℝ) := by norm_num
184 _ < Real.goldenRatio ^ 8 * (4.236 : ℝ) := by nlinarith