Negative variational free energy is an evidence lower bound

Proved

FreeEnergyPrinciple.negative_variational_free_energy_le_log_evidence

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

active-inferenceelbofree-energy-principlevariational-inference

The negative variational free energy is an evidence lower bound (ELBO form).

In the setting of the goal theorem, for every recognition density $Q$ :

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

Role: the form in which variational inference states the principle. Negating the variational free energy gives a functional whose value lower-bounds the log marginal likelihood (the log evidence): maximizing it over recognition densities moves recognition toward the posterior and tightens the bound. This is the same inequality as the goal theorem with both sides negated, recorded separately because it is the connecting form to variational-inference practice (ELBO) and to the expected-free-energy developments of active inference.

Formalization Note — transcribed from the proved theorem negative_variationalFreeEnergy_le_logEvidence 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 negative_variational_free_energy_le_log_evidence
    {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 recognition ≤
      Real.log (predictedOutcome model policy outcome) := by sorry

end FreeEnergyPrinciple

Source

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

Read-back

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

Read-back of negative_variational_free_energy_le_log_evidence.

Let $P$ , $S$ , $O$ be arbitrary types, each equipped with a finiteness structure (so that counting/probability constructions over them are available). Let model be a generative model as defined in this bundle — an object of type GenerativeModel Policy State Outcome — and let $u \in P$ be a policy and $o \in O$ an outcome.

Write $p := \text{predictedOutcome}(model, u, o)$ , a real number given by the bundle's function that, for this model, policy, and outcome, is interpreted as the model's predicted probability of the outcome. The statement assumes the hypothesis $0 < p$ ; note that this is a substantive assumption, not automatic — if the predicted quantity is zero or non-positive for some choice of model, policy, and outcome, the hypothesis fails and the theorem says nothing about that case. (Conversely, because the hypothesis appears as an explicit premise, the theorem is trivially true in any situation where no such positive $p$ exists.)

Let $\rho$ be an arbitrary element of FiniteLaw State, the bundle's type of finite probability laws on the state space; $\rho$ is universally quantified, so the claim must hold for every such recognition distribution. The bundle's quantity $\mathcal{F}$ := variationalFreeEnergy model u o h ρ is a real number depending on the model, the policy, the outcome, the positivity hypothesis $h$ , and the recognition density $\rho$ .

The theorem asserts:

-\mathcal{F} \;\le\; \log p.

Equivalently, $\mathcal{F} \ge -\log p$ for every recognition law $\rho$ , whenever the predicted outcome probability is strictly positive. The inequality is the non-strict $\le$ in the displayed direction; no equality case, uniqueness, or minimization claim is made, and no statement is made about which recognition law is optimal.

Symbols used above, all defined in this bundle's files (Def_fep_generative_model, Def_fep_finite_information, Def_fep_finite_laws): predictedOutcome, variationalFreeEnergy, GenerativeModel, and FiniteLaw. A precise unfolding of these definitions is not possible from the theorem statement alone; the auditor comparing this read-back against the intended claim should consult those definition files directly, in particular to confirm what predictedOutcome and variationalFreeEnergy actually compute and whether the argument $h$ affects the value of $\mathcal{F}$ .

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