IndisputableMonolith.Information.NESSConditionalIndependenceMeasure
The module defines a measurable projection of a state space into an FEP partition together with supporting sets for conditional independence in NESS settings. Researchers formalizing information measures under the free energy principle would cite these constructions when building blanket-based independence results. The module consists entirely of definitions and supporting lemmas with no central theorem or proof.
claimA measurable projection $\pi$ of a state space into the FEP partition, equipped with blanket sets that certify conditional independence of internal and external variables given the blanket.
background
The module sits in the Information domain and imports only Mathlib and its ProbabilityMeasure library. It introduces the blanket projection together with atomSet, internalBlanketSet, blanketExternalSet, blanketSet, and CondIndepGivenBlanket. These objects formalize the measurable structures needed to express conditional independence given a blanket in a probability space.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The constructions feed the sibling results LedgerBoundarySparsity, ledger_sparsity_implies_measure_condIndep, conditional_product_form, NESSMeasureCert and nessMeasureCert_holds, supplying the measurable projection and independence certificate required for NESS measure validation.
scope and limits
- Does not contain any theorem statements or proofs.
- Does not import Recognition Science forcing-chain or phi-ladder material.
- Does not define numerical constants or mass formulas.