theorem
proved
f_gap_gt
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Numerics.Interval.AlphaBounds on GitHub at line 190.
browse module
All declarations in this module, on Recognition.
explainer page
Derivations using this theorem
depends on
formal source
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
214 exact mul_lt_mul_of_pos_left h_log_lo h_w8_pos
215
216theorem f_gap_lt : f_gap < (1.203 : ℝ) := by
217 simp only [f_gap]
218 have h_w8_hi := W8Bounds.w8_computed_lt
219 have h_log_hi := log_phi_lt_0483
220 have h_w8_pos : 0 < w8_from_eight_tick := IndisputableMonolith.Constants.w8_pos