partitionFunction_pos
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish positivity when the index set ι is infinite.
- Does not treat continuous energy spectra or path integrals.
- Does not constrain the sign of β.
- Does not invoke the Recognition Composition Law or phi-ladder constants.
Lean usage
boltzmannProb_pos E β i := div_pos (Real.exp_pos _) (partitionFunction_pos E β)formal statement (Lean)
42theorem partitionFunction_pos (E : ι → ℝ) (β : ℝ) :
43 0 < partitionFunction E β := by
proof body
Term-mode proof.
44 unfold partitionFunction
45 apply Finset.sum_pos
46 · intro i _
47 exact Real.exp_pos _
48 · exact Finset.univ_nonempty
49
50/-- Boltzmann probability for level `i`. -/