`e_ne_phi`

proved

show as: view math explainer →

module: IndisputableMonolith.Mathematics.Euler
domain: Mathematics
line: 178 · 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 178.

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

e_gt_phi IndisputableMonolith.Mathematics.Euler

formal source

 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",
 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:

papers checked against this theorem

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