DecEventSpace
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not impose any metric, topology, or ordering on events.
- Does not assert that E is finite or countably infinite.
- Does not connect events to the phi-ladder or spectral emergence.
- Does not provide a concrete model or example of an event space.
formal statement (Lean)
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. -/