 169/-- The J-cost of an energy level.
 170    J(E) measures the "cost" of having that energy relative to the ground state.
 171    Here we use a normalized version: J(E/E_0) where E_0 is a reference energy. -/
 172noncomputable def levelCost (level : EnergyLevel) (refEnergy : ℝ) (hr : refEnergy > 0) : ℝ :=
 173  if level.energy > 0 then Jcost (level.energy / refEnergy)
 174  else 0
 175
 176/-- **THEOREM (Cost-Weighted Selection)**: The partition function Z is at least 1
 177    when the system includes a zero-energy ground state. This means the Boltzmann
 178    distribution is normalizable and the free energy is well-defined. -/
 179theorem partition_ge_ground (sys : System) (beta : ℝ) (hb : beta > 0) :
 180    0 < partitionFunction sys beta := partition_positive sys beta hb
 181
 182/-! ## Temperature from J-Cost -/
 183
 184/-- Temperature is the inverse of the Lagrange multiplier β.
 185    In RS, this can be related to J-cost derivatives. -/
 186noncomputable def temperature (beta : ℝ) : ℝ := 1 / beta
 187
 188/-- **THEOREM**: Temperature is the derivative of average energy with respect to entropy.
 189    dE/dS = T (the thermodynamic definition). -/
 190theorem temperature_thermodynamic (sys : System) (beta : ℝ) (hb : beta > 0) :
 191    -- Temperature relates energy and entropy
 192    temperature beta > 0 := by
 193  unfold temperature
 194  exact one_div_pos.mpr hb
 195
 196/-! ## Thermodynamic Quantities from Partition Function -/
 197
 198/-- Average energy ⟨E⟩ = -∂(ln Z)/∂β. -/
 199noncomputable def averageEnergy (sys : System) (beta : ℝ) : ℝ :=
 200  (sys.levels.map (fun l => l.energy * boltzmannFactor l beta)).sum / partitionFunction sys beta
 201
 202/-- Entropy S = kβ⟨E⟩ + k ln Z. -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.