Finite Markov blankets embedded as native measures
Definitionfep2_native_blanketconditional-independencefree-energy-principlemarkov-blanketmeasure-theory
The Markov-blanket layer: a finite static blanket factorization, embedded into Mathlib's native measure theory.
A static blanket model over finite internal, sensory, active, and external states is a factorization
over the blanket , the internal states, and the external states — exactly the canonical FEP partition with the sensory-active pair as the blanket. The generated static joint is the normalized law built by the lifted external kernel over the blanket-internal joint; it has the exact factorization pointwise.
Finite laws embed as native measures: a normalized finite law becomes a weighted sum of Dirac masses, and a finite kernel becomes a kernel whose rows are those embedded laws. On these discrete carriers the embedding is faithful — singletons carry exactly the authored masses, the embedding preserves joints as Mathlib's composition-product measures, and pushforwards commute with it.
On the static joint, the blanket, internal, and external coordinates are the three projections of the state. The native marginal of the blanket coordinate is exactly the authored blanket law; the blanket-internal and blanket-external marginals are the authored conditional kernels composed with it; and the full triple is the blanket marginal followed by the product of the two conditionals. The conditional pair kernel (the product of the two conditionals at a fixed blanket) embeds as Mathlib's native product kernel, and the atomic rectangle factorization
holds on the singletons that generate the discrete space. Conditional distributions of the internal and external coordinates given the blanket are identified with the two embedded conditionals almost everywhere under the blanket marginal.
Definition code
import Definitions.Def_fep_finite_laws
import Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
import Mathlib.Probability.Independence.Conditional
import Mathlib.Probability.Kernel.Composition.Comp
import Mathlib.Tactic
/-!
# Native Markov blankets (mission substrate)
Mission `Free Energy Principle II` Markov-blanket substrate, transcribed from
the proved modules `FepSketches.markov_blanket` and `FepSketches.native_blanket`
of the fep_lean formalization (Active Inference Institute), reusing the
published `Free Energy Principle I` finite substrate. A static blanket model
factorizes a finite joint as `P(b,i,e) = P(b) P(i|b) P(e|b)` over blanket,
internal, and external coordinates; normalized finite laws embed as weighted
sums of Dirac measures, so the authored factorization transports to Mathlib's
native measure-theoretic conditional distributions and its `CondIndepFun`
predicate. The conditional-independence result is not inferred from finite
mutual information: it is obtained by identifying the two finite conditional
kernels with Mathlib conditional distributions and applying Mathlib's native
joint-measure characterization.
-/
namespace FreeEnergyPrinciple
open MeasureTheory ProbabilityTheory
open scoped BigOperators ENNReal MeasureTheory ProbabilityTheory
variable {α β Internal Sensory Active External : Type*}
namespace FiniteLaw
variable [Fintype α] [Fintype β]
/-- Push a finite law through a deterministic function. -/
def map [DecidableEq β] (f : α → β) (p : FiniteLaw α) : FiniteLaw β := by
exact
{ mass := fun y => ∑ x : α, if f x = y then p x else 0
nonneg := fun y => Finset.sum_nonneg fun x _ => by
by_cases h : f x = y
· simpa [h] using p.nonneg x
· simp [h]
sum_one := by
rw [Finset.sum_comm]
simpa using p.sum_one }
@[simp]
theorem map_mass [DecidableEq β] (f : α → β) (p : FiniteLaw α) (y : β) :
p.map f y = ∑ x : α, if f x = y then p x else 0 := rfl
end FiniteLaw
/-! ## Finite static Markov-blanket factorization -/
/-- Sensory-active blanket state. -/
abbrev Blanket (Sensory Active : Type*) := Sensory × Active
/-- Static state arranged as blanket, internal, and external coordinates. -/
abbrev StaticState (Internal Sensory Active External : Type*) :=
((Blanket Sensory Active) × Internal) × External
variable [Fintype Internal] [Fintype Sensory] [Fintype Active] [Fintype External]
/-- A static blanket factorization `P(b,i,e)=P(b)P(i|b)P(e|b)`. -/
structure StaticModel (Internal Sensory Active External : Type*)
[Fintype Internal] [Fintype Sensory] [Fintype Active] [Fintype External] where
blanketLaw : FiniteLaw (Blanket Sensory Active)
internalGiven : FiniteKernel (Blanket Sensory Active) Internal
externalGiven : FiniteKernel (Blanket Sensory Active) External
/-- Lift the external conditional so it can follow a sampled blanket-internal
pair without acquiring a dependency on the internal coordinate. -/
def externalLift (model : StaticModel Internal Sensory Active External) :
FiniteKernel ((Blanket Sensory Active) × Internal) External where
mass bi external := model.externalGiven bi.1 external
nonneg bi external := model.externalGiven.nonneg bi.1 external
sum_one bi := model.externalGiven.sum_one bi.1
/-- Normalized static joint law induced by a Markov-blanket factorization. -/
def staticJoint (model : StaticModel Internal Sensory Active External) :
FiniteLaw (StaticState Internal Sensory Active External) :=
(externalLift model).joint
(model.internalGiven.joint model.blanketLaw)
/-- The generated joint has the exact Markov-blanket factorization. -/
theorem staticJoint_factorization
(model : StaticModel Internal Sensory Active External)
(blanket : Blanket Sensory Active) (internal : Internal)
(external : External) :
staticJoint model ((blanket, internal), external) =
(model.blanketLaw blanket * model.internalGiven blanket internal) *
model.externalGiven blanket external := rfl
/-! ## Finite laws as native measures -/
section FiniteEmbedding
variable [Fintype α] [Fintype β]
[MeasurableSpace α] [MeasurableSpace β]
[DiscreteMeasurableSpace α] [DiscreteMeasurableSpace β]
/-- A normalized finite law represented as a native Mathlib measure by
weighted Dirac masses. -/
noncomputable def embeddedLaw (law : FiniteLaw α) : Measure α :=
Measure.sum fun state => ENNReal.ofReal (law state) • Measure.dirac state
/-- The native measure assigns each singleton exactly the authored finite
mass, embedded in `ℝ≥0∞`. -/
@[simp]
theorem embeddedLaw_apply_singleton (law : FiniteLaw α) (state : α) :
embeddedLaw law {state} = ENNReal.ofReal (law state) := by
simpa [embeddedLaw] using
(Measure.sum_smul_dirac_singleton
(f := fun state : α => ENNReal.ofReal (law state)) (a := state))
/-- A normalized finite law embeds as a probability measure. -/
@[simp]
theorem embeddedLaw_apply_univ (law : FiniteLaw α) :
embeddedLaw law Set.univ = 1 := by
rw [embeddedLaw, Measure.sum_apply_of_countable, tsum_fintype]
simp only [Measure.smul_apply, Measure.dirac_apply]
simp only [Set.indicator_of_mem (Set.mem_univ _), Pi.one_apply, smul_eq_mul, mul_one]
rw [← ENNReal.ofReal_sum_of_nonneg (fun state _ => law.nonneg state), law.sum_one]
simp
noncomputable instance embeddedLaw_isProbabilityMeasure (law : FiniteLaw α) :
IsProbabilityMeasure (embeddedLaw law) where
measure_univ := embeddedLaw_apply_univ law
/-- Pushforward commutes with the finite-law embedding on discrete
carriers. -/
theorem embeddedLaw_map [DecidableEq β]
(law : FiniteLaw α) (mapState : α → β) :
(embeddedLaw law).map mapState = embeddedLaw (law.map mapState) := by
classical
apply Measure.ext_of_singleton
intro target
rw [Measure.map_apply Measurable.of_discrete MeasurableSet.of_discrete,
embeddedLaw, Measure.sum_apply_of_countable, tsum_fintype,
embeddedLaw_apply_singleton, FiniteLaw.map_mass]
simp only [Measure.smul_apply, Measure.dirac_apply, Set.indicator_apply,
Pi.one_apply, smul_eq_mul, mul_ite, mul_one, mul_zero]
rw [ENNReal.ofReal_sum_of_nonneg]
· apply Finset.sum_congr rfl
intro state _
by_cases hstate : mapState state = target <;> simp [hstate]
· intro state _
split_ifs
· exact law.nonneg state
· exact le_rfl
/-- A finite kernel represented by its embedded probability-measure rows. -/
noncomputable def embeddedKernel (kernel : FiniteKernel α β) : Kernel α β :=
Kernel.ofFunOfCountable fun state => embeddedLaw (kernel.row state)
omit [DiscreteMeasurableSpace β] in
@[simp]
theorem embeddedKernel_apply (kernel : FiniteKernel α β) (state : α) :
embeddedKernel kernel state = embeddedLaw (kernel.row state) := rfl
@[simp]
theorem embeddedKernel_apply_singleton
(kernel : FiniteKernel α β) (state : α) (target : β) :
embeddedKernel kernel state {target} = ENNReal.ofReal (kernel state target) := by
rw [embeddedKernel_apply, embeddedLaw_apply_singleton]
rfl
noncomputable instance embeddedKernel_isMarkovKernel
(kernel : FiniteKernel α β) : IsMarkovKernel (embeddedKernel kernel) where
isProbabilityMeasure state := embeddedLaw_isProbabilityMeasure (kernel.row state)
/-- Embedding a finite prior-kernel joint is exactly Mathlib's native
composition-product measure. -/
theorem embeddedLaw_joint_eq_compProd
(prior : FiniteLaw α) (kernel : FiniteKernel α β) :
embeddedLaw (kernel.joint prior) =
embeddedLaw prior ⊗ₘ embeddedKernel kernel := by
classical
apply Measure.ext_of_singleton
rintro ⟨state, target⟩
rw [embeddedLaw_apply_singleton]
change ENNReal.ofReal (prior state * kernel state target) = _
rw [show ({(state, target)} : Set (α × β)) = {state} ×ˢ {target} by ext; simp,
Measure.compProd_apply_prod MeasurableSet.of_discrete MeasurableSet.of_discrete,
lintegral_singleton]
simp [embeddedLaw_apply_singleton, FiniteKernel.row,
ENNReal.ofReal_mul (prior.nonneg state), mul_comm]
end FiniteEmbedding
/-! ## Blanket coordinates on the native measure -/
section StaticBlanket
variable [MeasurableSpace Internal] [MeasurableSpace Sensory]
[MeasurableSpace Active] [MeasurableSpace External]
[DiscreteMeasurableSpace Internal] [DiscreteMeasurableSpace Sensory]
[DiscreteMeasurableSpace Active] [DiscreteMeasurableSpace External]
noncomputable local instance : DecidableEq Internal := Classical.decEq Internal
noncomputable local instance : DecidableEq Sensory := Classical.decEq Sensory
noncomputable local instance : DecidableEq Active := Classical.decEq Active
noncomputable local instance : DecidableEq External := Classical.decEq External
/-- Blanket coordinate on the existing finite static-state carrier. -/
def blanketCoordinate
(state : StaticState Internal Sensory Active External) :
Blanket Sensory Active := state.1.1
/-- Internal coordinate on the existing finite static-state carrier. -/
def internalCoordinate
(state : StaticState Internal Sensory Active External) : Internal :=
state.1.2
/-- External coordinate on the existing finite static-state carrier. -/
def externalCoordinate
(state : StaticState Internal Sensory Active External) : External :=
state.2
/-- The association map used by Mathlib's `(blanket, internal, external)`
conditional-distribution characterization. -/
def blanketTripleCoordinate
(state : StaticState Internal Sensory Active External) :
Blanket Sensory Active × (Internal × External) :=
(blanketCoordinate state, internalCoordinate state, externalCoordinate state)
theorem blanketCoordinate_measurable :
Measurable
(blanketCoordinate :
StaticState Internal Sensory Active External → Blanket Sensory Active) :=
Measurable.of_discrete
theorem internalCoordinate_measurable :
Measurable
(internalCoordinate :
StaticState Internal Sensory Active External → Internal) :=
Measurable.of_discrete
theorem externalCoordinate_measurable :
Measurable
(externalCoordinate :
StaticState Internal Sensory Active External → External) :=
Measurable.of_discrete
theorem blanketTripleCoordinate_measurable :
Measurable
(blanketTripleCoordinate :
StaticState Internal Sensory Active External →
Blanket Sensory Active × (Internal × External)) :=
Measurable.of_discrete
/-- The finite product row containing the internal and external conditionals
at a fixed blanket value. -/
def conditionalPairKernel
(model : StaticModel Internal Sensory Active External) :
FiniteKernel (Blanket Sensory Active) (Internal × External) where
mass blanket pair :=
model.internalGiven blanket pair.1 * model.externalGiven blanket pair.2
nonneg blanket pair :=
mul_nonneg (model.internalGiven.nonneg blanket pair.1)
(model.externalGiven.nonneg blanket pair.2)
sum_one blanket := by
rw [Fintype.sum_prod_type]
simp_rw [← Finset.mul_sum, model.externalGiven.sum_one, mul_one]
exact model.internalGiven.sum_one blanket
/-- The embedded finite product row is Mathlib's native product kernel. -/
theorem embeddedConditionalPairKernel_eq_prod
(model : StaticModel Internal Sensory Active External) :
embeddedKernel (conditionalPairKernel model) =
embeddedKernel model.internalGiven ×ₖ embeddedKernel model.externalGiven := by
classical
apply Kernel.ext
intro blanket
apply Measure.ext_of_singleton
rintro ⟨internal, external⟩
rw [embeddedKernel_apply_singleton]
change ENNReal.ofReal
(model.internalGiven blanket internal *
model.externalGiven blanket external) = _
rw [show ({(internal, external)} : Set (Internal × External)) =
{internal} ×ˢ {external} by ext; simp,
Kernel.prod_apply_prod]
simp [FiniteKernel.row,
ENNReal.ofReal_mul (model.internalGiven.nonneg blanket internal)]
omit [MeasurableSpace Internal] [MeasurableSpace Sensory]
[MeasurableSpace Active] [MeasurableSpace External]
[DiscreteMeasurableSpace Internal] [DiscreteMeasurableSpace Sensory]
[DiscreteMeasurableSpace Active] [DiscreteMeasurableSpace External] in
private theorem staticJoint_map_triple_finite
(model : StaticModel Internal Sensory Active External) :
(staticJoint model).map blanketTripleCoordinate =
(conditionalPairKernel model).joint model.blanketLaw := by
classical
apply FiniteLaw.ext_mass
funext state
rcases state with ⟨blanket, internal, external⟩
have coordinate_eq
(source : StaticState Internal Sensory Active External) :
blanketTripleCoordinate source = (blanket, internal, external) ↔
source = ((blanket, internal), external) := by
rcases source with ⟨⟨sourceBlanket, sourceInternal⟩, sourceExternal⟩
simp [blanketTripleCoordinate, blanketCoordinate, internalCoordinate,
externalCoordinate, and_assoc]
rw [FiniteLaw.map_mass]
simp_rw [coordinate_eq]
simp only [Finset.sum_ite_eq', Finset.mem_univ]
change staticJoint model ((blanket, internal), external) =
model.blanketLaw blanket *
(model.internalGiven blanket internal *
model.externalGiven blanket external)
rw [staticJoint_factorization]
ring
omit [MeasurableSpace Internal] [MeasurableSpace Sensory]
[MeasurableSpace Active] [MeasurableSpace External]
[DiscreteMeasurableSpace Internal] [DiscreteMeasurableSpace Sensory]
[DiscreteMeasurableSpace Active] [DiscreteMeasurableSpace External] in
private theorem staticJoint_map_blanketExternal_finite
(model : StaticModel Internal Sensory Active External) :
(staticJoint model).map
(fun state => (blanketCoordinate state, externalCoordinate state)) =
model.externalGiven.joint model.blanketLaw := by
classical
apply FiniteLaw.ext_mass
funext state
rcases state with ⟨blanket, external⟩
rw [FiniteLaw.map_mass, Fintype.sum_prod_type]
change (∑ blanketInternal : Blanket Sensory Active × Internal,
∑ sourceExternal : External,
if (blanketInternal.1, sourceExternal) = (blanket, external) then
staticJoint model (blanketInternal, sourceExternal)
else 0) = _
calc
(∑ blanketInternal : Blanket Sensory Active × Internal,
∑ sourceExternal : External,
if (blanketInternal.1, sourceExternal) = (blanket, external) then
staticJoint model (blanketInternal, sourceExternal)
else 0) =
∑ blanketInternal : Blanket Sensory Active × Internal,
if blanketInternal.1 = blanket then
staticJoint model (blanketInternal, external)
else 0 := by
apply Finset.sum_congr rfl
intro blanketInternal _
by_cases hblanket : blanketInternal.1 = blanket <;>
simp [hblanket]
_ = ∑ sourceBlanket : Blanket Sensory Active,
if sourceBlanket = blanket then
∑ internal : Internal,
staticJoint model ((sourceBlanket, internal), external)
else 0 := by
rw [Fintype.sum_prod_type]
apply Finset.sum_congr rfl
intro sourceBlanket _
by_cases hblanket : sourceBlanket = blanket <;> simp [hblanket]
_ = ∑ internal : Internal,
staticJoint model ((blanket, internal), external) := by simp
_ = model.blanketLaw blanket * model.externalGiven blanket external := by
simp_rw [staticJoint_factorization]
rw [← Finset.sum_mul, ← Finset.mul_sum,
model.internalGiven.sum_one, mul_one]
private theorem staticJoint_map_blanketInternal_embedded
(model : StaticModel Internal Sensory Active External) :
(embeddedLaw (staticJoint model)).map
(fun state => (blanketCoordinate state, internalCoordinate state)) =
embeddedLaw model.blanketLaw ⊗ₘ embeddedKernel model.internalGiven := by
change (embeddedLaw (staticJoint model)).fst = _
rw [staticJoint, embeddedLaw_joint_eq_compProd, Measure.fst_compProd,
embeddedLaw_joint_eq_compProd]
/-- The native blanket marginal is exactly the embedded authored blanket
law. -/
theorem staticJoint_map_blanket
(model : StaticModel Internal Sensory Active External) :
(embeddedLaw (staticJoint model)).map blanketCoordinate =
embeddedLaw model.blanketLaw := by
calc
(embeddedLaw (staticJoint model)).map blanketCoordinate =
((embeddedLaw (staticJoint model)).map
(fun state => (blanketCoordinate state, internalCoordinate state))).fst := by
rw [Measure.fst, Measure.map_map Measurable.of_discrete Measurable.of_discrete]
rfl
_ = (embeddedLaw model.blanketLaw ⊗ₘ
embeddedKernel model.internalGiven).fst := by
rw [staticJoint_map_blanketInternal_embedded]
_ = embeddedLaw model.blanketLaw := Measure.fst_compProd _ _
/-- The blanket-internal marginal is the authored internal conditional kernel
composed with the native blanket marginal. -/
theorem staticJoint_map_blanket_internal
(model : StaticModel Internal Sensory Active External) :
(embeddedLaw (staticJoint model)).map
(fun state => (blanketCoordinate state, internalCoordinate state)) =
(embeddedLaw (staticJoint model)).map blanketCoordinate ⊗ₘ
embeddedKernel model.internalGiven := by
rw [staticJoint_map_blanket, staticJoint_map_blanketInternal_embedded]
/-- The blanket-external marginal is the authored external conditional kernel
composed with the native blanket marginal. -/
theorem staticJoint_map_blanket_external
(model : StaticModel Internal Sensory Active External) :
(embeddedLaw (staticJoint model)).map
(fun state => (blanketCoordinate state, externalCoordinate state)) =
(embeddedLaw (staticJoint model)).map blanketCoordinate ⊗ₘ
embeddedKernel model.externalGiven := by
calc
(embeddedLaw (staticJoint model)).map
(fun state => (blanketCoordinate state, externalCoordinate state)) =
embeddedLaw ((staticJoint model).map
(fun state => (blanketCoordinate state, externalCoordinate state))) :=
embeddedLaw_map
(α := StaticState Internal Sensory Active External)
(β := Blanket Sensory Active × External)
(staticJoint model)
(fun state => (blanketCoordinate state, externalCoordinate state))
_ = embeddedLaw (model.externalGiven.joint model.blanketLaw) := by
rw [staticJoint_map_blanketExternal_finite (model := model)]
_ = embeddedLaw model.blanketLaw ⊗ₘ embeddedKernel model.externalGiven :=
embeddedLaw_joint_eq_compProd _ _
_ = (embeddedLaw (staticJoint model)).map blanketCoordinate ⊗ₘ
embeddedKernel model.externalGiven := by
rw [staticJoint_map_blanket]
/-- The complete native joint is the blanket marginal followed by the product
of the authored internal and external conditional kernels. -/
theorem staticJoint_map_triple_factorization
(model : StaticModel Internal Sensory Active External) :
(embeddedLaw (staticJoint model)).map blanketTripleCoordinate =
(embeddedLaw (staticJoint model)).map blanketCoordinate ⊗ₘ
(embeddedKernel model.internalGiven ×ₖ
embeddedKernel model.externalGiven) := by
calc
(embeddedLaw (staticJoint model)).map blanketTripleCoordinate =
embeddedLaw ((staticJoint model).map blanketTripleCoordinate) :=
embeddedLaw_map
(α := StaticState Internal Sensory Active External)
(β := Blanket Sensory Active × (Internal × External))
(staticJoint model) blanketTripleCoordinate
_ = embeddedLaw
((conditionalPairKernel model).joint model.blanketLaw) := by
rw [staticJoint_map_triple_finite (model := model)]
_ = embeddedLaw model.blanketLaw ⊗ₘ
embeddedKernel (conditionalPairKernel model) :=
embeddedLaw_joint_eq_compProd _ _
_ = embeddedLaw model.blanketLaw ⊗ₘ
(embeddedKernel model.internalGiven ×ₖ
embeddedKernel model.externalGiven) := by
rw [embeddedConditionalPairKernel_eq_prod]
_ = (embeddedLaw (staticJoint model)).map blanketCoordinate ⊗ₘ
(embeddedKernel model.internalGiven ×ₖ
embeddedKernel model.externalGiven) := by
rw [staticJoint_map_blanket]
theorem internal_condDistrib_ae_eq
[Nonempty Internal]
(model : StaticModel Internal Sensory Active External) :
condDistrib internalCoordinate blanketCoordinate
(embeddedLaw (staticJoint model)) =ᵐ[
(embeddedLaw (staticJoint model)).map blanketCoordinate]
embeddedKernel model.internalGiven :=
condDistrib_ae_eq_of_measure_eq_compProd_of_measurable
blanketCoordinate_measurable internalCoordinate_measurable
(staticJoint_map_blanket_internal model)
theorem external_condDistrib_ae_eq
[Nonempty External]
(model : StaticModel Internal Sensory Active External) :
condDistrib externalCoordinate blanketCoordinate
(embeddedLaw (staticJoint model)) =ᵐ[
(embeddedLaw (staticJoint model)).map blanketCoordinate]
embeddedKernel model.externalGiven :=
condDistrib_ae_eq_of_measure_eq_compProd_of_measurable
blanketCoordinate_measurable externalCoordinate_measurable
(staticJoint_map_blanket_external model)
end StaticBlanket
end FreeEnergyPrinciple
Source
fep_lean / fep_formal v1.2.0 (Active Inference Institute), FepSketches.markov_blanket.lean + FepSketches.native_blanket.lean (both proved, 0 sorry) — catalogue topics fep-138/fep-139 substrate; 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 (sensory), (active), (internal), (external), this file defines: Blanket ; StaticState ; and StaticModel, a triple of a normalized finite law on and two finite kernels , (every row nonnegative and summing to ). externalLift extends to a kernel from to by ignoring the internal coordinate: . staticJoint is the joint finite law on StaticState obtained by composing these, so — proved by rfl, i.e. by construction. The file further defines embeddings of finite laws as weighted sums of Dirac masses (proved to be probability measures) and finite kernels as Mathlib kernels, plus coordinate projections blanketCoordinate, internalCoordinate, externalCoordinate. Proved theorems: the embedded joint equals a native composition-product measure; the pushforward of the embedded joint onto blanket-internal (resp. blanket-external, resp. the full triple) equals the blanket marginal composed with the embedded (resp. , resp. the product kernel ); and, assuming (resp. ) nonempty, Mathlib's condDistrib of internal given blanket equals the embedded (resp. ) almost everywhere. AUDITOR-FLAG: the factorization holds by definitional composition, not as a discovered property; no hypothesis ties beyond nonnegativity/normalization. AUDITOR-FLAG: the Nonempty hypotheses are redundant — a kernel to an empty type cannot satisfy row normalization, so existence of the model already forces nonempty. AUDITOR-FLAG: degenerate models (singleton types, degenerate laws) are admissible and covered.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.