Exactness of the variational bound at the Bayesian posterior

Proved

FreeEnergyPrinciple.variational_free_energy_posterior

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

active-inferencebayesian-inferencefree-energy-principlevariational-inference

Exactness of the variational bound at the Bayesian posterior.

In the setting of the goal theorem (finite generative model, policy $\pi$ , outcome $o$ with $P(o \mid \pi) > 0$ ), take the recognition density to be the exact Bayesian posterior itself, $Q = P(\cdot \mid o, \pi)$ . Then the variational free energy collapses to the outcome surprisal:

F\big[P(\cdot \mid o, \pi),\, o,\, \pi\big] \;=\; -\log P(o \mid \pi).

Role: the attaining witness for the bound. Combined with the goal theorem it shows $-\log P(o \mid \pi)$ is the infimum of $F[\,\cdot\,, o, \pi]$ over all recognition densities, attained at the Bayesian posterior; the companion uniqueness milestone shows the attainment is unique, including posteriors with zero-mass states.

Formalization Note — transcribed from the proved theorem variationalFreeEnergy_posterior 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_posterior
    {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
        (posteriorState model policy outcome h) =
      outcomeSurprisal model policy outcome := by sorry

end FreeEnergyPrinciple

Source

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

Read-back

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

Let $\mathcal{P}$ , $\mathcal{S}$ , and $\mathcal{O}$ be types (of policies, states, and outcomes), each of which is finite. Let model be a value of the bundle's GenerativeModel structure indexed by these three types — a record bundling the distributions of the generative model, including (by the naming used here) at least the quantity predictedOutcome model policy outcome and whatever variationalFreeEnergy and outcomeSurprisal compute from it. Let policy be a policy in $\mathcal{P}$ and outcome an outcome in $\mathcal{O}$ . Suppose the hypothesis

0 < \operatorname{predictedOutcome}(\text{model}, \text{policy}, \text{outcome}),

i.e. the model's predicted probability (or predicted value) of this outcome under this policy is strictly positive. Under these assumptions, the theorem asserts that for every value recognition of the bundle's FiniteLaw State type — a finite law on states, whatever that structure contains — the following equality holds:

\operatorname{variationalFreeEnergy}\bigl(\text{model}, \text{policy}, \text{outcome},\ h,\ \operatorname{posteriorState}(\text{model}, \text{policy}, \text{outcome}, h)\bigr) = \operatorname{outcomeSurprisal}(\text{model}, \text{policy}, \text{outcome}).

In words: the variational free energy of the model, policy, and outcome, evaluated at the posterior state over states that the bundle's function posteriorState produces from the same model, policy, outcome, and positivity hypothesis, equals the outcome surprisal of that model, policy, and outcome.

Remarks on quantifiers and edge cases, taken literally from the statement:

The variable recognition is universally quantified and appears nowhere in the equation being asserted; the claim holds for every finite law on states regardless of its value.
The hypothesis $h$ (strict positivity of the predicted outcome) is a genuine assumption: the statement says nothing about the case where $\operatorname{predictedOutcome}(\text{model}, \text{policy}, \text{outcome}) = 0$ or negative, and both posteriorState and variationalFreeEnergy take $h$ as an argument, so their behavior in that case is outside the claim.
posteriorState is the specific function defined in this bundle, applied to model, policy, outcome, and $h$ ; the theorem does not quantify over arbitrary posteriors — the equality is asserted only for that particular value.
The meanings of predictedOutcome, posteriorState, variationalFreeEnergy, outcomeSurprisal, GenerativeModel, and FiniteLaw are those given by the imported definitions in this bundle; the statement as written does not further constrain them beyond what those definitions say.
The claim is an unconditional equality (no inequality, no existence statement), and it is asserted for all policies and outcomes of the finite types simultaneously.

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