`phi_lt_two`

proved

show as: view math explainer →

module: IndisputableMonolith.Mathematics.Euler
domain: Mathematics
line: 168 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Mathematics.Euler on GitHub at line 168.

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

 165  linarith
 166
 167/-- φ < 2 (from phi < 1.62). -/
 168theorem phi_lt_two : phi < 2 := by
 169  linarith [Constants.phi_lt_onePointSixTwo]
 170
 171/-- e > φ: Euler's number exceeds the golden ratio. -/
 172theorem e_gt_phi : phi < Real.exp 1 := by
 173  have h1 : phi < 2 := phi_lt_two
 174  have h2 : Real.exp 1 > 2 := e_gt_two
 175  linarith
 176
 177/-- e ≠ φ: e and φ are distinct constants. -/
 178theorem e_ne_phi : Real.exp 1 ≠ phi := ne_of_gt e_gt_phi
 179
 180/-- e > 1: e exceeds 1. -/
 181theorem e_gt_one : Real.exp 1 > 1 := by
 182  linarith [e_gt_two]
 183
 184/-! ## φ and e: A Deeper Connection? -/
 185
 186/-- Is there a deep connection between φ and e?
 187
 188    Both are transcendental.
 189    Both appear in growth processes.
 190
 191    φ: Discrete (Fibonacci recursion)
 192    e: Continuous (differential equations)
 193
 194    They represent two sides of growth:
 195    - φ: Optimal discrete packing/ratios
 196    - e: Optimal continuous rates -/
 197def phiVsE : List String := [
 198  "φ: Discrete recursion, packing, ratios",

papers checked against this theorem

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