Expected free energy of a policy over the finite generative model

Definition

fep2_expected_free_energy

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

active-inferenceexpected-free-energyfree-energy-principlemutual-information

The expected-free-energy layer of the mission, built on the published Free Energy Principle I finite substrate.

Beyond FEP-I's marginals and kernels, this definition packages the joint-law bookkeeping the epistemic terms need: the first marginal of a finite joint law, the independent product of two finite laws, the fact that the generated joint's first marginal reconstructs its prior, the conditional entropy of a finite kernel under an input law, the kernel chain rule $H(P(x)\,P(y\mid x)) = H(P) + H(Y\mid X)$ , and mutual information as the finite KL from a joint law to the product of its marginals, together with its entropy-decomposition under full marginal support.

On top of the published generative model it then defines, for a policy $\pi$ :

the predicted state-outcome joint $P(s,o\mid\pi)$ of the model's likelihood over the predicted state law;
the preference risk $\mathrm{KL}(P(o\mid\pi)\,\|\,C)$ — divergence of predicted outcomes from preferred outcomes;
the likelihood ambiguity $H(A[\cdot\mid s])$ averaged under the predicted states — expected surprise about outcomes given latent states;
the epistemic value $I(s;o\mid\pi)$ — mutual information between latent state and outcome;
the pragmatic preference cost — expected negative log preference;
the expected free energy $G[\pi] = \text{pragmatic cost} - \text{epistemic value}$ , with the epistemic sign fixed by definition;
the full-support contract recording exactly which positivity the logarithmic decompositions need, and the two helper identities (epistemic value is predictive outcome entropy minus ambiguity; risk is cross-entropy minus predicted-outcome entropy) the mission's theorems rest on.

Zero-mass atoms are handled by the same totalized conventions as in FEP-I: entropy uses Real.negMulLog, so $0\log 0 = 0$ exactly.

Definition code

import Definitions.Def_fep_finite_laws
import Definitions.Def_fep_finite_information
import Definitions.Def_fep_generative_model
import Mathlib.Tactic

/-!
# Expected free energy (mission substrate)

Mission `Free Energy Principle II` expected-free-energy substrate, transcribed
from the proved module `FepSketches.active_inference` of the fep_lean
formalization (Active Inference Institute), reusing the published `Free
Energy Principle I` finite substrate.  One policy-conditioned layer owns the
predicted state-outcome joint and the four information functionals of expected
free energy: pragmatic cost, epistemic value, preference risk, and likelihood
ambiguity.  The epistemic sign is fixed by definition; the mission's theorems
derive the risk-plus-ambiguity decomposition and its nonnegativity.
-/

namespace FreeEnergyPrinciple

open Finset
open scoped BigOperators

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

/-! ## Marginals and independent products of finite laws -/

namespace FiniteLaw

/-- First marginal of a finite joint law. -/
def fstMarginal (p : FiniteLaw (α × β)) : FiniteLaw α where
  mass x := ∑ y : β, p (x, y)
  nonneg x := Finset.sum_nonneg fun y _ => p.nonneg (x, y)
  sum_one := by
    simpa [Fintype.sum_prod_type] using p.sum_one

/-- Independent product of two finite laws. -/
def product (p : FiniteLaw α) (q : FiniteLaw β) : FiniteLaw (α × β) where
  mass xy := p xy.1 * q xy.2
  nonneg xy := mul_nonneg (p.nonneg xy.1) (q.nonneg xy.2)
  sum_one := by
    classical
    rw [Fintype.sum_prod_type]
    simp_rw [← Finset.mul_sum, q.sum_one, mul_one]
    exact p.sum_one

/-- The first marginal of an independent product is its first factor. -/
theorem product_fstMarginal_mass (p : FiniteLaw α) (q : FiniteLaw β)
    (x : α) :
    (p.product q).fstMarginal x = p x := by
  simp [fstMarginal, product, ← Finset.mul_sum, q.sum_one]

/-- The second marginal of an independent product is its second factor. -/
theorem product_sndMarginal_mass (p : FiniteLaw α) (q : FiniteLaw β)
    (y : β) :
    (p.product q).sndMarginal y = q y := by
  simp [sndMarginal, product, ← Finset.sum_mul, p.sum_one]

end FiniteLaw

/-- The generated joint's first marginal reconstructs its prior. -/
theorem joint_fstMarginal_mass (prior : FiniteLaw α)
    (kernel : FiniteKernel α β) (x : α) :
    (kernel.joint prior).fstMarginal x = prior x := by
  simp [FiniteLaw.fstMarginal, FiniteKernel.joint, ← Finset.mul_sum,
    kernel.sum_one]

/-! ## Conditional entropy and mutual information -/

/-- Conditional entropy of a normalized finite kernel under an input law. -/
noncomputable def conditionalEntropy
    (prior : FiniteLaw α) (kernel : FiniteKernel α β) : ℝ :=
  ∑ x, prior x * entropy (kernel.row x)

/-- Entropy chain rule for the joint law generated by a finite kernel. -/
theorem entropy_joint_eq_add_conditional
    (prior : FiniteLaw α) (kernel : FiniteKernel α β) :
    entropy (kernel.joint prior) =
      entropy prior + conditionalEntropy prior kernel := by
  classical
  simp only [entropy, FiniteKernel.joint, Fintype.sum_prod_type,
    Real.negMulLog_mul, conditionalEntropy, FiniteKernel.row]
  simp_rw [Finset.sum_add_distrib]
  congr 1
  · apply Finset.sum_congr rfl
    intro x _
    rw [← Finset.sum_mul, kernel.sum_one, one_mul]
  · simp_rw [Finset.mul_sum]

/-- Mutual information as KL from a joint law to the product of its
marginals. -/
noncomputable def mutualInformation (joint : FiniteLaw (α × β)) : ℝ :=
  finiteKL joint (joint.fstMarginal.product joint.sndMarginal)

/-- Mutual information is nonnegative. -/
theorem mutualInformation_nonneg (joint : FiniteLaw (α × β)) :
    0 ≤ mutualInformation joint :=
  finiteKL_nonneg _ _

/-- Cross-entropy against the product of positive marginals separates into
the two marginal entropies. -/
theorem crossEntropy_product_marginals (joint : FiniteLaw (α × β))
    (hfst : ∀ x, 0 < joint.fstMarginal x)
    (hsnd : ∀ y, 0 < joint.sndMarginal y) :
    crossEntropy joint (joint.fstMarginal.product joint.sndMarginal) =
      entropy joint.fstMarginal + entropy joint.sndMarginal := by
  classical
  simp only [crossEntropy, entropy, Fintype.sum_prod_type, FiniteLaw.product]
  simp_rw [Real.log_mul (ne_of_gt (hfst _)) (ne_of_gt (hsnd _))]
  simp only [mul_add, neg_mul]
  simp_rw [Finset.sum_add_distrib]
  congr 1
  · apply Finset.sum_congr rfl
    intro x _
    simp only [FiniteLaw.fstMarginal, Real.negMulLog_eq_neg]
    rw [Finset.sum_neg_distrib, Finset.sum_mul]
  · rw [Finset.sum_comm]
    apply Finset.sum_congr rfl
    intro y _
    simp only [FiniteLaw.sndMarginal, Real.negMulLog_eq_neg]
    rw [Finset.sum_neg_distrib, Finset.sum_mul]

/-- Mutual information equals the entropy sum of the marginals minus joint
entropy whenever both marginals have full support. -/
theorem mutualInformation_eq_entropy_marginals (joint : FiniteLaw (α × β))
    (hfst : ∀ x, 0 < joint.fstMarginal x)
    (hsnd : ∀ y, 0 < joint.sndMarginal y) :
    mutualInformation joint =
      entropy joint.fstMarginal + entropy joint.sndMarginal - entropy joint := by
  rw [mutualInformation,
    finiteKL_eq_crossEntropy_sub_entropy _ _
      (fun xy => mul_pos (hfst xy.1) (hsnd xy.2)),
    crossEntropy_product_marginals joint hfst hsnd]

/-! ## Expected free energy of a policy -/

/-- Predicted state-outcome joint under a policy. -/
def predictedJoint (model : GenerativeModel Policy State Outcome)
    (policy : Policy) : FiniteLaw (State × Outcome) :=
  model.likelihood.joint (predictedState model policy)

/-- Preference risk: divergence of predicted outcomes from preferred
outcomes. -/
noncomputable def risk (model : GenerativeModel Policy State Outcome)
    (policy : Policy) : ℝ :=
  finiteKL (predictedOutcome model policy) model.preferences

/-- Likelihood ambiguity averaged under policy-conditioned predicted
states. -/
noncomputable def ambiguity (model : GenerativeModel Policy State Outcome)
    (policy : Policy) : ℝ :=
  conditionalEntropy (predictedState model policy) model.likelihood

/-- Epistemic value: mutual information between latent state and outcome. -/
noncomputable def epistemicValue
    (model : GenerativeModel Policy State Outcome) (policy : Policy) : ℝ :=
  mutualInformation (predictedJoint model policy)

/-- Pragmatic preference cost as expected negative log preference. -/
noncomputable def pragmaticCost
    (model : GenerativeModel Policy State Outcome) (policy : Policy) : ℝ :=
  crossEntropy (predictedOutcome model policy) model.preferences

/-- Expected free energy with the epistemic-value sign made explicit. -/
noncomputable def expectedFreeEnergy
    (model : GenerativeModel Policy State Outcome) (policy : Policy) : ℝ :=
  pragmaticCost model policy - epistemicValue model policy

/-- Support assumptions required for logarithmic EFE decompositions.  They
are not hidden in the model carrier. -/
structure FullSupport (model : GenerativeModel Policy State Outcome) : Prop where
  state_pos : ∀ policy state, 0 < predictedState model policy state
  outcome_pos : ∀ policy outcome, 0 < predictedOutcome model policy outcome
  preference_pos : ∀ outcome, 0 < model.preferences outcome

/-- Epistemic value is nonnegative because it is a finite KL divergence. -/
theorem epistemicValue_nonneg
    (model : GenerativeModel Policy State Outcome) (policy : Policy) :
    0 ≤ epistemicValue model policy :=
  mutualInformation_nonneg _

/-- The predicted joint reconstructs the predicted state marginal. -/
theorem predictedJoint_fstMarginal_mass
    (model : GenerativeModel Policy State Outcome) (policy : Policy)
    (state : State) :
    (predictedJoint model policy).fstMarginal state =
      predictedState model policy state :=
  joint_fstMarginal_mass _ _ _

/-- The predicted joint's second marginal is the predicted outcome law. -/
theorem predictedJoint_sndMarginal
    (model : GenerativeModel Policy State Outcome) (policy : Policy) :
    (predictedJoint model policy).sndMarginal =
      predictedOutcome model policy := rfl

/-- Preference risk is cross-entropy minus predicted-outcome entropy. -/
theorem risk_eq_crossEntropy_sub_entropy
    (model : GenerativeModel Policy State Outcome) (policy : Policy)
    (support : FullSupport model) :
    risk model policy =
      pragmaticCost model policy - entropy (predictedOutcome model policy) := by
  exact finiteKL_eq_crossEntropy_sub_entropy _ _ support.preference_pos

/-- Epistemic value is predictive outcome entropy minus likelihood
ambiguity. -/
theorem epistemicValue_eq_entropy_sub_ambiguity
    (model : GenerativeModel Policy State Outcome) (policy : Policy)
    (support : FullSupport model) :
    epistemicValue model policy =
      entropy (predictedOutcome model policy) - ambiguity model policy := by
  let joint := predictedJoint model policy
  have hfst : ∀ state, 0 < joint.fstMarginal state := by
    intro state
    rw [predictedJoint_fstMarginal_mass]
    exact support.state_pos policy state
  have hsnd : ∀ outcome, 0 < joint.sndMarginal outcome := by
    intro outcome
    rw [predictedJoint_sndMarginal]
    exact support.outcome_pos policy outcome
  have hfstLaw : joint.fstMarginal = predictedState model policy := by
    apply FiniteLaw.ext_mass
    funext state
    exact predictedJoint_fstMarginal_mass model policy state
  have hchain :
      entropy joint =
        entropy (predictedState model policy) + ambiguity model policy := by
    simpa [joint, predictedJoint, ambiguity] using
      entropy_joint_eq_add_conditional
        (predictedState model policy) model.likelihood
  rw [epistemicValue,
    mutualInformation_eq_entropy_marginals joint hfst hsnd,
    hfstLaw, predictedJoint_sndMarginal, hchain]
  ring

end FreeEnergyPrinciple

Source

fep_lean / fep_formal v1.2.0 (Active Inference Institute), FepSketches.active_inference.lean (proved, 0 sorry) — the EFE layer `risk`, `ambiguity`, `epistemicValue`, `pragmaticCost`, `expectedFreeEnergy`, `FullSupport` plus the marginal/mutual-information substrate of FepSketches.finite_probability and FepSketches.finite_information; https://github.com/ActiveInferenceInstitute/fep_formal

Read-back

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

In namespace FreeEnergyPrinciple, for finite types $\alpha,\beta$ (with Policy, State, Outcome finite too), the file defines over a FiniteLaw (a real mass function with pointwise-nonnegativity and total-mass-1 fields, visible from its constructor uses) and a GenerativeModel carrying a FiniteKernel likelihood, predictedState, predictedOutcome, and preferences (upstream shapes; not visible in this file):

$\mathrm{conditionalEntropy}(\pi, K) = \sum_x \pi(x)\, H(K\,\text{row}\,x)$ for prior law $\pi$ and kernel $K$ .
$\mathrm{mutualInformation}(J) = \mathrm{finiteKL}(J,\ \mathrm{fstMarginal}(J)\cdot \mathrm{sndMarginal}(J))$ — the KL divergence from a joint law to its independent-product marginals.
For a model $M$ $M$ and policy $p$ $p$ :
- $\mathrm{predictedJoint}(M,p) = M.\mathrm{likelihood} \cdot \mathrm{predictedState}(M,p)$ (kernel joint with predicted state law), a law on $\mathrm{State}\times\mathrm{Outcome}$ .
- $\mathrm{risk}(M,p) = \mathrm{finiteKL}(\mathrm{predictedOutcome}(M,p),\ M.\mathrm{preferences})$ .
- $\mathrm{ambiguity}(M,p) = \mathrm{conditionalEntropy}(\mathrm{predictedState}(M,p),\ M.\mathrm{likelihood})$ .
- $\mathrm{epistemicValue}(M,p) = \mathrm{mutualInformation}(\mathrm{predictedJoint}(M,p))$ .
- $\mathrm{pragmaticCost}(M,p) = \mathrm{crossEntropy}(\mathrm{predictedOutcome}(M,p),\ M.\mathrm{preferences})$ .
- $\boxed{\mathrm{expectedFreeEnergy}(M,p) = \mathrm{pragmaticCost}(M,p) - \mathrm{epistemicValue}(M,p)}$ .

A predicate FullSupport bundles three positivity hypotheses (all predicted states, all predicted outcomes, and all preferences strictly positive); the decomposition theorems (risk = pragmaticCost $-$ outcome entropy; $\mathrm{epistemicValue} =$ outcome entropy $-$ ambiguity) explicitly require FullSupport, which is therefore not hidden in the model carrier.

AUDITOR-FLAG: The epistemic term's sign is fixed by definition (subtracted nonnegative mutual information); nothing in this file states the risk-plus-ambiguity decomposition itself. AUDITOR-FLAG: risk, pragmaticCost, ambiguity, expectedFreeEnergy are defined unconditionally — positivity assumptions live only in the theorems, so these real-valued functions may evaluate to junk where supports are empty. AUDITOR-FLAG: All entropy/KL functionals are noncomputable; predictedJoint and the marginals are computable. The two marginal product-factors $\prod$ and chain-rule theorems are proven, not assumed.

[You have received this identical output 3 times. Re-reading 'agent://Aud0/readback' will not change it — use a narrower selector (path:A-B), or proceed with the edit.]

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