partitionFunction_pos
plain-language theorem explainer
Partition function positivity asserts that for any real-valued energy assignment E over a finite index set and any real β the sum Z = ∑ exp(−β E_i) is strictly positive. Statistical mechanicians and variational inference researchers cite it to guarantee that Boltzmann probabilities are well-defined and sum to one. The proof is a direct term-mode application of Finset.sum_pos after unfolding the definition and using positivity of the exponential together with nonemptiness of the finite index set.
Claim. Let $E : ι → ℝ$ and $β ∈ ℝ$. The partition function $Z(E,β) := ∑_i exp(−β E(i))$ satisfies $Z(E,β) > 0$.
background
In the HelmholtzReal module the partition function is the finite sum of Boltzmann factors exp(−β E_i) over a Fintype index set ι. This supplies the concrete normalization needed for the real Helmholtz free energy F = −log Z / β and for the claim that the Boltzmann distribution minimizes the variational free-energy functional. The module works entirely with finite discrete systems and avoids the placeholder axioms present in the abstract FreeEnergy module.
proof idea
The term proof unfolds partitionFunction to a Finset.sum of exponential terms, then applies Finset.sum_pos. The two required hypotheses are supplied by Real.exp_pos (each summand is positive) and Finset.univ_nonempty (the index set is nonempty).
why it matters
The result is invoked by boltzmannProb_pos, boltzmannProb_sum_one and helmholtzRealCert_holds inside the same module, and by boltzmann_minimizes_vfe in the variational free-energy section. It supplies the elementary positivity step that lets the Gibbs inequality argument go through, thereby grounding the finite-case thermodynamics claims that sit downstream of the Recognition Composition Law and the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.