`e_gt_one`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Mathematics.Euler on GitHub at line 181.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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",
 199  "e: Continuous rates, derivatives, growth",
 200  "Both: Fundamental to self-similar processes",
 201  "Together: Complete description of growth phenomena"
 202]
 203
 204/-- Euler's identity connects e, i, π, and 1:
 205
 206    e^(iπ) + 1 = 0
 207
 208    φ appears when we consider:
 209    cos(π/5) = φ/2
 210
 211    So: e^(iπ/5) = cos(π/5) + i sin(π/5) = φ/2 + i sin(π/5)

papers checked against this theorem

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