heatCapacity

formal source

  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
 110    -- The weight is exp(-J_cost / k_B T)
 111    True := trivial
 112
 113/-- The ledger structure naturally provides:
 114    1. **Discrete states**: Ledger entries are countable
 115    2. **Energy assignment**: J-cost determines "energy"
 116    3. **Degeneracy**: Multiple entries with same cost
 117    4. **Conservation**: Total ledger balance is conserved -/
 118def ledgerProperties : List String := [
 119  "Discrete microstates from ledger entries",