def
definition
attempt5
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
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 :