pith. machine review for the scientific record. sign in
def definition def or abbrev

heatCapacity

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  89noncomputable def heatCapacity (sys : DiscreteSystem) (T : ℝ) (hT : T > 0) : ℝ :=

proof body

Definition body.

  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) -/

depends on (26)

Lean names referenced from this declaration's body.