Finite generative model and posterior-form variational free energy

Definition

fep_generative_model

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

active-inferencefree-energy-principlegenerative-modelvariational-inference

The mission's model layer: a finite generative model for active inference, the laws it predicts, and the posterior-form variational free energy.

Over finite types $\mathsf{Policy}, \mathsf{State}, \mathsf{Outcome}$ , a generative model consists of five fields:

an initial state law $P(s)$ over $\mathsf{State}$ ;
a policy-conditioned transition kernel $P(s' \mid s, \pi)$ ;
a state-to-outcome likelihood kernel $P(o \mid s)$ ;
a preference law $P_{\mathrm{pref}}(o)$ over outcomes;
a policy prior $P(\pi)$ .

Under a policy $\pi$ the model predicts the state law $P(s \mid \pi)$ (marginalizing the initial law through the transition) and the outcome law $P(o \mid \pi)$ . At an outcome $o$ with positive predicted mass $P(o \mid \pi) > 0$ , the exact Bayesian posterior state law is the finite Bayes rule $P(\cdot \mid o, \pi) = P(s) \mapsto P(s)\,P(o \mid s)\,/\,P(o \mid \pi)$ . The outcome surprisal is $-\log P(o \mid \pi)$ (a total function; positivity enters the theorems as an explicit hypothesis, not inside the definition). A recognition density $Q$ is any finite law over states, and the posterior-form variational free energy of $Q$ at $(o, \pi)$ is

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

Formalization Note — transcribed verbatim from the proved module FepSketches.active_inference of the fep_lean formalization (fields, prediction, posterior, surprisal, and the free-energy functional; rollout/planning and expected-free-energy constructs of that module are out of this mission's scope and are planned for a follow-up mission); the file compiles sorry-free.

Definition code

import Definitions.Def_fep_finite_information

/-!
# Finite generative model and posterior-form variational free energy

Transcribed from the proved module `FepSketches.active_inference` of the
fep_lean formalization (Active Inference Institute).  One policy-conditioned
carrier owns prediction, observation, posterior state, preferences, and the
posterior-form variational free energy.  The epistemic sign is fixed by
definition; the theorems of this mission derive the surprisal bound, its
exactness at the Bayesian posterior, its uniqueness characterization, and the
evidence lower bound.
-/

namespace FreeEnergyPrinciple

open Finset
open scoped BigOperators

variable {Policy State Outcome : Type*}
  [Fintype Policy] [Fintype State] [Fintype Outcome]

/-- Finite policy-conditioned generative model for active inference. -/
structure GenerativeModel (Policy State Outcome : Type*)
    [Fintype Policy] [Fintype State] [Fintype Outcome] where
  initialState : FiniteLaw State
  transition : Policy → FiniteKernel State State
  likelihood : FiniteKernel State Outcome
  preferences : FiniteLaw Outcome
  policyPrior : FiniteLaw Policy

/-- State prediction under a candidate policy. -/
def predictedState (model : GenerativeModel Policy State Outcome)
    (policy : Policy) : FiniteLaw State :=
  (model.transition policy).predictive model.initialState

/-- Predicted outcome marginal under a policy. -/
def predictedOutcome (model : GenerativeModel Policy State Outcome)
    (policy : Policy) : FiniteLaw Outcome :=
  model.likelihood.predictive (predictedState model policy)

/-- Exact posterior state law after a positive-mass outcome. -/
noncomputable def posteriorState
    (model : GenerativeModel Policy State Outcome) (policy : Policy)
    (outcome : Outcome) (h : 0 < predictedOutcome model policy outcome) :
    FiniteLaw State :=
  model.likelihood.posterior (predictedState model policy) outcome h

/-- Surprisal of one outcome under a policy.  Positivity is required by the
downstream posterior/VFE theorems rather than hidden in this total function. -/
noncomputable def outcomeSurprisal
    (model : GenerativeModel Policy State Outcome) (policy : Policy)
    (outcome : Outcome) : ℝ :=
  -Real.log (predictedOutcome model policy outcome)

/-- Posterior-form variational free energy:
`F[Q,o,π] = KL(Q || P(s|o,π)) - log P(o|π)`. -/
noncomputable def variationalFreeEnergy
    (model : GenerativeModel Policy State Outcome) (policy : Policy)
    (outcome : Outcome) (h : 0 < predictedOutcome model policy outcome)
    (recognition : FiniteLaw State) : ℝ :=
  finiteKL recognition (posteriorState model policy outcome h) +
    outcomeSurprisal model policy outcome

end FreeEnergyPrinciple

Source

fep_lean / fep_formal v1.2.0 (Active Inference Institute), FepSketches.active_inference.lean (proved, 0 sorry); https://github.com/ActiveInferenceInstitute/fep_formal

Read-back

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

Read-back: `GenerativeModel`, `predictedState`, `predictedOutcome`, `posteriorState`, `outcomeSurprisal`, `variationalFreeEnergy`

Structure GenerativeModel. For types $\mathsf{Policy}$ , $\mathsf{State}$ , $\mathsf{Outcome}$ that are all finite, a generative model is a record consisting of five pieces of data:

an initial state law $\rho \in \mathrm{FiniteLaw}(\mathsf{State})$ , i.e. a probability distribution over states;
a transition assignment $T$ , giving for each policy $\pi \in \mathsf{Policy}$ a finite transition kernel over states, $T(\pi) \in \mathrm{FiniteKernel}(\mathsf{State}, \mathsf{State})$ ;
a likelihood kernel $L \in \mathrm{FiniteKernel}(\mathsf{State}, \mathsf{Outcome})$ , mapping each state to a distribution over outcomes;
a preference law $p \in \mathrm{FiniteLaw}(\mathsf{Outcome})$ , a distribution over outcomes;
a policy prior $\sigma \in \mathrm{FiniteLaw}(\mathsf{Policy})$ , a distribution over policies.

Here $\mathrm{FiniteLaw}(X)$ denotes a probability law on the finite type $X$ and $\mathrm{FiniteKernel}(X, Y)$ a finite transition kernel from $X$ to $Y$ ; the structures used (FiniteLaw, FiniteKernel, finiteKL, and the predictive/posterior operations) are imported from a definitions module and their internal meaning is not restated in this file.

Definition predictedState. Given a model, a policy $\pi$ , the predicted state law is the predictive (pushforward) distribution obtained by applying the transition kernel $T(\pi)$ to the initial state law $\rho$ . This is total: it is defined for every policy, with no positivity or support condition.

Definition predictedOutcome. Given a model and a policy $\pi$ , the predicted outcome law is the predictive distribution obtained by applying the likelihood kernel $L$ to the predicted state law under $\pi$ . Again total, defined for every policy.

Definition posteriorState. Given a model, a policy $\pi$ , an outcome $o$ , and the explicit hypothesis that the predicted outcome mass $P(o \mid \pi)$ (as defined by predictedOutcome) is strictly positive, the posterior state law is the Bayesian posterior obtained by conditioning the predicted state law under $\pi$ on the outcome $o$ via the likelihood kernel's posterior operation. The definition is partial in the sense that it is only stated when $0 < P(o \mid \pi)$ ; for outcomes of zero predicted mass, this declaration provides no value.

Definition outcomeSurprisal. For a model, a policy $\pi$ , and an outcome $o$ , the surprisal is

-\log\big(P(o \mid \pi)\big),

the negative natural logarithm of the predicted outcome mass. This is a total function of $(\pi, o)$ : when $P(o \mid \pi) = 0$ the value is $+\infty$ -valued behavior of $\mathbb{R}$ -valued log is not guarded here — as written, the definition computes $-\log 0$ using the total real logarithm, so at zero-mass outcomes the value is whatever Real.log 0 evaluates to (it does not throw an error or return a special value), and no positivity assumption is baked into this definition. It is noncomputable.

Definition variationalFreeEnergy. Given a model, a policy $\pi$ , an outcome $o$ , the positivity hypothesis $0 < P(o \mid \pi)$ , and an arbitrary "recognition" state law $Q \in \mathrm{FiniteLaw}(\mathsf{State})$ , the posterior-form variational free energy is

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

that is, the finite KL divergence from the supplied recognition law $Q$ to the posterior state law (as defined above, which requires the same positivity hypothesis), plus the surprisal of $o$ under $\pi$ . Note precisely what is quantified: $Q$ is universally quantified and arbitrary — the definition imposes no constraint tying $Q$ to the model, so degenerate choices of $Q$ are included. The KL divergence used is the finiteKL operation on finite laws; as imported, it is applied to an arbitrary pair of state laws with no hypothesis guarding against non-absolute-continuity, so the value at pairs where $Q$ is not absolutely continuous with respect to the posterior is whatever finiteKL returns by its own convention (this file states none). The definition is noncomputable.

No theorem in this file asserts anything about these definitions; the declarations above are definitions only, and the positivity hypothesis $0 < P(o \mid \pi)$ appears in posteriorState and variationalFreeEnergy but not in predictedState, predictedOutcome, or outcomeSurprisal.

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

Finite generative model and posterior-form variational free energy

Read-back: GenerativeModel, predictedState, predictedOutcome, posteriorState, outcomeSurprisal, variationalFreeEnergy

Read-back: `GenerativeModel`, `predictedState`, `predictedOutcome`, `posteriorState`, `outcomeSurprisal`, `variationalFreeEnergy`