Gaussian variational free energy is squared mean error plus evidence surprisal

Proved

FreeEnergyPrinciple.gaussianVariationalFreeEnergy_eq_meanSquare_add_surprisal

by ActiveInference · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

free-energy-principlegaussiankalman-filtervariational-inference

The Gaussian instantiation of the variational bound: for an exact scalar Gaussian filter, variational free energy is a squared mean error plus evidence surprisal.

Fix a scalar Gaussian filter model: an OU prediction step (rate $\kappa$ , center, diffusion variance rate, step duration $\tau$ ), a fixed-variance Gaussian observation channel with noise variance $r$ , and a nondegenerate Gaussian prior belief $(m, v)$ . The filter predicts the Gaussian belief $(m_p, v_p)$ with $v_p = e^{-2\kappa\tau} v + \gamma$ , forms the innovation variance $v_p + r$ , and updates in closed form:

m^* = m_p + \frac{v_p}{v_p+r}\,(o - m_p), \qquad v^* = \frac{v_p\,r}{v_p + r}.

Both the evidence and the update denominators are strictly positive, so the recognition family — the fixed-variance Gaussian family at variance $v^*$ — is genuinely nondegenerate.

The posterior-form variational free energy at recognition mean $\mu$ is the native KL from the recognition law $\mathcal{N}(\mu, v^*)$ to the posterior law $\mathcal{N}(m^*, v^*)$ , plus the evidence surprisal $S(o) = -\log\rho(o)$ taken against the evidence family's density at the predicted mean. The target identity:

F[\mu] \;=\; \frac{(\mu - m^*)^2}{2 v^*} \;+\; S(o).

The first summand is the exact closed form of the fixed-variance Gaussian KL — no approximation is involved — and the second is the density-relative surprisal of the datum under the evidence law. Equality of free energy and surprisal holds exactly at $\mu = m^*$ , the Gaussian analogue of FEP-I's posterior-exactness theorem; the native-KL remainder vanishing characterizes the posterior mean in the fixed-variance family.

Preamble

import Mathlib.InformationTheory.KullbackLeibler.Basic
import Definitions.Def_fep2_gaussian_vfe

Formal statement

namespace FreeEnergyPrinciple
open InformationTheory

theorem gaussianVariationalFreeEnergy_eq_meanSquare_add_surprisal
    (model : ScalarGaussianFilterModel) (prior : ScalarGaussianBelief)
    (observation recognitionMean : ℝ) :
    gaussianVariationalFreeEnergy model prior observation recognitionMean =
      (recognitionMean - posteriorMean model prior observation) ^ 2 /
          (2 * (posteriorVariance model prior : ℝ)) +
        evidenceSurprisal model prior observation := by sorry

end FreeEnergyPrinciple

Source

fep_lean / fep_formal v1.2.0 (Active Inference Institute), FepSketches.compositions.smooth_reference_kernel.lean § Maintained continuous Gaussian VFE, theorem gaussianVariationalFreeEnergy_eq_meanSquare_add_surprisal (proved, 0 sorry), substrate FepSketches.gaussian_information_geometry.lean (klDiv_law_eq_meanSquare) + FepSketches.compositions.gaussian_filter.lean; https://github.com/ActiveInferenceInstitute/fep_formal

Read-back

What the Lean code literally says, in plain math · glm-flash-latest

For every scalar Gaussian filter model, every prior belief, and all real $y$ (observation) and $r$ (recognition mean) — no additional hypotheses or typeclass binders; strict positivity is carried inside the structures — the theorem asserts, as an equality in $\mathbb{R}$ :

\mathrm{gaussianVariationalFreeEnergy}(\mathrm{model},\ \mathrm{prior},\ y,\ r) \;=\; \frac{(r - m_{\mathrm{post}})^2}{2\, v_{\mathrm{post}}} \;+\; S

Unfolding the bundle's own definitions:

The left side $F$ is $\bigl[\mathrm{KL}\bigl(\mathcal{N}(r, v_{\mathrm{post}})\,\big\|\,\mathcal{N}(m_{\mathrm{post}}, v_{\mathrm{post}})\bigr)\bigr]$ converted from $\mathbb{R}_{\ge 0}^{\infty}$ to $\mathbb{R}$ by the total embedding that sends $+\infty$ to $0$ , plus $S$ . The KL is oriented recognition-to-posterior, and both Gaussians share the variance $v_{\mathrm{post}}$ .
$m_{\mathrm{post}}$ (posteriorMean) is the closed-form one-step filter update: the Ornstein–Uhlenbeck predicted mean (prior mean pulled toward the dynamics center by the factor $e^{-\mathrm{rate}\, t}$ , step duration $t \ge 0$ ) plus the gain (predicted variance $\div$ innovation variance) times $(y - \text{predicted mean})$ .
$v_{\mathrm{post}}$ (posteriorVariance) is predicted variance $\times$ observation-noise variance $\div$ innovation variance (predicted plus observation-noise variance), provably $> 0$ ; hence $2 v_{\mathrm{post}} > 0$ and no division-by-zero junk arises.
$S$ (evidenceSurprisal) is $-\ln d(y)$ , where $d$ is the Gaussian density with mean the predicted (pre-observation) mean and variance the innovation variance; $d(y) > 0$ , so the logarithm is the ordinary real one.

The quantifiers include degenerate cases such as $t = 0$ and arbitrary $r$ .

The proof is sorry: the statement is admitted, not proved.

AUDITOR-FLAG: proof is an admitted placeholder (sorry) — the theorem is stated but nothing is established. AUDITOR-FLAG: no finiteness hypothesis is imposed on the KL; it enters through the total $\infty \mapsto 0$ embedding (finiteness holds here only because the two measures share the variance $v_{\mathrm{post}} > 0$ ).

Human review

Endorsed by Shuze Chen · Sep 25, 2026
Confirmed by the moderator at approval.
Endorsed by ActiveInference · Sep 25, 2026
Confirmed by the mission captain (proposal self-audit).

View graph