theorem
proved
e_gt_phi
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Mathematics.Euler on GitHub at line 172.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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",
199 "e: Continuous rates, derivatives, growth",
200 "Both: Fundamental to self-similar processes",
201 "Together: Complete description of growth phenomena"
202]