def
definition
def or abbrev
phiVsE
show as:
view Lean formalization →
formal statement (Lean)
197def phiVsE : List String := [
proof body
Definition body.
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)
212
213 **Proved**: The real part of e^(iπ/5) equals φ/2, using
214 the classical identity cos(π/5) = (1 + √5)/4 = φ/2. -/