pith. machine review for the scientific record. sign in
class definition def or abbrev high

EventSpace

show as:
view Lean formalization →

EventSpace is a type class on a type E of observable outcomes that requires at least two distinct elements. Recognition-geometry researchers cite it when constructing the basic objects for detectors and recognition maps. The declaration is a direct class definition that imposes only the single nontriviality condition.

claimAn event space is a type $E$ such that there exist distinct $e_1,e_2$ in $E$ with $e_1$ different from $e_2$.

background

Recognition Geometry treats space as emergent from recognizers and events rather than as a primitive. The module opens with axiom RG0 asserting a nonempty configuration space and then introduces EventSpace as the corresponding structure for observable outcomes. Events are concrete detections such as needle positions or detector clicks. The class requires only that the event type be nontrivial, i.e., contain at least two distinct members.

proof idea

The declaration is a direct class definition with an empty proof body. It simply records the field nontrivial : exists e1 e2 : E, e1 != e2.

why it matters in Recognition Science

EventSpace supplies the event component of the RecognitionTriple structure and is extended by DecEventSpace. It is used by core_status to certify the module's foundational definitions and by the Dimension module to state IndependentRecognizers and pair-separation properties. The definition therefore closes the basic setup that lets recognition maps generate geometry, consistent with the module's reversal of the usual geometric order.

scope and limits

formal statement (Lean)

  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 -/

used by (19)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.