Expected free energy decomposes into risk plus ambiguity

Proved

FreeEnergyPrinciple.expectedFreeEnergy_eq_risk_add_ambiguity

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

active-inferenceexpected-free-energyfree-energy-principlepolicy-selection

The risk-plus-ambiguity decomposition of expected free energy — the canonical decomposition behind expected free energy in active inference [Friston et al. 2017].

Fix a finite generative model over policy, state, and outcome types, a policy $\pi$ , and suppose the model has full support: every predicted state, every predicted outcome, and every preference mass is strictly positive. Write

$G[\pi]$ for the expected free energy of the policy, defined as pragmatic cost minus epistemic value (the epistemic sign is fixed by definition);
$\mathrm{KL}\big(P(o\mid\pi)\,\|\,C\big)$ for the preference risk — divergence of the predicted outcome law from the preference law;
$H\big(A[\cdot\mid s]\big)$ averaged under $P(s\mid\pi)$ for the likelihood ambiguity.

Then

G[\pi] \;=\; \mathrm{KL}\big(P(o\mid\pi)\,\|\,C\big) \;+\; \sum_s P(s\mid\pi)\,H\big(A[\cdot\mid s]\big).

The proof runs through two entropy identities available from the definition layer: the epistemic value is the predicted outcome entropy minus the ambiguity (mutual information $I(s;o\mid\pi)$ via the entropy decomposition of the joint), and the risk is the cross-entropy minus the same outcome entropy (Gibbs' inequality under full reference support). Substituting both into the definition leaves exactly risk plus ambiguity.

A companion corollary available from the same substrate: the decomposition is a sum of nonnegative terms, so $G[\pi] \ge 0$ — but the decomposition itself, not mere nonnegativity, is the target.

Preamble

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

Formal statement

namespace FreeEnergyPrinciple

theorem expectedFreeEnergy_eq_risk_add_ambiguity
    {Policy State Outcome : Type*} [Fintype Policy] [Fintype State]
    [Fintype Outcome]
    (model : GenerativeModel Policy State Outcome) (policy : Policy)
    (support : FullSupport model) :
    expectedFreeEnergy model policy =
      risk model policy + ambiguity model policy := by sorry

end FreeEnergyPrinciple

Source

fep_lean / fep_formal v1.2.0 (Active Inference Institute), FepSketches.active_inference.lean, theorem expectedFreeEnergy_eq_risk_add_ambiguity (proved, 0 sorry); catalogue echo fep-021/fep-133; https://github.com/ActiveInferenceInstitute/fep_formal

Read-back

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

Let $\mathcal{P}$ (policies), $\mathcal{S}$ (states), $\mathcal{O}$ (outcomes) be arbitrary types, each equipped with a finite-type structure. The theorem asserts: for every generative model $M$ (a structure carrying an initial state law $P_0$ , a policy-indexed transition kernel $T_\pi$ , a likelihood kernel $K$ , a preference law $r$ , and a policy prior — all normalized real-valued mass functions on the finite types), every policy $\pi \in \mathcal{P}$ , and every certificate of full support of $M$ , we have

\mathbb{E}(M,\pi) = \operatorname{risk}(M,\pi) + \operatorname{ambiguity}(M,\pi).

Unfolding the bundle's own definitions, with $p_\pi(s) = \sum_{s'} P_0(s')T_\pi(s'|s)$ , $q_\pi(o) = \sum_s p_\pi(s)K(o|s)$ , and joint law $J_\pi(s,o) = p_\pi(s)K(o|s)$ :

\underbrace{\Big(\sum_o -q_\pi(o)\log r(o)\Big) - \mathrm{KL}\big(J_\pi \,\|\, p_\pi \otimes q_\pi\big)}_{\mathbb{E}(M,\pi)\;=\;\text{cross-entropy} - \text{mutual information}} \;=\; \underbrace{\sum_o r(o)\,\varphi\big(q_\pi(o)/r(o)\big)}_{\operatorname{risk}(M,\pi)} + \underbrace{\sum_s p_\pi(s) \sum_o \big(-K(o|s)\log K(o|s)\big)}_{\operatorname{ambiguity}(M,\pi)}

where $\varphi$ is the totalized KL integrand (defined at $0/0$ , contributing $0$ there), so the risk sum and the KL are finite even at zero-mass atoms. The full-support hypothesis consists of three strict-positivity assumptions: $p_\pi(s) > 0$ for all $\pi, s$ ; $q_\pi(o) > 0$ for all $\pi, o$ ; $r(o) > 0$ for all $o$ . These are the only assumptions; nothing is assumed about the policy prior, and no model failing positivity falls under the claim. The equality is an equation between real numbers, asserted for every policy and model; no converse is claimed. AUDITOR-FLAG: the proof body is a bare sorry — the statement is unproved as shipped in this artifact.

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