boltzmannProb_sum_one
plain-language theorem explainer
The normalization of Boltzmann probabilities states that the sum over states of exp(-β E_i) divided by the partition function Z equals one for any finite collection of real energies E and inverse temperature β. Researchers deriving variational bounds or discrete Helmholtz potentials cite this to confirm the reference distribution lies on the probability simplex. The proof is a term-mode reduction that unfolds the definitions and applies div_self to the positive partition function.
Claim. Let $Z = ∑_i exp(-β E_i)$. Then $∑_i [exp(-β E_i) / Z] = 1$.
background
In the Recognition Science treatment of thermodynamics the partition function is defined as Z(β) = ∑_i exp(-β E_i) over a finite index set ι. The Boltzmann probability for each state is then the normalized factor exp(-β E_i)/Z. The module supplies real proofs of the associated free-energy identities on this discrete setting, replacing the earlier placeholder statements in FreeEnergy with concrete theorems that rely on the Gibbs inequality for minimization.
proof idea
The proof is a term-mode reduction. It unfolds boltzmannProb and partitionFunction to expose the sum of Boltzmann factors divided by Z, rewrites the sum as a single division via Finset.sum_div, and applies div_self using the positivity of Z supplied by partitionFunction_pos.
why it matters
This result supplies the prob_sum field when the Boltzmann reference distribution is constructed in VariationalFreeEnergyFromRCL.boltzmannDist. It is collected into the certificate HelmholtzRealCert_holds that assembles the real theorems for the Helmholtz free energy. Within the framework it closes the normalization step required before the Gibbs inequality can be invoked to prove that the Boltzmann distribution minimizes the variational free-energy functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.