boltzmannProb_pos
plain-language theorem explainer
The theorem shows that the Boltzmann probability for any index i is strictly positive. It is invoked when constructing the Boltzmann reference distribution inside the variational free energy module. The proof is a one-line wrapper that invokes div_pos on the positivity of the exponential and the positivity of the partition function.
Claim. For any map $E : I → ℝ$, inverse temperature $β ∈ ℝ$, and index $i ∈ I$, the normalized probability $p_i = exp(-β E_i) / Z$ satisfies $p_i > 0$, where $Z = ∑_j exp(-β E_j)$ denotes the partition function.
background
The HelmholtzReal module supplies concrete real-number proofs for the finite discrete case of the Helmholtz free energy. The partition function is the sum of exp(-β E_j) over the finite index set. The Boltzmann probability is defined as the normalized exponential exp(-β E_i) divided by that sum. The module document states that the free energy is convex in β and that the Boltzmann distribution minimizes the functional sum p_i E_i - T H[p] over the simplex. Upstream, partitionFunction_pos establishes positivity of the sum by applying Finset.sum_pos to each Real.exp_pos term.
proof idea
The proof is a one-line wrapper that applies div_pos to Real.exp_pos _ and partitionFunction_pos E β.
why it matters
The result is required by boltzmannDist to supply the prob_pos field of the ProbDist structure. It is used again in boltzmann_minimizes_vfe to establish that the Boltzmann distribution minimizes the variational free energy via the Gibbs inequality. It supplies the concrete positivity step that lets the thermodynamics module replace the placeholder axioms of FreeEnergy with proved statements, thereby connecting the partition function to the Recognition Composition Law through the variational principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.