lemma
proved
log_phi_lt_0483
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Numerics.Interval.AlphaBounds on GitHub at line 183.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
200 _ < w8_from_eight_tick * log IndisputableMonolith.Constants.phi := by
201 exact mul_lt_mul_of_pos_left h_log_lo h_w8_pos
202
203/-- Stronger lower bound for the gap term using log(φ) > 0.481. -/
204theorem f_gap_gt_strong : (1.1979 : ℝ) < f_gap := by
205 simp only [f_gap]
206 have h_w8_lo := W8Bounds.w8_computed_gt
207 have h_log_lo := log_phi_gt_0481
208 have h_w8_pos : 0 < w8_from_eight_tick := IndisputableMonolith.Constants.w8_pos
209 have h0481 : 0 < (0.481 : ℝ) := by norm_num
210 calc (1.1979 : ℝ) < 2.490564399 * (0.481 : ℝ) := by norm_num
211 _ < w8_from_eight_tick * (0.481 : ℝ) := by
212 exact mul_lt_mul_of_pos_right h_w8_lo h0481
213 _ < w8_from_eight_tick * log IndisputableMonolith.Constants.phi := by