RecognitionPreservingMap

formal source

  41
  42/-- A recognition-preserving map is a transformation that preserves events.
  43    This is the fundamental symmetry concept in recognition geometry. -/
  44structure RecognitionPreservingMap (r : Recognizer C E) where
  45  /-- The underlying transformation -/
  46  toFun : C → C
  47  /-- The transformation preserves recognition events -/
  48  preserves_event : ∀ c, r.R (toFun c) = r.R c
  49
  50/-- Coercion to function -/
  51instance (r : Recognizer C E) : CoeFun (RecognitionPreservingMap r) (fun _ => C → C) where
  52  coe := RecognitionPreservingMap.toFun
  53
  54/-! ## Basic Properties -/
  55
  56variable {r : Recognizer C E}
  57
  58/-- A recognition-preserving map preserves indistinguishability -/
  59theorem symmetry_preserves_indistinguishable (T : RecognitionPreservingMap r)
  60    {c₁ c₂ : C} (h : Indistinguishable r c₁ c₂) :
  61    Indistinguishable r (T c₁) (T c₂) := by
  62  unfold Indistinguishable at *
  63  rw [T.preserves_event, T.preserves_event]
  64  exact h
  65
  66/-- A recognition-preserving map preserves distinguishability -/
  67theorem symmetry_preserves_distinguishable (T : RecognitionPreservingMap r)
  68    {c₁ c₂ : C} (h : Distinguishable r c₁ c₂) :
  69    Distinguishable r (T c₁) (T c₂) := by
  70  unfold Distinguishable at *
  71  rw [T.preserves_event, T.preserves_event]
  72  exact h
  73
  74/-- A recognition-preserving map maps resolution cells to resolution cells -/