partitionFunction
plain-language theorem explainer
The partition function sums Boltzmann factors exp(-β E_i) over energy levels in a system at inverse temperature beta. Researchers deriving statistical mechanics from Recognition Science's J-cost would cite it as the normalizing constant for the resulting distribution. It is realized as a direct list sum after mapping each level through the factor definition.
Claim. $Z = ∑_l exp(-β E_l)$ where the sum runs over energy levels $l$ of the system and β is the inverse temperature.
background
The module THERMO-001 derives the Boltzmann distribution from Recognition Science's J-cost functional, where states are selected by cost-weighted probability under a fixed total cost constraint. A System is a structure holding a non-empty list of EnergyLevel entries, each carrying an energy value. The partition function is the sum of Boltzmann factors, with the factor for level l at inverse temperature β given by exp(-β E_l) as supplied by upstream definitions such as boltzmannFactor in ActivationEnergy ('Boltzmann factor: exp(-Ea / kT)').
proof idea
One-line wrapper that maps each energy level to its Boltzmann factor at the supplied beta then sums the resulting list.
why it matters
This definition is the base for averageEnergy, entropy, freeEnergy, partition_positive, and entropy_nonneg_of_Z_ge_one in the same module. It is invoked by boltzmann_minimizes_vfe in VariationalFreeEnergyFromRCL to establish that the Boltzmann distribution minimizes variational free energy via the Gibbs inequality. Within the framework it supplies the partition function step in the derivation of statistical mechanics from J-cost, consistent with the module's core insight that β emerges as the Lagrange multiplier for the cost constraint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.