nessMeasureCert_holds
plain-language theorem explainer
The theorem certifies that the NESSMeasureCert structure is inhabited by assembling two prior results on conditional independence for probability measures. Researchers formalizing the free-energy principle in measure-theoretic terms would cite it to close the blanket-factorization step. The proof is a direct term-mode construction that supplies the conditional_independence field from the sparsity implication and the conditional_product field from the event-level product identity.
Claim. The NESS measure certificate holds: for any probability measure $P$ on a measurable space and any blanket projection $π$, ledger boundary sparsity of $P$ with respect to $π$ implies conditional independence of the internal and external variables given the blanket, and conditional independence implies the product identity $P(I=i,B=b,E=e)·P(B=b)=P(I=i,B=b)·P(B=b,E=e)$ for all events.
background
The module supplies an explicit probability-factorization statement that replaces an earlier True-predicate surface. Conditional independence is defined via the blanket factorization $P(I=i,B=b,E=e)·P(B=b)=P(I=i,B=b)·P(B=b,E=e)$, which is the finite-event form of the FEP Markov-blanket condition. LedgerBoundarySparsity is the hypothesis that the ledger boundary is sparse enough to enforce this factorization; CondIndepGivenBlanket is the resulting independence predicate. The upstream theorem ledger_sparsity_implies_measure_condIndep states that LedgerBoundarySparsity P π directly yields CondIndepGivenBlanket P π. The upstream theorem conditional_product_form supplies the multiplication identity that avoids division side-conditions in ENNReal.
proof idea
The proof is a one-line term that constructs the NESSMeasureCert structure. It populates the conditional_independence field by applying ledger_sparsity_implies_measure_condIndep and the conditional_product field by applying conditional_product_form. No tactics are used; the term simply projects the two required fields from the already-proved siblings.
why it matters
This declaration supplies the top-level certificate that the measure-theoretic NESS conditional-independence statement is inhabited. It closes the explicit factorization step described in the module documentation, replacing an earlier predicate-only formulation. In the Recognition Science setting it anchors the information-theoretic layer that feeds into the forcing chain and the phi-ladder mass formulas by guaranteeing the required conditional-independence property over probability measures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.