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