`log_phi_gt_048`

proved

show as: view math explainer →

module: IndisputableMonolith.Numerics.Interval.AlphaBounds
domain: Numerics
line: 169 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Numerics.Interval.AlphaBounds on GitHub at line 169.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 166    exact_mod_cast exp_0483_taylor_floor
 167  exact lt_of_lt_of_le h_num h_lower
 168
 169private lemma log_phi_gt_048 : (0.48 : ℝ) < log IndisputableMonolith.Constants.phi := by
 170  rw [Real.lt_log_iff_exp_lt IndisputableMonolith.Constants.phi_pos]
 171  have hphi_lo : (((16161 / 10000 : ℚ) : ℝ)) < IndisputableMonolith.Constants.phi := by
 172    have hphi : (1.61803395 : ℝ) < IndisputableMonolith.Constants.phi := W8Bounds.phi_gt_161803395
 173    linarith
 174  exact lt_trans exp_048_lt hphi_lo
 175
 176private lemma log_phi_gt_0481 : (0.481 : ℝ) < log IndisputableMonolith.Constants.phi := by
 177  rw [Real.lt_log_iff_exp_lt IndisputableMonolith.Constants.phi_pos]
 178  have hphi_lo : (((16177 / 10000 : ℚ) : ℝ)) < IndisputableMonolith.Constants.phi := by
 179    have hphi : (1.61803395 : ℝ) < IndisputableMonolith.Constants.phi := W8Bounds.phi_gt_161803395
 180    linarith
 181  exact lt_trans exp_0481_lt hphi_lo
 182
 183private lemma log_phi_lt_0483 : log IndisputableMonolith.Constants.phi < (0.483 : ℝ) := by
 184  rw [Real.log_lt_iff_lt_exp IndisputableMonolith.Constants.phi_pos]
 185  have hphi_hi : IndisputableMonolith.Constants.phi < (((16209 / 10000 : ℚ) : ℝ)) := by
 186    have hphi : IndisputableMonolith.Constants.phi < (1.6180340 : ℝ) := W8Bounds.phi_lt_16180340
 187    linarith
 188  exact lt_trans hphi_hi exp_0483_gt
 189
 190theorem f_gap_gt : (1.195 : ℝ) < f_gap := by
 191  simp only [f_gap]
 192  have h_w8_lo := W8Bounds.w8_computed_gt
 193  have h_log_lo := log_phi_gt_048
 194  have h_w8_pos : 0 < w8_from_eight_tick := IndisputableMonolith.Constants.w8_pos
 195  have h048 : 0 < (0.48 : ℝ) := by norm_num
 196  -- f_gap = w8 * log(phi) > 2.490564399 * 0.48 = 1.19547...
 197  calc (1.195 : ℝ) < 2.490564399 * (0.48 : ℝ) := by norm_num
 198    _ < w8_from_eight_tick * (0.48 : ℝ) := by
 199      exact mul_lt_mul_of_pos_right h_w8_lo h048

papers checked against this theorem

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