`ratio_mu_e_exp`

definition

show as: view math explainer →

module: IndisputableMonolith.Masses.Verification
domain: Masses
line: 165 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Masses.Verification on GitHub at line 165.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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
 185    _ < Real.goldenRatio ^ 8 * Real.goldenRatio ^ 3 := by nlinarith
 186
 187private lemma phi11_lt : Constants.phi ^ (11 : ℕ) < (200 : ℝ) := by
 188  rw [phi_eq_goldenRatio]
 189  have h8 := Numerics.phi_pow8_lt
 190  have h3 := Numerics.phi_cubed_lt
 191  have hpos : (0 : ℝ) < Real.goldenRatio ^ 3 := by positivity
 192  have heq : Real.goldenRatio ^ 11 = Real.goldenRatio ^ 8 * Real.goldenRatio ^ 3 := by ring_nf
 193  rw [heq]
 194  calc Real.goldenRatio ^ 8 * Real.goldenRatio ^ 3
 195      < (46.99 : ℝ) * Real.goldenRatio ^ 3 := by nlinarith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.