internalBlanketSet
plain-language theorem explainer
internalBlanketSet defines the subset of states in Ω where the internal projection equals a fixed value i and the blanket projection equals a fixed value b. Researchers formalizing free-energy principle Markov blankets cite this construction when stating conditional independence via product factorization over probability measures. The definition is a direct set comprehension using the two projection maps from the BlanketProjection structure.
Claim. Let π be a blanket projection from Ω onto the triple (Internal, Blanket, External). For fixed i in Internal and b in Blanket, the set consists of all ω in Ω such that the internal coordinate of ω equals i and the blanket coordinate of ω equals b.
background
The module develops a measure-theoretic version of conditional independence for non-equilibrium steady states by replacing predicate-based statements with explicit factorization over a ProbabilityMeasure. A BlanketProjection is a measurable map from the state space Ω into three coarse-grained coordinates: internal, blanket, and external. This structure encodes the free-energy principle partition into a Markov blanket. The definition supplies the event set needed to express the product identity that defines conditional independence given the blanket.
proof idea
This is a one-line definition that directly constructs the set via comprehension over the internal and blanket projection maps supplied by the BlanketProjection structure. No lemmas are applied; the body is the predicate that the internal coordinate equals i and the blanket coordinate equals b.
why it matters
This event set is the basic building block for the downstream definitions of CondIndepGivenBlanket and LedgerBoundarySparsity, which encode the blanket factorization P(I=i, B=b, E=e) · P(B=b) = P(I=i, B=b) · P(B=b, E=e). It therefore supplies the concrete events required by the NESSMeasureCert structure that certifies conditional independence for probability measures. In the Recognition Science setting this supports the information-theoretic side of the forcing chain by giving an explicit factorization that aligns with the J-cost and recognition composition law at the level of coarse-grained coordinates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.