averageEnergy
plain-language theorem explainer
The definition computes the average energy of a discrete system as the expectation value under the Boltzmann distribution derived from the ledger-sum partition function. Thermodynamicists and statistical mechanicians cite it when extracting thermodynamic potentials from Z in Recognition Science. It is realized as the direct weighted sum of energies times degeneracies times Boltzmann factors, divided by the partition function.
Claim. For a discrete system with energy levels $E_i$ and degeneracies $g_i$ at temperature $T > 0$, the average energy is given by $⟨E⟩ = (∑_i E_i g_i exp(−β E_i)) / Z$, where $β = 1/(k_B T)$ and $Z = ∑_i g_i exp(−β E_i)$ is the partition function.
background
DiscreteSystem is a structure recording the number of energy levels, the energy of each level, and its degeneracy (at least 1), with the requirement that there is at least one level. The module derives the partition function Z as a sum over ledger configurations weighted by J-cost, yielding the standard relations F = −k_B T ln Z, ⟨E⟩ = −∂ln Z/∂β, and S = k_B (ln Z + β⟨E⟩). Upstream, k_B is taken from ComputationLimitsStructure as the Landauer constant satisfying the minimum energy cost to erase one bit, while beta is the inverse-temperature map used throughout the thermodynamics siblings.
proof idea
The definition is a direct arithmetic expression: the sum over Fin sys.numLevels of energy times degeneracy times exp(−beta T hT times energy), divided by the partitionFunction call.
why it matters
This definition supplies the average energy used by the entropy and heatCapacity definitions in the same module and by the corresponding averageEnergy, entropy, and free_energy_identity declarations in BoltzmannDistribution. It realizes the standard thermodynamic relation ⟨E⟩ = −∂ln Z/∂β inside the Recognition Science ledger-sum construction of Z, closing the link from partition function to thermodynamic potentials.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.