BlanketProjection
plain-language theorem explainer
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.
Claim. Let $Ω$, $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.