boltzmann_minimizes_vfe
plain-language theorem explainer
The Boltzmann distribution minimizes variational free energy over any competing distribution q on a finite index set. Researchers in active inference and free-energy principles would cite this discrete case of the Gibbs inequality. The proof expands the difference into a positive multiple of the KL divergence between q and the Boltzmann distribution and invokes its nonnegativity.
Claim. Let $E : ι → ℝ$ be an energy assignment on a finite set $ι$, let $β > 0$, and let $q$ be any probability distribution on $ι$. Then the variational free energy of the Boltzmann distribution satisfies $F[ Boltzmann(E, β) ; E, β ] ≤ F[ q ; E, β ]$.
background
In this module the variational free energy is defined on a finite probability simplex as the sum of expected energy and a scaled entropy term: $F[q; E, β] = ∑_i q_i E_i + (1/β) ∑_i q_i log q_i$. A ProbDist is a function from $ι$ to positive reals that sums to one. The Boltzmann distribution is the reference measure $p_i = exp(-β E_i)/Z$ that arises as the minimizer. The module derives VFE from the Recognition Composition Law via the J-cost bridge and identifies its minimum value with the Helmholtz free energy. Upstream results supply the partition function positivity and the KL nonnegativity lemma.
proof idea
The proof first algebraically expands the difference VFE[q] minus VFE[Boltzmann] into (1/β) times the sum ∑ q_i log(q_i / p_i), which is exactly the KL divergence. It then applies the already-proved lemma kl_nonneg to obtain nonnegativity of the difference and concludes by linarith.
why it matters
This theorem supplies the minimization property required by the VFECert certificate, which in turn certifies that the variational free energy attains the Helmholtz free energy at the Boltzmann point. Within the Recognition Science framework it closes the link between the RCL-derived information measures and classical thermodynamics, confirming that the eight-tick octave structure yields the expected free-energy descent. No open scaffolding remains in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.