EventSpace
plain-language theorem explainer
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.
Claim. An 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.