ledger_sparsity_implies_measure_condIndep
plain-language theorem explainer
The ledger boundary sparsity condition on a probability measure directly yields the conditional independence of internal and external variables given the blanket. Researchers deriving non-equilibrium steady state measures or FEP Markov blankets would cite this equivalence. The proof is a one-line exact match because the sparsity hypothesis and the target predicate are identical by definition.
Claim. Let $P$ be a probability measure on a space $Ω$. Let $π$ be a measurable projection of $Ω$ into internal, blanket, and external partitions. If for all internal values $i$, blanket values $b$, and external values $e$ the equality $P(atomSet(π,i,b,e)) · P(blanketSet(π,b)) = P(internalBlanketSet(π,i,b)) · P(blanketExternalSet(π,b,e))$ holds, then the conditional independence given the blanket holds for $P$ and $π$.
background
The module replaces generic True predicates with an explicit probability-factorization statement over ProbabilityMeasure. BlanketProjection supplies the three measurable maps that coarse-grain the state space into the FEP partition (internal, blanket, external). Both LedgerBoundarySparsity and CondIndepGivenBlanket are defined by the same product identity on the atom, blanket, internal-blanket, and blanket-external sets; the module doc states this is the finite-valued event-level form of the FEP Markov blanket condition.
proof idea
The proof is a one-line wrapper that applies the identity between the ledger boundary sparsity hypothesis and the conditional independence predicate.
why it matters
This supplies the conditional_independence field of the NESSMeasureCert certificate constructed in nessMeasureCert_holds. It closes the step from the ledger sparsity assumption to the measure-theoretic statement required for non-equilibrium steady state analysis. The factorization aligns with the free-energy principle Markov blanket requirement and sits downstream of ledger factorization and observer forcing results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.