def
definition
e_minus_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 76.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
73 e^φ ≈ 5.043
74 φ^e ≈ 3.069 -/
75noncomputable def e_over_phi : ℝ := exp 1 / phi
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