DecEventSpace
plain-language theorem explainer
DecEventSpace equips any EventSpace with decidable equality on its events. Workers on constructive recognition models cite it when they must compute whether two observable outcomes coincide. The declaration is a direct class extension of EventSpace that adds only the DecidableEq instance.
Claim. A type $E$ is a DecEventSpace when it is an EventSpace (hence contains at least two distinct events) and equality on $E$ is decidable.
background
Recognition Geometry derives space from the structure of recognition maps rather than taking it as primitive. The module therefore begins with recognizers and events; an EventSpace is simply a type whose elements are observable outcomes such as detector clicks or template matches, required only to be nontrivial. The supplied sibling definition states the nontriviality axiom explicitly: there exist distinct $e_1, e_2 : E$ with $e_1 ≠ e_2$.
proof idea
The declaration is a class definition that extends EventSpace E by the single field decEq : DecidableEq E. No lemmas are applied; the construction is purely syntactic and inherits the parent axioms without further proof.
why it matters
DecEventSpace supplies the decidability needed for any later constructive reasoning inside Recognition Geometry. It sits immediately after the EventSpace class and before the RecognitionTriple and core_status declarations in the same module. The surrounding text replaces vacuous existence statements with constructive witnesses, consistent with Axiom RG0 of nonempty configuration space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.