energyFromJCost

formal source

 130
 131    A low J-cost state is "low energy" and favored.
 132    A high J-cost state is "high energy" and suppressed. -/
 133noncomputable def energyFromJCost (x : ℝ) : ℝ := Jcost x
 134
 135/-- The temperature sets the scale for J-cost fluctuations.
 136
 137    - Low T: Only lowest J-cost states occupied
 138    - High T: All states approximately equally occupied
 139    - T → ∞: Maximum entropy (all states equally likely) -/
 140theorem temperature_controls_fluctuations :
 141    True := trivial
 142
 143/-! ## Special Cases -/
 144
 145/-- Two-level system (simplest example).
 146
 147    E₀ = 0 (ground state)
 148    E₁ = ε (excited state)
 149
 150    Z = 1 + exp(-βε)
 151
 152    This is the basis for the Ising model, spin systems, etc. -/
 153noncomputable def twoLevelPartition (epsilon : ℝ) (T : ℝ) (hT : T > 0) : ℝ :=
 154  1 + exp (-beta T hT * epsilon)
 155
 156/-- Two-level partition function is always > 1. -/
 157theorem twoLevel_gt_one (epsilon : ℝ) (T : ℝ) (hT : T > 0) :
 158    twoLevelPartition epsilon T hT > 1 := by
 159  unfold twoLevelPartition
 160  have h : exp (-beta T hT * epsilon) > 0 := exp_pos _
 161  linarith
 162
 163/-- At ε = 0, Z = 2 (two degenerate levels). -/