VFECert
plain-language theorem explainer
VFECert packages the equality of variational free energy at the Boltzmann distribution with the Helmholtz free energy together with the minimization property of that distribution. Workers on free-energy accounts of inference would invoke this structure to apply the Gibbs inequality inside a Recognition Science derivation. It is assembled as a record from the two component theorems that establish the equality and the inequality separately.
Claim. Let $VFE(q; E, β) = ∑_i q_i E_i + (1/β) ∑_i q_i log q_i$ denote the variational free energy of a probability distribution $q$ on a finite index set with energy function $E$ and inverse temperature $β > 0$. Let $p$ denote the Boltzmann distribution with $p_i ∝ exp(-β E_i)$. Then $VFE(p; E, β)$ equals the Helmholtz free energy $-(1/β) log Z$ where $Z = ∑_i exp(-β E_i)$, and $VFE(p; E, β) ≤ VFE(q; E, β)$ holds for every probability distribution $q$.
background
The module defines variational free energy on finite partitions arising from recognition processes. VFE(q, E, β) is the expected energy under q plus (1/β) times the entropy of q. A ProbDist is a positive function on a finite type that sums to one. The Boltzmann distribution boltzmannDist(E, β) is the normalized exponential of -β E. Helmholtz free energy helmholtzF(E, β) is -log(partitionFunction(E, β))/β. The local setting is the derivation of Friston's VFE from the Recognition Composition Law on discrete recognition partitions, with status zero sorry.
proof idea
VFECert is a structure definition that records two properties. The first field is instantiated by the theorem establishing equality to helmholtzF at the Boltzmann point. The second field is instantiated by the theorem boltzmann_minimizes_vfe, which expands the difference VFE(q) - VFE(p) into (1/β) times the KL divergence and invokes non-negativity of KL.
why it matters
VFECert supplies the certificate that the variational free energy is minimized by the Boltzmann distribution and attains the Helmholtz value there. It is consumed by vfeCert_holds to produce an instance of the certificate. Within the Recognition Science framework this step identifies the minimum of the free-energy functional with the thermodynamic potential, closing the link from the Recognition Composition Law through information measures to equilibrium thermodynamics on finite sets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.