VFE
plain-language theorem explainer
The variational free energy on a finite probability distribution q over states with energies E at inverse temperature β equals the expected energy plus (1/β) times the sum of q log q. Workers in variational inference and statistical mechanics cite this definition when establishing that the Boltzmann distribution achieves its minimum value. The definition is a direct transcription of the standard expression expected energy minus temperature times entropy.
Claim. $F[q; E, β] := ∑_i q(i) E(i) + (1/β) ∑_i q(i) log q(i)$, where q is a probability distribution on a finite set ι (a positive function summing to 1).
background
This module implements variational free energy on finite recognition partitions to connect information measures with thermodynamics. The module documentation states that the Friston VFE takes the form F[q ; p] = E_q[E] + KL[q || p_prior], which reduces for a Boltzmann reference p_i = exp(-β E_i)/Z to sum q_i E_i - (1/β) H[q]. A ProbDist ι is a structure with a function prob : ι → ℝ such that prob i > 0 for every i and the sum of prob i over ι equals 1.
proof idea
This is a direct definition with no proof steps. The body transcribes the canonical expression for variational free energy as the sum of expected energy and the (1/β)-scaled sum of q log q terms.
why it matters
This definition anchors the module results. It is referenced by boltzmann_minimizes_vfe to prove the Boltzmann distribution minimizes VFE via the Gibbs inequality, and by vfe_at_boltzmann_eq_helmholtzF to equate the minimum value with the Helmholtz free energy. In the Recognition Science setting it supplies the information-theoretic starting point for thermodynamic potentials, consistent with the module goal of monotone descent under ledger updates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.