blanketExternalSet
plain-language theorem explainer
blanketExternalSet defines the event subset of Ω consisting of states ω where the blanket projection equals a fixed b and the external projection equals a fixed e, given a BlanketProjection π. Researchers formalizing the free-energy-principle Markov blanket in measure-theoretic terms cite this when writing the product identities that replace predicate-based conditional independence. The definition is a direct set comprehension that applies the two projection functions supplied by the BlanketProjection structure.
Claim. Let π be a BlanketProjection of Ω into the triple (Internal, Blanket, External). For fixed b ∈ Blanket and e ∈ External the set blanketExternalSet(π, b, e) equals {ω ∈ Ω | π.blanket(ω) = b ∧ π.external(ω) = e}.
background
The module replaces predicate-based conditional-independence theorems with explicit factorization statements over ProbabilityMeasure. Conditional independence is expressed by the identity 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 form of the FEP Markov-blanket condition. A BlanketProjection is the structure that supplies the three coordinate maps internal, blanket and external used to define the coarse-grained events.
proof idea
One-line definition that builds the set by the conjunction of the two equality conditions on the blanket and external projection functions taken from the BlanketProjection structure.
why it matters
The set is the joint blanket-external event required by the factorization identities. It is used directly by CondIndepGivenBlanket, conditional_product_form, LedgerBoundarySparsity and NESSMeasureCert. In the Recognition Science setting it supplies the concrete events needed for the information-theoretic side of the NESS description, consistent with the blanket factorization that appears in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.