separating_singleton_cells

formal source

  63    exact hc
  64
  65/-- If a recognizer separates, every resolution cell is a singleton. -/
  66theorem separating_singleton_cells (r : Recognizer C E) (h : IsSeparating r) (c : C) :
  67    ResolutionCell r c = {c} := by
  68  ext x
  69  simp only [ResolutionCell, Set.mem_setOf_eq, Set.mem_singleton_iff]
  70  constructor
  71  · intro hx; exact h hx
  72  · intro hx; subst hx; rfl
  73
  74/-! ## Two-Recognizer Separation -/
  75
  76/-- Two recognizers together separate if their composite distinguishes all configs. -/
  77def PairSeparates {E₁ E₂ : Type*} [EventSpace E₁] [EventSpace E₂]
  78    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) : Prop :=
  79  IsSeparating (r₁ ⊗ r₂)
  80
  81/-- Pair separation is equivalent to: same (e₁, e₂) implies same config. -/
  82theorem pairSeparates_iff {E₁ E₂ : Type*} [EventSpace E₁] [EventSpace E₂]
  83    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
  84    PairSeparates r₁ r₂ ↔
  85      ∀ c₁ c₂, (r₁.R c₁ = r₁.R c₂ ∧ r₂.R c₁ = r₂.R c₂) → c₁ = c₂ := by
  86  simp only [PairSeparates, IsSeparating, Function.Injective, composite_R_eq,
  87             Prod.mk.injEq]
  88
  89/-! ## Independence -/
  90
  91/-- Two recognizers are **independent** if each provides information the other doesn't.
  92    This means: ∃ configs distinguished by r₁ but not r₂, and vice versa. -/
  93def IndependentRecognizers {E₁ E₂ : Type*} [EventSpace E₁] [EventSpace E₂]
  94    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) : Prop :=
  95  (∃ c₁ c₂, r₁.R c₁ ≠ r₁.R c₂ ∧ r₂.R c₁ = r₂.R c₂) ∧
  96  (∃ c₁ c₂, r₁.R c₁ = r₁.R c₂ ∧ r₂.R c₁ ≠ r₂.R c₂)