pairSeparates_iff

formal source

  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₂)
  97
  98/-- If recognizers are independent, their composite strictly refines both. -/
  99theorem independent_strict_refines {E₁ E₂ : Type*} [EventSpace E₁] [EventSpace E₂]
 100    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
 101    (h : IndependentRecognizers r₁ r₂) :
 102    ¬IsSeparating r₁ ∧ ¬IsSeparating r₂ →
 103      (∃ c₁ c₂, r₁.R c₁ = r₁.R c₂ ∧ (r₁ ⊗ r₂).R c₁ ≠ (r₁ ⊗ r₂).R c₂) := by
 104  intro ⟨_, _⟩
 105  obtain ⟨⟨_, _, _, _⟩, ⟨c₃, c₄, heq, hne⟩⟩ := h
 106  use c₃, c₄, heq
 107  simp only [composite_R_eq]
 108  intro hcontra
 109  rw [Prod.mk.injEq] at hcontra
 110  exact hne hcontra.2
 111
 112/-! ## Physical Interpretation: Spacetime Dimension -/