averageEnergy
plain-language theorem explainer
The definition computes the mean energy of a system as the Boltzmann-weighted sum of its discrete energy levels, normalized by the partition function. Researchers deriving statistical mechanics from Recognition Science's J-cost functional cite this when evaluating thermodynamic averages from cost-weighted state selection. It implements the standard expression for ⟨E⟩ directly as a weighted sum over the system's levels.
Claim. $⟨E⟩ = (∑_l E_l ⋅ exp(−β E_l)) / Z$, where $Z$ is the partition function over the system's energy levels at inverse temperature β.
background
The module derives the Boltzmann distribution from Recognition Science's J-cost functional, where lower-cost states are selected with higher probability under a fixed total-cost constraint. A System is a non-empty list of EnergyLevel records, each carrying a real energy value. The boltzmannFactor (imported from chemistry and Shannon entropy modules) supplies the factor exp(−E/kT) or its RS-native analogue; the partition function normalizes the resulting probabilities. This places the definition inside the cost-to-thermodynamics bridge described in the module documentation.
proof idea
The definition is a direct one-line implementation of the weighted average: it maps each level to its energy multiplied by the Boltzmann factor at the supplied β, sums the products, and divides by the partition function.
why it matters
It supplies the mean energy required by the entropy definition S = β⟨E⟩ + ln Z and the free-energy identity F = ⟨E⟩ − TS in the same module. The definition closes the link from J-cost constraints to standard thermodynamic relations targeted by the module's derivation of P_i = exp(−β E_i)/Z. It is referenced by the partition-function module's corresponding averageEnergy, entropy, and heat-capacity definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.