partition_positive
plain-language theorem explainer
The partition function Z for any nonempty collection of energy levels is strictly positive whenever the inverse temperature β exceeds zero. Recognition Science modelers and statistical mechanicians cite this to guarantee that Boltzmann probabilities are normalizable and free energies are defined. The proof extracts the head term via the nonempty list property, applies boltzmannFactor_pos to obtain a positive summand, shows the tail sum is nonnegative, and closes with linarith.
Claim. Let sys be a system whose energy levels form a nonempty list and let β > 0. Then the partition function Z(sys, β) := ∑_i exp(−β E_i) satisfies Z(sys, β) > 0.
background
The module THERMO-001 derives the Boltzmann distribution from Recognition Science's J-cost functional: states are selected by minimizing total recognition cost J(x) subject to a fixed ledger balance, with β arising as the Lagrange multiplier conjugate to that constraint. A System is the structure whose sole data are a nonempty list of EnergyLevel entries. The partitionFunction is defined as the sum of boltzmannFactor terms; upstream definitions in ActivationEnergy and EnzymeCatalysis give boltzmannFactor(E, β) = exp(−E/β) (with kT scaled to 1).
proof idea
The tactic proof unfolds partitionFunction, invokes sys.nonempty to obtain a nonempty list, performs a cases split to extract head and tail, rewrites the sum as the head boltzmannFactor plus the mapped tail sum, applies boltzmannFactor_pos to the head term, invokes list_sum_nonneg_of_pos on the tail (which itself calls boltzmannFactor_pos on each element), and finishes with linarith.
why it matters
partition_positive is invoked directly by partition_ge_ground (which shows Z ≥ 1 when a zero-energy ground state is present), by prob_nonneg (non-negative probabilities), and by prob_normalized (normalization to unity). It therefore supplies the positivity step required for the central claim P_i = exp(−β E_i)/Z in the paper on statistical mechanics from Recognition Science. The result sits inside the thermodynamics layer that converts J-cost constraints into the standard exponential distribution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.