e_from_normalization

formal source

 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
 161
 162/-- e > 2 (from the strict convexity of exp, or 1+x < exp(x) for x ≠ 0). -/
 163theorem e_gt_two : Real.exp 1 > 2 := by
 164  have h := Real.add_one_lt_exp (show (1:ℝ) ≠ 0 by norm_num)
 165  linarith
 166
 167/-- φ < 2 (from phi < 1.62). -/
 168theorem phi_lt_two : phi < 2 := by
 169  linarith [Constants.phi_lt_onePointSixTwo]
 170
 171/-- e > φ: Euler's number exceeds the golden ratio. -/
 172theorem e_gt_phi : phi < Real.exp 1 := by
 173  have h1 : phi < 2 := phi_lt_two
 174  have h2 : Real.exp 1 > 2 := e_gt_two
 175  linarith