`log_phi_bounds`

proved

show as: view math explainer →

module: IndisputableMonolith.RSBridge.GapProperties
domain: RSBridge
line: 326 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RSBridge.GapProperties on GitHub at line 326.

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

 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
 351/-- Hypothesis for numerical lower bound: log(1 + 276/1.618034) > 5.1442 -/
 352def log_171p6_lower_hypothesis : Prop := (5.1442 : ℝ) < Real.log (1 + 276 / (1.618034 : ℝ))
 353
 354/-- Hypothesis for numerical upper bound: log(1 + 276/1.618033) < 5.1444 -/
 355def log_171p6_upper_hypothesis : Prop := Real.log (1 + 276 / (1.618033 : ℝ)) < (5.1444 : ℝ)
 356

papers checked against this theorem

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