Recognizer

formal source

  62from a configuration space `𝒞` onto an event space `ℰ`. The fact that
  63it is many-to-one is essential; it is what generates the
  64indistinguishability quotient. -/
  65structure Recognizer (𝒞 ℰ : Type*) where
  66  observe : 𝒞 → ℰ
  67  surjective : Function.Surjective observe
  68
  69/-! ## The Indistinguishability Quotient -/
  70
  71/-- Two configurations are observationally indistinguishable under a
  72recognizer if the recognizer maps them to the same event. -/
  73def Recognizer.kernel {𝒞 ℰ : Type*} (r : Recognizer 𝒞 ℰ) (x y : 𝒞) : Prop :=
  74  r.observe x = r.observe y
  75
  76/-- The kernel of a recognizer is an equivalence relation. -/
  77theorem Recognizer.kernel_is_equivalence {𝒞 ℰ : Type*} (r : Recognizer 𝒞 ℰ) :
  78    Equivalence (r.kernel) :=
  79  ⟨fun _ => rfl, fun h => h.symm, fun h₁ h₂ => h₁.trans h₂⟩
  80
  81/-! ## The Recognizer-Induced Cost on the Event Space -/
  82
  83/-- The cost of distinguishing two events: zero when they are the same
  84event, a positive weight otherwise. This is exactly the equality-induced
  85cost of `PrimitiveDistinction` applied to the event space `ℰ`. -/
  86noncomputable def Recognizer.cost {𝒞 ℰ : Type*} (_r : Recognizer 𝒞 ℰ)
  87    (weight : ℝ) : ℰ → ℰ → ℝ :=
  88  equalityCost ℰ weight
  89
  90/-! ## The Three Definitional Aristotelian Conditions
  91
  92A recognizer induces (L1), (L2), and (L3a) on its event space
  93automatically, by `PrimitiveDistinction`. No further structural choice
  94is required.
  95-/