NESSMeasureCert
plain-language theorem explainer
NESSMeasureCert packages the implication from ledger-boundary sparsity to blanket conditional independence together with the explicit product factorization for a probability measure under a blanket projection. Researchers modeling non-equilibrium steady states or free-energy principle Markov blankets in physics would cite this structure when certifying measure factorization. It is introduced as a direct record definition with no computational steps or lemmas applied.
Claim. Let $P$ be a probability measure on a measurable space $Ω$ and let $π$ be a blanket projection of $Ω$ into internal, blanket and external components. Then NESSMeasureCert holds when ledger-boundary sparsity of $P$ under $π$ implies the blanket factorization (conditional independence of internal and external given the blanket) and, whenever the factorization holds, the equality $P( atomSet(π,i,b,e) ) ⋅ P( blanketSet(π,b) ) = P( internalBlanketSet(π,i,b) ) ⋅ P( blanketExternalSet(π,b,e) )$ is satisfied for all $i,b,e$.
background
The module replaces predicate-based theorems with an explicit probability-factorization statement over ProbabilityMeasure. BlanketProjection is the structure supplying the three measurable maps internal : Ω → Internal, blanket : Ω → Blanket and external : Ω → External that realize the FEP partition. LedgerBoundarySparsity asserts that the measure obeys the blanket factorization for every triple of values; CondIndepGivenBlanket is the identical factorization property viewed as conditional independence. The local setting is the finite-event form of the Markov blanket condition: P(I=i,B=b,E=e)⋅P(B=b)=P(I=i,B=b)⋅P(B=b,E=e).
proof idea
As a structure definition NESSMeasureCert simply records the two required properties. The first field is the implication LedgerBoundarySparsity P π → CondIndepGivenBlanket P π; the second field is the product equality under the hypothesis that CondIndepGivenBlanket holds. No tactics or upstream lemmas are invoked inside the definition itself.
why it matters
NESSMeasureCert supplies the explicit certificate consumed by the downstream theorem nessMeasureCert_holds, which constructs an instance via ledger_sparsity_implies_measure_condIndep and conditional_product_form. It therefore anchors the measure-theoretic statement of the FEP Markov blanket condition inside the Recognition Science information layer, preparing the ground for later derivation of sparsity from a recognition-field generator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.