LedgerBoundarySparsity
plain-language theorem explainer
LedgerBoundarySparsity encodes the blanket factorization for a probability measure P under a given projection π. It asserts that the measure of each atomic triple event times the blanket marginal equals the internal-blanket marginal times the blanket-external marginal. Information theorists modeling free-energy principle Markov blankets cite it as the precise hypothesis for conditional independence. The definition consists of a direct universal quantification over the four event sets defined in the same module.
Claim. Let $P$ be a probability measure on space $Ω$ and let $π$ be a blanket projection partitioning $Ω$ into internal, blanket, and external coordinates. Then $P$ satisfies ledger-boundary sparsity when, for all coordinate values $i$, $b$, $e$, $P(π^{-1}(i,b,e)) · P(π^{-1}(b)) = P(π^{-1}(i,b)) · P(π^{-1}(b,e))$.
background
The module replaces predicate-based statements with explicit measure factorization over ProbabilityMeasure. BlanketProjection is the structure supplying the three measurable maps that coarse-grain $Ω$ into the FEP partition. The four event sets atomSet, internalBlanketSet, blanketSet, and blanketExternalSet are the preimages under these maps of fixed coordinate tuples, exactly as defined in the sibling declarations.
proof idea
As a definition the body is the explicit universal statement of the product equality. No lemmas or tactics are invoked; the four event sets from the same module are substituted directly into the measure product.
why it matters
It supplies the hypothesis for ledger_sparsity_implies_measure_condIndep, which concludes CondIndepGivenBlanket by exact application, and appears inside the NESSMeasureCert structure as the premise for both conditional independence and the conditional product form. In the Recognition framework it furnishes the information-theoretic interface for the Markov blanket condition in NESS models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.