def
definition
phi_to_e
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 79.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
76noncomputable def e_minus_phi : ℝ := exp 1 - phi
77noncomputable def e_times_phi : ℝ := exp 1 * phi
78noncomputable def e_to_phi : ℝ := (exp 1) ^ phi
79noncomputable def phi_to_e : ℝ := phi ^ (exp 1)
80
81/-! ## Possible φ-Formulas for e -/
82
83/-- Attempt 1: e ≈ φ + φ⁻¹ + 1/2
84
85 φ + 1/φ = φ + φ - 1 = 2φ - 1 ≈ 2.236
86 Plus 1/2 = 2.736 (not quite e ≈ 2.718) -/
87noncomputable def attempt1 : ℝ := phi + 1/phi + 1/2
88
89/-- Attempt 2: e ≈ φ² + (1 - 1/φ)
90
91 φ² = φ + 1 ≈ 2.618
92 1 - 1/φ = 1 - 0.618 = 0.382
93 Sum: 3.000 (too big) -/
94noncomputable def attempt2 : ℝ := phi^2 + (1 - 1/phi)
95
96/-- Attempt 3: e ≈ 2 + 1/φ²
97
98 1/φ² = φ - 1 = 0.618
99 Wait: 1/φ² = (φ-1)² = 0.382
100 2 + 0.382 = 2.382 (too small) -/
101noncomputable def attempt3 : ℝ := 2 + 1/phi^2
102
103/-- Attempt 4: e ≈ (φ + 1)^(2/φ)
104
105 φ + 1 = φ² ≈ 2.618
106 2/φ ≈ 1.236
107 2.618^1.236 ≈ 3.34 (too big) -/
108noncomputable def attempt4 : ℝ := (phi + 1)^(2/phi)
109