Information Nessconditional Independence Measure Ledger Sparsity Implies Measure

The sparsity condition

Conditional independence is a standard idea in probability. Three random variables are conditionally independent given a fourth when, once you know the fourth, learning one of the three tells you nothing extra about the others. In symbols, P(I, E | B) = P(I | B) P(E | B). The Recognition Science framework works with a finite, event-level version of this idea, written without division so that it stays valid even when probabilities are zero.

The framework's library of machine-checked theorems defines a ledger, a discrete record of events, through a projection that assigns each state of a system three coarse-grained coordinates: internal, blanket, and external. The blanket coordinate is the boundary that separates the internal from the external. The theorem ledger_sparsity_implies_measure_condIndep proves that a condition called ledger-boundary sparsity is exactly the same as conditional independence. That condition says the probability of the joint event, multiplied by the probability of the blanket event, equals the product of the two partial joint events. The proof is immediate: the theorem simply identifies the sparsity condition with the definition of conditional independence.

The statement is a formal equivalence, not a discovery about the physical world. It does not claim that real systems satisfy the sparsity condition. It does not derive the condition from a deeper recognition-field generator. The docstring says that such a derivation is later work; here the condition is exactly the hypothesis needed. The theorem is a bridge between two ways of writing the same mathematical fact.

In Recognition Science, this equivalence matters because it gives a concrete, checkable form to the Markov blanket condition used in the free energy principle. The blanket is the boundary; conditional independence is what makes the boundary a genuine separation. The theorem says that if a measure has the sparsity property, then the blanket does its job. It is a small but load-bearing link in the framework's account of how an internal model can be insulated from its external causes.

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 theorem does not claim that any real system satisfies the sparsity condition. The theorem does not derive the sparsity condition from a deeper recognition-field generator. The theorem does not establish a new mathematical fact beyond the equivalence of two definitions.

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: