`Indistinguishable`

definition

show as: view math explainer →

module: IndisputableMonolith.RecogGeom.Indistinguishable
domain: RecogGeom
line: 33 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RecogGeom.Indistinguishable on GitHub at line 33.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  30/-- Two configurations are indistinguishable under a recognizer if they
  31    produce the same event. This is the fundamental equivalence relation
  32    of recognition geometry. -/
  33def Indistinguishable {C E : Type*} (r : Recognizer C E) (c₁ c₂ : C) : Prop :=
  34  r.R c₁ = r.R c₂
  35
  36/-- Notation: c₁ ~[r] c₂ means c₁ and c₂ are indistinguishable under r -/
  37notation:50 c₁ " ~[" r "] " c₂ => Indistinguishable r c₁ c₂
  38
  39/-! ## Equivalence Relation Properties -/
  40
  41variable {C E : Type*} (r : Recognizer C E)
  42
  43/-- Indistinguishability is reflexive -/
  44theorem Indistinguishable.refl (c : C) : c ~[r] c := rfl
  45
  46/-- Indistinguishability is symmetric -/
  47theorem Indistinguishable.symm' {c₁ c₂ : C} (h : c₁ ~[r] c₂) : c₂ ~[r] c₁ :=
  48  Eq.symm h
  49
  50/-- Indistinguishability is transitive -/
  51theorem Indistinguishable.trans {c₁ c₂ c₃ : C}
  52    (h₁ : c₁ ~[r] c₂) (h₂ : c₂ ~[r] c₃) : c₁ ~[r] c₃ :=
  53  Eq.trans h₁ h₂
  54
  55/-- Indistinguishability is an equivalence relation -/
  56theorem indistinguishable_equivalence : Equivalence (Indistinguishable r) where
  57  refl := Indistinguishable.refl r
  58  symm := Indistinguishable.symm' r
  59  trans := Indistinguishable.trans r
  60
  61/-- The indistinguishability setoid -/
  62def indistinguishableSetoid : Setoid C where
  63  r := Indistinguishable r

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.