heatCapacity
plain-language theorem explainer
Heat capacity for a discrete system is defined via the energy fluctuation formula C_V = k_B β² (⟨E²⟩ - ⟨E⟩²). Researchers building thermodynamic relations from Recognition Science ledger states cite this expression to connect microscopic J-costs to macroscopic response functions. The definition directly assembles the standard variance formula using the system's energy levels, degeneracies, partition function, and average energy.
Claim. For a discrete system with energy levels $E_i$ and degeneracies $g_i$, the heat capacity at temperature $T > 0$ is $C_V = k_B β^2 (⟨E^2⟩ - ⟨E⟩^2)$, where $β = 1/(k_B T)$, the averages are taken with respect to the Boltzmann weights $g_i exp(-β E_i)/Z$, and $Z$ is the partition function.
background
In Recognition Science, the partition function emerges as a sum over ledger configurations weighted by their J-cost. The DiscreteSystem structure encodes a finite collection of energy levels together with their degeneracies. Upstream results supply the canonical J_cost function J(x) = (x + x^{-1})/2 - 1, which induces the Boltzmann factor exp(-J_cost / k_B T) via the cost definitions in ObserverForcing and MultiplicativeRecognizerL4.
proof idea
This is a direct definition that implements the standard fluctuation formula for heat capacity. It evaluates the second moment of energy minus the square of the first moment, scaled by k_B β², using the sibling partitionFunction and averageEnergy. No external lemmas are invoked beyond summation and the beta helper.
why it matters
The definition supplies the RS-native expression for heat capacity within the THERMO-002 ledger-sum derivation of statistical mechanics. It completes the set of basic thermodynamic quantities (free energy, average energy, entropy, heat capacity) that follow from the partition function. The construction remains consistent with the J-uniqueness and phi-ladder scaling of the broader framework, though no downstream applications are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.