averageEnergy

formal source

  76  -k_B * T * log (partitionFunction sys T hT)
  77
  78/-- Average energy ⟨E⟩ = -∂ln Z/∂β = Σᵢ Eᵢ Pᵢ. -/
  79noncomputable def averageEnergy (sys : DiscreteSystem) (T : ℝ) (hT : T > 0) : ℝ :=
  80  (∑ i : Fin sys.numLevels,
  81    sys.energy i * (sys.degeneracy i : ℝ) * exp (-beta T hT * sys.energy i)) /
  82  partitionFunction sys T hT
  83
  84/-- Entropy S = k_B(ln Z + β⟨E⟩). -/
  85noncomputable def entropy (sys : DiscreteSystem) (T : ℝ) (hT : T > 0) : ℝ :=
  86  k_B * (log (partitionFunction sys T hT) + beta T hT * averageEnergy sys T hT)
  87
  88/-- Heat capacity C_V = ∂⟨E⟩/∂T. -/
  89noncomputable def heatCapacity (sys : DiscreteSystem) (T : ℝ) (hT : T > 0) : ℝ :=
  90  -- This would require calculus; placeholder
  91  k_B * (beta T hT)^2 *
  92    ((∑ i : Fin sys.numLevels,
  93      (sys.energy i)^2 * (sys.degeneracy i : ℝ) * exp (-beta T hT * sys.energy i)) /
  94    partitionFunction sys T hT - (averageEnergy sys T hT)^2)
  95
  96/-! ## RS Derivation: Ledger Sum -/
  97
  98/-- In Recognition Science, the partition function is a **sum over ledger states**.
  99
 100    Each microscopic configuration corresponds to a ledger entry.
 101    The Boltzmann weight exp(-βE) comes from the J-cost:
 102
 103    P(state) ∝ exp(-J_cost(state) / k_B T)
 104
 105    The partition function normalizes these probabilities:
 106    Z = Σ_{ledger states} exp(-J_cost / k_B T) -/
 107theorem partition_from_ledger_sum :
 108    -- Z = sum over all ledger configurations
 109    -- Each configuration has a J-cost