IndisputableMonolith.Information.NESSConditionalIndependenceMeasure

   1import Mathlib
   2import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
   3
   4/-!
   5# NESS Conditional Independence, Measure-Theoretic Factorization
   6
   7This module replaces the old `True`-predicate theorem surface with an explicit
   8probability-factorization statement over a `ProbabilityMeasure`.
   9
  10Mathlib in this checkout exposes `ProbabilityMeasure` and `condExp`, but does
  11not expose a stable `MeasureTheory.CondIndep` / `IndepFun` API under those
  12names. We therefore define conditional independence by the standard blanket
  13factorization:
  14
  15  P(I=i, B=b, E=e) · P(B=b) = P(I=i, B=b) · P(B=b, E=e).
  16
  17This is equivalent to `P(I=i, E=e | B=b) = P(I=i | B=b) P(E=e | B=b)` when
  18`P(B=b) ≠ 0`. It is the finite-valued event-level form of the FEP Markov
  19blanket condition.
  20-/
  21
  22namespace IndisputableMonolith.Information.NESSConditionalIndependenceMeasure
  23
  24open MeasureTheory
  25
  26noncomputable section
  27
  28variable {Ω Internal Blanket External : Type*} [MeasurableSpace Ω]
  29
  30/-- A measurable projection of a state space into the FEP partition. -/
  31structure BlanketProjection (Ω Internal Blanket External : Type*) where
  32  internal : Ω → Internal
  33  blanket : Ω → Blanket
  34  external : Ω → External
  35
  36/-- Event where all three coarse-grained coordinates take specified values. -/
  37def atomSet (π : BlanketProjection Ω Internal Blanket External)
  38    (i : Internal) (b : Blanket) (e : External) : Set Ω :=
  39  {ω | π.internal ω = i ∧ π.blanket ω = b ∧ π.external ω = e}
  40
  41/-- Event where internal and blanket coordinates take specified values. -/
  42def internalBlanketSet (π : BlanketProjection Ω Internal Blanket External)
  43    (i : Internal) (b : Blanket) : Set Ω :=
  44  {ω | π.internal ω = i ∧ π.blanket ω = b}
  45
  46/-- Event where blanket and external coordinates take specified values. -/
  47def blanketExternalSet (π : BlanketProjection Ω Internal Blanket External)
  48    (b : Blanket) (e : External) : Set Ω :=
  49  {ω | π.blanket ω = b ∧ π.external ω = e}
  50
  51/-- Blanket event. -/
  52def blanketSet (π : BlanketProjection Ω Internal Blanket External)
  53    (b : Blanket) : Set Ω :=
  54  {ω | π.blanket ω = b}
  55
  56/-- Measure-theoretic conditional independence as blanket factorization. -/
  57def CondIndepGivenBlanket
  58    (P : ProbabilityMeasure Ω)
  59    (π : BlanketProjection Ω Internal Blanket External) : Prop :=
  60  ∀ (i : Internal) (b : Blanket) (e : External),
  61    (P : Measure Ω) (atomSet π i b e) * (P : Measure Ω) (blanketSet π b) =
  62    (P : Measure Ω) (internalBlanketSet π i b) *
  63      (P : Measure Ω) (blanketExternalSet π b e)
  64
  65/-- Ledger-boundary sparsity on the measure surface: the measure has the
  66blanket factorization. In later work this can be derived from a concrete
  67recognition-field generator; here it is the exact hypothesis needed for
  68conditional independence. -/
  69def LedgerBoundarySparsity
  70    (P : ProbabilityMeasure Ω)
  71    (π : BlanketProjection Ω Internal Blanket External) : Prop :=
  72  ∀ (i : Internal) (b : Blanket) (e : External),
  73    (P : Measure Ω) (atomSet π i b e) * (P : Measure Ω) (blanketSet π b) =
  74    (P : Measure Ω) (internalBlanketSet π i b) *
  75      (P : Measure Ω) (blanketExternalSet π b e)
  76
  77theorem ledger_sparsity_implies_measure_condIndep
  78    (P : ProbabilityMeasure Ω)
  79    (π : BlanketProjection Ω Internal Blanket External)
  80    (h : LedgerBoundarySparsity P π) :
  81    CondIndepGivenBlanket P π := by
  82  exact h
  83
  84/-- Product form of conditional independence. This is the event-level
  85conditional-independence identity, kept in multiplication form to avoid
  86division side conditions in `ENNReal`. -/
  87theorem conditional_product_form
  88    (P : ProbabilityMeasure Ω)
  89    (π : BlanketProjection Ω Internal Blanket External)
  90    (h : CondIndepGivenBlanket P π)
  91    (i : Internal) (b : Blanket) (e : External) :
  92    (P : Measure Ω) (atomSet π i b e) * (P : Measure Ω) (blanketSet π b) =
  93    (P : Measure Ω) (internalBlanketSet π i b) *
  94      (P : Measure Ω) (blanketExternalSet π b e) := by
  95  exact h i b e
  96
  97structure NESSMeasureCert where
  98  conditional_independence :
  99    ∀ {Ω I B E : Type*} [MeasurableSpace Ω]
 100      (P : ProbabilityMeasure Ω) (π : BlanketProjection Ω I B E),
 101      LedgerBoundarySparsity P π → CondIndepGivenBlanket P π
 102  conditional_product :
 103    ∀ {Ω I B E : Type*} [MeasurableSpace Ω]
 104      (P : ProbabilityMeasure Ω) (π : BlanketProjection Ω I B E)
 105      (h : CondIndepGivenBlanket P π)
 106      (i : I) (b : B) (e : E),
 107      (P : Measure Ω) (atomSet π i b e) * (P : Measure Ω) (blanketSet π b) =
 108      (P : Measure Ω) (internalBlanketSet π i b) *
 109        (P : Measure Ω) (blanketExternalSet π b e)
 110
 111theorem nessMeasureCert_holds : NESSMeasureCert :=
 112{ conditional_independence := @ledger_sparsity_implies_measure_condIndep
 113  conditional_product := @conditional_product_form }
 114
 115end
 116
 117end IndisputableMonolith.Information.NESSConditionalIndependenceMeasure
 118