Information Nessconditional Independence Measure

Conditional independence as a factorization

Conditional independence is a standard probability concept. Three events A, B, and C are conditionally independent given B when, once you know B, learning whether A happened gives you no further information about whether C happened. The usual notation is P(A and C | B) = P(A | B) · P(C | B). The definition only becomes interesting when the events are not single outcomes but coarse-grained regions of a larger state space.

The classical setting for this idea is a Markov blanket. In a system with internal states, external states, and a boundary between them, the boundary states shield the internal states from the external ones. Conditional independence is the mathematical expression of that shielding: internal and external states are independent once the boundary is fixed. This is the structure that the formalization captures.

The formalization defines a BlanketProjection, a triple of functions that assign to each point of a state space its internal, blanket, and external coordinates. It then defines CondIndepGivenBlanket, the property that the probability of any combination of internal, blanket, and external values factors through the blanket. The definition uses a multiplication form, P(I=i, B=b, E=e) · P(B=b) = P(I=i, B=b) · P(B=b, E=e), which avoids division side conditions and works even when probabilities are zero.

The formalization also defines LedgerBoundarySparsity, a name for the same factorization viewed as a property of a probability measure. The central theorem, ledger_sparsity_implies_measure_condIndep, proves that ledger boundary sparsity implies conditional independence. The proof is immediate: the two definitions are identical. The real contribution is making the identification explicit, so that a measure with the blanket factorization is certified as satisfying conditional independence.

In Recognition Science, this is groundwork. The framework's long-term program is to derive the blanket factorization from a concrete recognition-field generator, a physical mechanism that would explain why the ledger's boundary is sparse. That derivation is not yet in the library. What is established now is the exact hypothesis: conditional independence is the measure-theoretic statement that the boundary between internal and external states is informationally sealed.

/-- Measure-theoretic conditional independence as blanket factorization. -/
def CondIndepGivenBlanket
    (P : ProbabilityMeasure Ω)
    (π : BlanketProjection Ω Internal Blanket External) : Prop :=
  ∀ (i : Internal) (b : Blanket) (e : External),
    (P : Measure Ω) (atomSet π i b e) * (P : Measure Ω) (blanketSet π b) =
    (P : Measure Ω) (internalBlanketSet π i b) *
      (P : Measure Ω) (blanketExternalSet π b e)

/-- Ledger-boundary sparsity on the measure surface: the measure has the
blanket factorization. In later work this can be derived from a concrete
recognition-field generator; here it is the exact hypothesis needed for
conditional independence. -/
def LedgerBoundarySparsity
    (P : ProbabilityMeasure Ω)
    (π : BlanketProjection Ω Internal Blanket External) : Prop :=
  ∀ (i : Internal) (b : Blanket) (e : External),
    (P : Measure Ω) (atomSet π i b e) * (P : Measure Ω) (blanketSet π b) =
    (P : Measure Ω) (internalBlanketSet π i b) *
      (P : Measure Ω) (blanketExternalSet π b e)

theorem ledger_sparsity_implies_measure_condIndep
    (P : ProbabilityMeasure Ω)
    (π : BlanketProjection Ω Internal Blanket External)
    (h : LedgerBoundarySparsity P π) :
    CondIndepGivenBlanket P π := by
  exact h

What this page does not claim

The blanket factorization is not yet derived from a recognition-field generator; it is an explicit hypothesis. The module does not define a numerical measure of information content. The theorem does not prove that any actual physical system satisfies conditional independence.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/NESSConditionalIndependenceMeasure.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: