partitionFunctionFormula

formal source

 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
 176
 177/-- e ≠ φ: e and φ are distinct constants. -/
 178theorem e_ne_phi : Real.exp 1 ≠ phi := ne_of_gt e_gt_phi
 179
 180/-- e > 1: e exceeds 1. -/
 181theorem e_gt_one : Real.exp 1 > 1 := by
 182  linarith [e_gt_two]
 183
 184/-! ## φ and e: A Deeper Connection? -/