VFECert
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not treat continuous distributions or infinite state spaces.
- Does not derive the Boltzmann form from the Recognition Composition Law directly.
- Does not address dynamical or non-stationary recognition processes.
- Does not incorporate the phi-ladder or spatial dimension constraints from the forcing chain.
formal statement (Lean)
210structure VFECert where
211 vfe_at_boltz : ∀ {ι : Type*} [Fintype ι] [Nonempty ι] (E : ι → ℝ) (β : ℝ),
212 0 < β → VFE (boltzmannDist E β) E β = helmholtzF E β
213 boltz_minimizes : ∀ {ι : Type*} [Fintype ι] [Nonempty ι] (E : ι → ℝ) (β : ℝ),
214 0 < β → ∀ q : ProbDist ι, VFE (boltzmannDist E β) E β ≤ VFE q E β
215