vfe_at_boltzmann_eq_helmholtzF
plain-language theorem explainer
Evaluating the variational free energy at the Boltzmann distribution recovers the Helmholtz free energy for positive inverse temperature. Researchers linking variational inference to thermodynamic potentials in the Recognition framework cite this identity. The proof unfolds the definitions of variational free energy and Boltzmann distribution, invokes the energy-entropy relation, and closes with linear arithmetic.
Claim. For finite index set $I$, energy function $E: I → ℝ$, and inverse temperature $β > 0$, let $p$ be the Boltzmann distribution $p_i ∝ exp(−β E_i)$. The variational free energy $F[p; E, β] := ∑_i p_i E_i + (1/β) ∑_i p_i log p_i equals the Helmholtz free energy $F(E, β)$.
background
The module constructs variational free energy on a finite recognition partition and shows its relation to the Recognition Composition Law. Variational free energy is defined as expected energy under trial distribution q plus a scaled negative entropy term. The Boltzmann distribution is the reference distribution p_i = exp(−β E_i)/Z that achieves the canonical minimum form expected energy minus temperature times entropy.
proof idea
Unfolds variational free energy and Boltzmann distribution definitions. Applies the upstream lemma F_eq_E_minus_TS after unfolding expected energy and Boltzmann entropy. Linear arithmetic equates the resulting expressions to the Helmholtz free energy.
why it matters
This identity supplies the first component of the VFECert certificate assembled in vfeCert_holds. It identifies the minimum value of variational free energy with the Helmholtz potential, completing the module's goal of connecting Recognition-derived statistics to thermodynamic identities. The module reports zero sorrys after this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.