prob_normalized

formal source

 150  finset_sum_eq_list_sum_aux sys.levels f
 151
 152/-- **THEOREM**: Probabilities sum to 1 (normalization). -/
 153theorem prob_normalized (sys : System) (beta : ℝ) (hb : beta > 0) :
 154    (Finset.univ.sum fun i => probability sys beta i) = 1 := by
 155  unfold probability
 156  simp only [div_eq_mul_inv]
 157  rw [← Finset.sum_mul]
 158  have hz : partitionFunction sys beta ≠ 0 := (partition_positive sys beta hb).ne'
 159  -- Sum of Boltzmann factors = partition function (by definition)
 160  have hsum : Finset.sum Finset.univ (fun i : Fin sys.levels.length =>
 161      boltzmannFactor (sys.levels.get i) beta) = partitionFunction sys beta := by
 162    unfold partitionFunction
 163    exact finset_sum_eq_list_sum sys (fun l => boltzmannFactor l beta)
 164  rw [hsum]
 165  exact mul_inv_cancel₀ hz
 166
 167/-! ## The J-Cost Connection -/
 168
 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