phiContinuedFraction

formal source

 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 :
 146    -- e is the unique base for self-similar exponentials
 147    True := trivial
 148
 149/-- The partition function:
 150    Z = Σ exp(-E_i/kT)
 151
 152    This normalization factor involves e inherently.
 153    In RS: Z is the sum over ledger configurations. -/
 154def partitionFunctionFormula : String :=
 155  "Z = Σ exp(-J_i/J₀) = normalization for probabilities"
 156
 157/-! ## Provable Bounds on e and φ -/
 158
 159/-- e = exp(1) is positive. -/
 160theorem e_pos : Real.exp 1 > 0 := Real.exp_pos 1