Uniqueness of the recognition density attaining the bound

Proved

FreeEnergyPrinciple.variational_free_energy_eq_surprisal_iff

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

active-inferencefree-energy-principlekl-divergencevariational-inference

Uniqueness of the recognition density attaining the variational bound.

In the setting of the goal theorem, equality in the bound characterizes exact Bayesian recognition:

F[Q, o, \pi] = -\log P(o \mid \pi) \quad\Longleftrightarrow\quad Q = P(\cdot \mid o, \pi).

Role: the equality case of the free energy principle's core inequality. A recognition density minimizes the variational free energy exactly when it is the exact Bayesian posterior implied by the model — the formal statement of "perception as Bayesian inference" behind the variational free energy. No full-support assumption is needed: at zero-mass reference atoms, normalization forces the recognition law's mass to zero as well, so the characterization covers degenerate posteriors exactly as the source proves it.

Formalization Note — the proof rests on the separation lemma $D_{\mathrm{KL}}(p \,\|\, q) = 0 \leftrightarrow p = q$ of Def_fep_finite_information, which is the technically nontrivial ingredient at zero-mass atoms. Transcribed from the proved theorem variationalFreeEnergy_eq_surprisal_iff of FepSketches.active_inference in the fep_lean formalization; compiled against the platform environment.

Preamble

import Definitions.Def_fep_finite_laws
import Definitions.Def_fep_finite_information
import Definitions.Def_fep_generative_model

Formal statement

namespace FreeEnergyPrinciple

theorem variational_free_energy_eq_surprisal_iff
    {Policy State Outcome : Type*} [Fintype Policy] [Fintype State]
    [Fintype Outcome]
    (model : GenerativeModel Policy State Outcome) (policy : Policy)
    (outcome : Outcome) (h : 0 < predictedOutcome model policy outcome)
    (recognition : FiniteLaw State) :
    variationalFreeEnergy model policy outcome h recognition =
        outcomeSurprisal model policy outcome ↔
      recognition = posteriorState model policy outcome h := by sorry

end FreeEnergyPrinciple

Source

fep_lean (fep_formal v1.2.0), FepSketches.active_inference.lean, theorem variationalFreeEnergy_eq_surprisal_iff; https://github.com/ActiveInferenceInstitute/fep_formal

Read-back

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

Theorem variational_free_energy_eq_surprisal_iff (read-back).

Let $P$ , $S$ , $O$ be types, each of which is finite (i.e., admits a finite enumeration of its elements). Let model be a generative model over policies in $P$ , states in $S$ , and outcomes in $O$ . Fix a policy $\pi \in P$ and an outcome $o \in O$ , and suppose the hypothesis

h:\; \text{predictedOutcome}(\text{model}, \pi, o) > 0,

that is, the model's predicted probability (or density) of the outcome $o$ under policy $\pi$ is strictly positive. Let recognition be a finite law on states $S$ , i.e., a probability distribution over the finite set of states.

The theorem asserts that the following two statements are equivalent (an if-and-only-if):

The variational free energy of the recognition distribution, evaluated for the model, the policy $\pi$ , the outcome $o$ , and the hypothesis $h$ , equals the outcome surprisal of the model — namely the negative logarithm (or the model-defined surprisal measure) of the predicted probability of $o$ under $\pi$ :

\text{variationalFreeEnergy}(\text{model}, \pi, o, h, \text{recognition}) \;=\; \text{outcomeSurprisal}(\text{model}, \pi, o);

The recognition distribution is exactly the posterior distribution over states of the model given the outcome and the policy:

\text{recognition} \;=\; \text{posteriorState}(\text{model}, \pi, o, h).

In other words, the free-energy functional coincides with the outcome surprisal precisely at the recognition distribution that is the model's posterior over states; at every other recognition distribution the equality fails (and by the iff, equality can hold only at the posterior).

Notes on scope: no side conditions are imposed on the types beyond finiteness; the positivity hypothesis $h$ appears both as an assumption and as an argument to the free-energy and posterior constructions, so the statement applies only when the predicted probability of the outcome is strictly positive (avoiding degenerate/singular cases).

Human review

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

View graph