Posterior-form variational free energy upper-bounds outcome surprisal

Proved

FreeEnergyPrinciple.variational_free_energy_ge_surprisal

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

active-inferenceelbofree-energy-principlevariational-inference

The variational free-energy bound of the free energy principle, in posterior form, over a finite generative model.

Fix a finite generative model over finite types $\mathsf{Policy}, \mathsf{State}, \mathsf{Outcome}$ (initial state law, policy-conditioned transitions, state-to-outcome likelihood, preferences, policy prior — definitions Def_fep_finite_laws, Def_fep_finite_information, Def_fep_generative_model). For a policy $\pi$ and an outcome $o$ with positive predicted mass $P(o \mid \pi) > 0$ , let $P(\cdot \mid o, \pi)$ be the exact Bayesian posterior state law and let the outcome surprisal be $-\log P(o \mid \pi)$ . For any recognition density $Q$ — a normalized finite law over states — the posterior-form variational free energy is

F[Q, o, \pi] \;=\; D_{\mathrm{KL}}\big(Q \,\|\, P(\cdot \mid o, \pi)\big) \;-\; \log P(o \mid \pi).

The theorem asserts, for every recognition density $Q$ :

-\log P(o \mid \pi) \;\le\; F[Q, o, \pi].

Whatever internal state estimate the system carries, the variational free energy of the data is never below the data's surprisal; the excess is exactly the KL divergence from the recognition density to the Bayesian posterior. This is the goal theorem of the mission — the finite, model-relative form of the free energy principle's core inequality (surprisal bound in the sense of Friston 2010; posterior-form identity in the sense of Parr–Pezzulo–Friston 2022).

Formalization Note — the positivity hypothesis $h : 0 < P(o \mid \pi)$ is explicit because the Bayesian posterior is defined only there; KL is the totalized real-valued finite KL of Def_fep_finite_information, nonnegative with no support assumptions; zero-mass atoms are handled by the exact $0 \cdot \log 0 = 0$ convention. Transcribed from the proved theorem outcomeSurprisal_le_variationalFreeEnergy 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_ge_surprisal
    {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) :
    outcomeSurprisal model policy outcome ≤
      variationalFreeEnergy model policy outcome h recognition := by sorry

end FreeEnergyPrinciple

Source

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

Read-back

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

Read-back of variational_free_energy_ge_surprisal.

Let $\mathcal{P}$ , $\mathcal{S}$ , and $\mathcal{O}$ be finite types of policies, states, and outcomes, respectively. Fix a generative model $m$ (a structure in the bundle FreeEnergyPrinciple bundling the model's distributions over these types), a policy $\pi \in \mathcal{P}$ , and an outcome $o \in \mathcal{O}$ .

The theorem assumes that the model's predicted probability of outcome $o$ under policy $\pi$ , denoted $p(o \mid \pi)$ in the bundle's notation (predictedOutcome m π o), is strictly positive: $p(o \mid \pi) > 0$ . It further takes an arbitrary element $\rho$ of the type FiniteLaw State, i.e. an arbitrary probability law on the finite state space $\mathcal{S}$ (the "recognition density"); no condition is imposed on $\rho$ .

Under these assumptions, the theorem asserts the inequality

-\log p(o \mid \pi) \;\le\; F_m(\pi, o, \rho),

where the left-hand side is the outcome surprisal outcomeSurprisal m π o, defined in the bundle as the negative logarithm of the predicted probability $p(o \mid \pi)$ , and the right-hand side is the variational free energy variationalFreeEnergy m π o h ρ, a quantity defined in the bundle that depends on the model $m$ , the policy $\pi$ , the outcome $o$ , the positivity hypothesis $p(o \mid \pi) > 0$ (which is needed for the surprisal to be defined), and the chosen recognition law $\rho$ .

In plain terms: for every policy $\pi$ , every outcome $o$ whose predicted probability is strictly positive, and every probability law $\rho$ on states, the surprisal of $o$ is at most the variational free energy evaluated at $\rho$ .

Points worth noting for the audit:

The inequality holds for every recognition law $\rho$ simultaneously (it is universally quantified as an explicit argument), not merely for the one minimizing free energy.
Outcomes $o$ with $p(o \mid \pi) = 0$ are excluded by the strict-positivity hypothesis $h$ ; the statement says nothing about them.
All three types are assumed finite (Fintype), which is part of the hypothesis structure of the statement.
The definitions of outcomeSurprisal, variationalFreeEnergy, predictedOutcome, and FiniteLaw are taken from this bundle and their exact formulas were not supplied here; the expansion above renders only their roles as referenced in the statement, and the auditor should compare the bundle's actual definitions of these quantities against the intended claim.

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