def
definition
log_lower_bound_phi_hypothesis
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RSBridge.GapProperties on GitHub at line 320.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
317 exact h
318
319/-- Hypothesis: log(1.618033) > 0.481211 (verified externally via Taylor expansion) -/
320def log_lower_bound_phi_hypothesis : Prop := (0.481211 : ℝ) < Real.log (1.618033 : ℝ)
321
322/-- Hypothesis: log(1.618034) < 0.481213 (verified externally via Taylor expansion) -/
323def log_upper_bound_phi_hypothesis : Prop := Real.log (1.618034 : ℝ) < (0.481213 : ℝ)
324
325/-- log(φ) is bounded: log(φ) ∈ (0.481211, 0.481213) -/
326lemma log_phi_bounds (h_low : log_lower_bound_phi_hypothesis) (h_high : log_upper_bound_phi_hypothesis) :
327 (0.481211 : ℝ) < Real.log phi ∧ Real.log phi < (0.481213 : ℝ) := by
328 have hphi := phi_bounds
329 have h_low' : (0.481211 : ℝ) < Real.log (1.618033 : ℝ) := by
330 simpa [log_lower_bound_phi_hypothesis] using h_low
331 have h_high' : Real.log (1.618034 : ℝ) < (0.481213 : ℝ) := by
332 simpa [log_upper_bound_phi_hypothesis] using h_high
333 constructor
334 · -- Lower bound: log(φ) > log(1.618033) > 0.481211
335 have h_mono : Real.log (1.618033 : ℝ) < Real.log phi := by
336 apply Real.log_lt_log (by norm_num) hphi.1
337 exact lt_trans h_low' h_mono
338 · -- Upper bound: log(φ) < log(1.618034) < 0.481213
339 have h_mono : Real.log phi < Real.log (1.618034 : ℝ) := by
340 apply Real.log_lt_log (by linarith [hphi.1]) hphi.2
341 exact lt_trans h_mono h_high'
342
343/-! ### Auxiliary numerical log bounds -/
344
345/-- Hypothesis for numerical lower bound: log(1 + 24/1.618034) > 2.7613 -/
346def log_15p83_lower_hypothesis : Prop := (2.7613 : ℝ) < Real.log (1 + 24 / (1.618034 : ℝ))
347
348/-- Hypothesis for numerical upper bound: log(1 + 24/1.618033) < 2.7615 -/
349def log_15p83_upper_hypothesis : Prop := Real.log (1 + 24 / (1.618033 : ℝ)) < (2.7615 : ℝ)
350