BlanketProjection
The projection structure supplies three maps from a state space to internal, blanket, and external components that realize the free-energy-principle partition. Researchers formalizing conditional independence for non-equilibrium steady states cite this when they need explicit events for blanket factorization over probability measures. The declaration is a plain structure definition with no axioms or computational content.
claimLet $Ω$, $I$, $B$, $E$ be types. A projection structure consists of three functions $π_I : Ω → I$, $π_B : Ω → B$, $π_E : Ω → E$ that assign to each state its internal, blanket, and external coordinates.
background
The module replaces predicate-based theorems with explicit factorization statements over ProbabilityMeasure objects. Conditional independence takes the blanket form $P(I=i, B=b, E=e) · P(B=b) = P(I=i, B=b) · P(B=b, E=e)$, which is the finite-event version of the Markov blanket condition. The projection structure supplies the coordinate maps that define the events appearing in this identity.
proof idea
The declaration is a structure definition that directly introduces the three projection functions internal, blanket, and external.
why it matters in Recognition Science
This structure is the domain type for atomSet, blanketSet, internalBlanketSet, CondIndepGivenBlanket, and the product-form theorem conditional_product_form. It supplies the concrete partition required to move the free-energy-principle Markov blanket into measure-theoretic language inside the Recognition Science information module.
scope and limits
- Does not impose measurability on the three projection maps.
- Does not encode the conditional independence identity itself.
- Does not specify or assume any probability measure on the state space.
- Does not restrict the cardinalities of the internal, blanket, or external spaces.
formal statement (Lean)
31structure BlanketProjection (Ω Internal Blanket External : Type*) where
32 internal : Ω → Internal
33 blanket : Ω → Blanket
34 external : Ω → External
35
36/-- Event where all three coarse-grained coordinates take specified values. -/