EventSpace

formal source

  43/-- An event space is a type of observable outcomes.
  44    Events are things like "the needle points this direction,"
  45    "the detector clicks," or "the image matches this template." -/
  46class EventSpace (E : Type*) where
  47  /-- The event space has at least two distinct events
  48      (otherwise recognition is trivial) -/
  49  nontrivial : ∃ e₁ e₂ : E, e₁ ≠ e₂
  50
  51/-- An event space with decidable equality -/
  52class DecEventSpace (E : Type*) extends EventSpace E where
  53  /-- Decidable equality on events -/
  54  decEq : DecidableEq E
  55
  56attribute [instance] DecEventSpace.decEq
  57
  58/-! ## Basic Properties -/
  59
  60/-- **THEOREM**: A configuration space has at least one element.
  61    Replaces the vacuous `∃ c : C, True` with a constructive witness. -/
  62theorem config_exists (C : Type*) [cs : ConfigSpace C] : ∃ c : C, c = ConfigSpace.witness C :=
  63  ⟨ConfigSpace.witness C, rfl⟩
  64
  65/-- An event space has at least two distinct elements -/
  66theorem event_nontrivial (E : Type*) [EventSpace E] : ∃ e₁ e₂ : E, e₁ ≠ e₂ :=
  67  EventSpace.nontrivial
  68
  69/-! ## Recognition Triple -/
  70
  71/-- A recognition triple bundles a configuration space, event space,
  72    and the implicit structure connecting them. This is the basic
  73    object of study in recognition geometry. -/
  74structure RecognitionTriple where
  75  /-- The type of configurations -/
  76  Config : Type*