def
definition
attempt5
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 115.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
112 2φ - 1 ≈ 2.236
113 φ^2.236 ≈ 2.963
114 Divided by φ: 1.83 (too small) -/
115noncomputable def attempt5 : ℝ := phi^(phi + 1/phi) / phi
116
117/-! ## Continued Fraction Connection -/
118
119/-- e has a beautiful continued fraction:
120
121 e = 2 + 1/(1 + 1/(2 + 1/(1 + 1/(1 + 1/(4 + 1/(1 + 1/(1 + ...)))))))
122
123 Pattern: [2; 1, 2, 1, 1, 4, 1, 1, 6, 1, 1, 8, ...]
124
125 φ has: [1; 1, 1, 1, 1, ...] (all 1s)
126
127 Both are "simple" continued fractions in some sense. -/
128def eContinuedFraction : List ℕ := [2, 1, 2, 1, 1, 4, 1, 1, 6, 1, 1, 8]
129
130def phiContinuedFraction : List ℕ := [1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
131
132/-! ## The J-Cost Connection -/
133
134/-- In RS, e appears in probability distributions:
135
136 Boltzmann: P ∝ exp(-E/kT)
137 J-cost: P ∝ exp(-J/J₀)
138
139 The exponential (base e) is fundamental for probability normalization.
140
141 Why e specifically? Because:
142 d/dx e^x = e^x
143
144 Only exponential maintains shape under differentiation. -/
145theorem e_from_normalization :