conditional_product_form
plain-language theorem explainer
The declaration delivers the multiplicative identity for conditional independence of internal and external events given the blanket, expressed directly on a probability measure. Information theorists and free-energy-principle researchers cite it to certify the Markov-blanket factorization in NESS models without division. The proof is a one-line wrapper that invokes the defining forall of CondIndepGivenBlanket on the supplied indices.
Claim. Let $P$ be a probability measure on state space $Ω$, let $π$ be a blanket projection, and assume the blanket factorization holds. Then for internal coordinate value $i$, blanket value $b$, and external value $e$, $P(ω : π.internal(ω)=i ∧ π.blanket(ω)=b ∧ π.external(ω)=e) · P(ω : π.blanket(ω)=b) = P(ω : π.internal(ω)=i ∧ π.blanket(ω)=b) · P(ω : π.blanket(ω)=b ∧ π.external(ω)=e)$.
background
The module replaces predicate-based statements with an explicit factorization over ProbabilityMeasure because Mathlib lacks a stable CondIndep API at this level. BlanketProjection is the structure supplying the three measurable maps that partition states into internal, blanket, and external types. The auxiliary sets atomSet, internalBlanketSet, blanketSet, and blanketExternalSet are the preimages of concrete value tuples under these maps. CondIndepGivenBlanket is defined as the proposition that the measure satisfies the product identity for every such tuple, which is equivalent to the conditional-probability form whenever the blanket has positive measure.
proof idea
The proof is a one-line wrapper that applies the assumption h : CondIndepGivenBlanket P π directly to the parameters i, b, e.
why it matters
This theorem populates the conditional_product field of the NESSMeasureCert record constructed in nessMeasureCert_holds. It encodes the event-level Markov-blanket condition required by the free-energy principle and supplies the measure-theoretic factorization used downstream to certify NESS measures. In the Recognition Science setting it supports the information layer that feeds the phi-ladder and eight-tick dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.