vfeCert_holds
plain-language theorem explainer
The theorem packages the two core properties of variational free energy on a finite partition: the Boltzmann distribution achieves the minimum value, which equals the Helmholtz free energy. Researchers deriving free-energy principles from the Recognition Composition Law or linking statistical mechanics to recognition partitions would cite this result. The proof is a one-line term that directly assembles the two supporting lemmas into the VFECert structure.
Claim. Let $ι$ be a finite nonempty type. For any energy function $E:ι→ℝ$ and inverse temperature $β>0$, the variational free energy of the Boltzmann distribution equals the Helmholtz free energy: $VFE(boltzmannDist(E,β),E,β)=helmholtzF(E,β)$. Moreover, the Boltzmann distribution minimizes the variational free energy: $VFE(boltzmannDist(E,β),E,β)≤VFE(q,E,β)$ for every probability distribution $q$ on $ι$.
background
The module works on a finite recognition partition equipped with an energy function $E$. Variational free energy is defined as $VFE(q,E,β)=∑q_i E_i - (1/β) H[q]$, where $H[q]$ is the Shannon entropy of the distribution $q$. The Boltzmann reference distribution is $boltzmannDist(E,β)_i=exp(-β E_i)/Z$, with $Z$ the partition function. Helmholtz free energy $helmholtzF(E,β)$ is the thermodynamic potential imported from Thermodynamics.HelmholtzReal. The upstream lemmas establish the equality at the Boltzmann point and the minimization property via the non-negativity of KL divergence.
proof idea
The proof is a one-line term wrapper. It supplies the two fields of the VFECert structure by applying the lemmas vfe_at_boltzmann_eq_helmholtzF and boltzmann_minimizes_vfe, each specialized to the required type-class assumptions on $ι$. No additional rewriting or case analysis is performed.
why it matters
This declaration certifies the central variational properties required by the module's stated purpose: VFE on a finite partition with monotone descent under ledger updates. It directly supports the identification of the Friston free-energy functional with the Helmholtz potential inside the Recognition Science framework, closing the link between the Recognition Composition Law and classical statistical mechanics. No downstream uses are recorded yet, leaving open its integration into larger ledger-update or QFT statistics arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.