def
definition
phiVsE
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 197.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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)
212
213 **Proved**: The real part of e^(iπ/5) equals φ/2, using
214 the classical identity cos(π/5) = (1 + √5)/4 = φ/2. -/
215theorem euler_phi_connection :
216 -- cos(π/5) = φ/2 (the real part of e^(iπ/5))
217 Real.cos (Real.pi / 5) = phi / 2 := by
218 rw [Real.cos_pi_div_five]
219 -- phi / 2 = (1 + sqrt 5) / 2 / 2 = (1 + sqrt 5) / 4
220 unfold phi
221 ring
222
223/-! ## RS Interpretation -/
224
225/-- RS interpretation of e:
226
227 1. **J-cost decay**: Probabilities involve e^(-J)