partitionFunction
plain-language theorem explainer
The partition function Z for a discrete energy spectrum E is the sum of exp(−β E_i) over states. Researchers deriving average energy, entropy, and the Boltzmann distribution's minimization of variational free energy cite this definition. It is introduced as a direct summation of exponential Boltzmann factors with no further lemmas.
Claim. $Z(beta) := sum_i exp(-beta E_i)$ for an energy assignment $E$ on a discrete index set and inverse temperature $beta$.
background
The HelmholtzReal module supplies explicit real-valued constructions for thermodynamic quantities on finite discrete systems, replacing trivial placeholders from the FreeEnergy module. The partition function is the central object from which free energy $F = -log Z / beta$, entropy, and average energy are derived. Upstream results define similar partition functions: the BoltzmannDistribution version sums Boltzmann factors, the PartitionFunction version includes degeneracy weights, and the JCostThermoBridge version uses J-cost Boltzmann factors for ratio systems.
proof idea
The declaration is a one-line definition that directly applies the summation operator to the terms exp(−beta E_i) for each index i. No lemmas or tactics are required beyond the standard real exponential and sum.
why it matters
This definition underpins the BoltzmannDistribution module, feeding the definitions of averageEnergy, entropy, and freeEnergy as well as the theorem that the Boltzmann distribution minimizes variational free energy via the Gibbs inequality. It realizes the partition function in the Recognition Science thermodynamics, enabling the connection between the recognition composition law and statistical mechanics via the J-cost bridge. It addresses the scaffolding for real proofs of the second law and Legendre transform structure on finite systems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.