blanketSet
plain-language theorem explainer
The blanketSet definition extracts the preimage of a fixed blanket value b under the blanket coordinate map of a BlanketProjection π. Researchers formulating the free-energy principle in measure-theoretic terms cite this when stating conditional independence via blanket factorization over internal, blanket, and external events. It is a direct set comprehension that isolates the conditioning event from the projection structure.
Claim. Let π be a measurable projection of the state space Ω into internal, blanket, and external coordinates. For a fixed blanket value b, the blanket event is the set {ω ∈ Ω | π.blanket(ω) = b}.
background
This module replaces predicate-based statements with explicit probability-factorization over a ProbabilityMeasure, using the standard blanket factorization P(I=i, B=b, E=e) · P(B=b) = P(I=i, B=b) · P(B=b, E=e). The BlanketProjection structure supplies three measurable maps from Ω to the FEP partitions: internal, blanket, and external. The blanketSet isolates the event where the blanket coordinate equals a specified b, which serves as the conditioning set in the factorization identity.
proof idea
The definition is a direct set comprehension that applies the blanket projection function from the BlanketProjection structure to select states matching the given b.
why it matters
This definition supplies the blanket event used in CondIndepGivenBlanket and the product-form theorem conditional_product_form. It implements the event-level form of the FEP Markov blanket condition inside the NESSMeasureCert structure. The construction supports deriving ledger-boundary sparsity from recognition-field generators in later work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.