atomSet
plain-language theorem explainer
atomSet defines the atomic event in state space Ω consisting of all outcomes where the internal, blanket, and external projections under a BlanketProjection simultaneously equal the fixed values i, b, and e. Researchers formalizing measure-theoretic conditional independence for the free-energy principle Markov blanket would cite this when building factorization statements over ProbabilityMeasure. The definition is a direct set comprehension over the three projection functions.
Claim. Let π be a BlanketProjection of Ω onto the triple (Internal, Blanket, External). For fixed i ∈ Internal, b ∈ Blanket, e ∈ External, the set atomSet(π, i, b, e) consists of all ω ∈ Ω such that π.internal(ω) = i, π.blanket(ω) = b, and π.external(ω) = e.
background
The module replaces predicate-based theorems with explicit probability-factorization statements over ProbabilityMeasure. Conditional independence is defined via the blanket factorization 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 and avoids division side-conditions in ENNReal. A BlanketProjection is the measurable structure that supplies the three coordinate maps internal, blanket, and external from Ω.
proof idea
The definition is a one-line set comprehension that collects states whose images under the three projection maps of BlanketProjection equal the supplied singletons i, b, and e.
why it matters
atomSet supplies the concrete event sets required by CondIndepGivenBlanket, the product-form theorem conditional_product_form, LedgerBoundarySparsity, and the NESSMeasureCert structure. It implements the event-level factorization that the module doc identifies as the finite-valued form of the FEP Markov blanket condition. In the Recognition Science setting it provides the information-layer interface needed for later connection to the forcing chain and phi-ladder, though that link is not yet formalized here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.