EventSpace
plain-language theorem explainer
EventSpace is the class of types E serving as observable outcomes in recognition geometry, requiring at least two distinct events. Researchers building recognition triples or deriving dimension from independent recognizers cite this definition. The declaration is a direct class definition encoding the single nontriviality field with no lemmas or tactics.
Claim. An event space is a type $E$ such that there exist distinct $e_1, e_2$ in $E$.
background
Recognition Geometry treats recognizers and events as primitive, with space emerging from recognition maps rather than the reverse. The module opens with axiom RG0 asserting a nonempty configuration space and pairs it with EventSpace for observable outcomes such as detector clicks or matched templates. This class supplies the minimal nontriviality condition on events.
proof idea
The declaration is a class definition that directly introduces the EventSpace structure and its nontrivial field. No lemmas are applied and no tactics are used.
why it matters
EventSpace supplies the event component for RecognitionTriple and is extended by DecEventSpace; it is invoked in core_status and in the Dimension module for IndependentRecognizers and pair separation. It encodes the non-triviality needed for recognition geometry to proceed beyond the RG0 configuration-space axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.