IndisputableMonolith.Information.NESSConditionalIndependenceMeasure
The module defines a measurable projection of state spaces into FEP partitions together with blanket sets and conditional independence measures for NESS. Information theorists formalizing Markov blankets in active inference cite these constructions when separating internal and external dynamics. The module supplies the supporting definitions and certificates without internal proofs.
claimA measurable projection $P: X → B$ of a state space $X$ into the FEP partition $B$, with associated blanket sets and the conditional independence relation $X_1 ⊥ X_2 | B$ under the NESS measure.
background
Recognition Science builds information measures on the J-cost functional and the phi-ladder. This module introduces the blanket set as the Markov blanket that separates internal states from external states in the free-energy partition. It imports Mathlib's ProbabilityMeasure to express conditional independence given the blanket and to certify NESSMeasureCert.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module supplies the definitions required by ledger_sparsity_implies_measure_condIndep and nessMeasureCert_holds, which close the information-theoretic step in the forcing chain. It formalizes the conditional independence needed for the eight-tick octave structure.
scope and limits
- Does not derive the projection from J-uniqueness.
- Does not compute numerical values for physical constants.
- Does not address quantum or relativistic extensions.
- Does not prove the NESS certificate for arbitrary measures.