Native conditional independence of internal and external states given the blanket

Proved

FreeEnergyPrinciple.staticJoint_condIndepFun

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

conditional-independencefree-energy-principlemarkov-blanketmeasure-theory

The defining conditional-independence property of a Markov blanket, in Mathlib's native measure-theoretic predicate.

A static blanket model factorizes a finite joint over blanket $b$ (the sensory-active pair), internal states $i$ , and external states $e$ :

P(b, i, e) = P(b)\,P(i\mid b)\,P(e\mid b).

Finite laws embed as weighted sums of Dirac masses, so the authored factorization becomes a genuine probability measure on the discrete state space, and the blanket/internal/external coordinates become genuine random variables on it.

The target: the embedded static joint satisfies Mathlib's CondIndepFun predicate — internal and external coordinates are conditionally independent given the blanket coordinate,

I \;\perp_{[\,b\,]}\; E.

The proof does not pass through finite mutual information: it identifies the two authored conditional kernels with Mathlib's native conditional distributions (condDistrib) almost everywhere under the blanket marginal — the native blanket marginal is exactly the authored blanket law, and the blanket-internal and blanket-external marginals are the authored kernels composed with it — and then applies Mathlib's native characterization of conditional independence by the factorization of the $(b, i, e)$ -joint.

Two honesty constraints carry over from the source: internal and external carriers must be nonempty (so the conditional distributions exist), and the claim is exactly conditional independence — nonvacuity is witnessed by a Boolean model with two positively weighted, perfectly correlated blanket regimes, where internal and external states both copy the sensory coordinate (their unconditional association is nontrivial) while their conditional law at each blanket value is a product of point masses.

Preamble

import Mathlib.Probability.Independence.Conditional
import Definitions.Def_fep2_native_blanket

Formal statement

namespace FreeEnergyPrinciple
open MeasureTheory ProbabilityTheory

theorem staticJoint_condIndepFun
    {Internal Sensory Active External : Type*}
    [Fintype Internal] [Fintype Sensory] [Fintype Active] [Fintype External]
    [MeasurableSpace Internal] [MeasurableSpace Sensory]
    [MeasurableSpace Active] [MeasurableSpace External]
    [DiscreteMeasurableSpace Internal] [DiscreteMeasurableSpace Sensory]
    [DiscreteMeasurableSpace Active] [DiscreteMeasurableSpace External]
    [Nonempty Internal] [Nonempty External]
    (model : StaticModel Internal Sensory Active External) :
    ProbabilityTheory.CondIndepFun
      (MeasurableSpace.comap blanketCoordinate inferInstance)
      blanketCoordinate_measurable.comap_le
      internalCoordinate externalCoordinate
      (embeddedLaw (staticJoint model)) := by sorry

end FreeEnergyPrinciple

Source

fep_lean / fep_formal v1.2.0 (Active Inference Institute), FepSketches.native_blanket.lean, theorem staticJoint_condIndepFun (proved, 0 sorry); catalogue topics fep-138/fep-139; https://github.com/ActiveInferenceInstitute/fep_formal

Read-back

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

Theorem staticJoint_condIndepFun — literal statement. Let Internal, Sensory, Active, External be finite types, each with a discrete measurable space structure, with Internal and External nonempty. A model is exactly a triple $(P_B, P_{I\mid B}, P_{E\mid B})$ where $B = \text{Sensory}\times\text{Active}$ : a law $P_B$ on $B$ , and conditionals $P_{I\mid B}(b)$ on Internal and $P_{E\mid B}(b)$ on External (each summing to 1). Existence of a model forces $B$ nonempty, since $P_B$ must sum to 1. Let the state space be the nested-pair carrier $((B\times\text{Internal})\times\text{External})$ , and let $\mu$ be the probability measure assigning each state $((s,a),i,e)$ the mass $P_B(s,a)\,P_{I\mid B}(s,a)(i)\,P_{E\mid B}(s,a)(e)$ , built as a weighted sum of Dirac masses.

The theorem asserts: under $\mu$ , the random variables $I$ (state's Internal component) and $E$ (state's External component) are conditionally independent given the $\sigma$ -algebra generated by the blanket projection $b=(\text{sensory},\text{active})$ alone (the pullback of the blanket's measurable structure, assumed measurable). Unfolded, this means: for every subset $A\subseteq\text{Internal}$ and $B'\subseteq\text{External}$ (all subsets qualify — every carrier is discrete), as functions on the state space,

\mu[\,I\in A \text{ and } E\in B' \mid b\,] = \mu[\,I\in A\mid b\,]\cdot\mu[\,E\in B'\mid b\,]

holding $\mu$ -almost everywhere — equivalently, at every blanket value $b$ with $P_B(b)>0$ . No additional hypotheses; the conclusion is exactly Mathlib's conditional-independence predicate and nothing more.

AUDITOR-FLAG: the proof body is sorry — this artifact carries only the statement, unproven. AUDITOR-FLAG: Nonempty Internal/Nonempty External are stated but not Nonempty Sensory/Active; an empty Sensory or Active yields no model at all ( $P_B$ cannot sum to 1), so no vacuous instance arises.

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