event_nontrivial
Any event space contains at least two distinct events. Recognition-geometry workers cite the result to guarantee that recognition maps remain non-degenerate before constructing triples or applying the composition law. The proof is a one-line term that extracts the nontrivial field from the EventSpace class instance.
claimFor any type $E$ equipped with an EventSpace structure, there exist $e_1, e_2 : E$ such that $e_1 ≠ e_2$.
background
Recognition Geometry treats space as emergent from recognizers and events rather than primitive. The EventSpace class models observable outcomes (needle directions, detector clicks, template matches) and encodes the minimal non-degeneracy condition that at least two distinct events exist. The module opens with axiom RG0 asserting nonempty configuration spaces; the present theorem supplies the parallel non-triviality condition on the event side.
proof idea
The proof is a direct term that applies the nontrivial field of the EventSpace class definition.
why it matters in Recognition Science
The result supplies the non-degeneracy axiom required by RecognitionTriple and downstream geometry constructions. It sits at the base of the recognition framework, ensuring the composition law and the T0–T8 forcing chain operate on distinguishable events rather than a singleton. No open scaffolding remains; the statement is fully discharged by the class field.
scope and limits
- Does not equip the event space with a metric or topology.
- Does not decide equality between concrete events.
- Does not construct explicit physical events or assign probabilities.
- Does not address continuous versus discrete event spaces.
formal statement (Lean)
66theorem event_nontrivial (E : Type*) [EventSpace E] : ∃ e₁ e₂ : E, e₁ ≠ e₂ :=
proof body
Term-mode proof.
67 EventSpace.nontrivial
68
69/-! ## Recognition Triple -/
70
71/-- A recognition triple bundles a configuration space, event space,
72 and the implicit structure connecting them. This is the basic
73 object of study in recognition geometry. -/