CondIndepGivenBlanket
plain-language theorem explainer
CondIndepGivenBlanket encodes the blanket factorization for conditional independence in a probability measure over a partitioned state space. Workers on free-energy-principle models and non-equilibrium steady states cite it as the event-level Markov blanket condition. The definition directly states the product equality between the joint measure on internal-blanket-external events and the blanket marginal versus the two pairwise measures.
Claim. Let $P$ be a probability measure on state space $Ω$ and let $π$ be a blanket projection partitioning states into internal, blanket, and external components. Conditional independence given the blanket holds when $P(I=i, B=b, E=e) · P(B=b) = P(I=i, B=b) · P(B=b, E=e)$ for all values $i$, $b$, $e$ of the respective components.
background
This module replaces predicate-based theorems with explicit probability factorization over ProbabilityMeasure. It uses the standard blanket factorization $P(I=i, B=b, E=e) · P(B=b) = P(I=i, B=b) · P(B=b, E=e)$, which equals the conditional $P(I=i, E=e | B=b) = P(I=i | B=b) P(E=e | B=b)$ when $P(B=b) ≠ 0$. This is the finite event form of the FEP Markov blanket condition. BlanketProjection is a structure supplying measurable maps from $Ω$ to the three partitions. The definition relies on auxiliary sets such as the atom set for specific $(i,b,e)$ and the blanket set for $b$.
proof idea
The declaration is a direct definition that equates the two sides of the blanket factorization for every combination of internal, blanket, and external values. No lemmas are applied; it simply writes the required product identity using the measure induced by $P$ on the projected events.
why it matters
This definition supplies the target property for the ledger-sparsity-implies-measure-condIndep theorem and appears in the NESSMeasureCert structure. It fills the role of the explicit hypothesis for conditional independence in the information module, linking ledger boundary sparsity to the product form. In the Recognition Science setting it operationalizes the Markov blanket for NESS models without requiring division in the measure algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.