RecognitionTriple
plain-language theorem explainer
RecognitionTriple packages a configuration space with an event space as the primitive object in recognition geometry. Researchers deriving space from recognition processes cite this bundle as the entry point for the framework. The declaration is introduced by direct structure definition that assembles the two space axioms.
Claim. A recognition triple consists of a type $C$ equipped with a configuration space structure (nonempty type of world states) together with a type $E$ equipped with an event space structure (type of observable outcomes containing at least two distinct elements).
background
Recognition geometry treats space as emergent from recognizers and events rather than as a primitive manifold. A configuration space is a nonempty type representing possible states of the world; recognizers receive only events derived from those states. An event space is a type of observable outcomes required to contain at least two distinct elements so that recognition is nontrivial.
proof idea
The declaration is a direct structure definition requiring four fields: the configuration type, the event type, an instance of the configuration space structure, and an instance of the event space structure. No lemmas or tactics are invoked; the construct simply bundles the two space axioms for downstream use.
why it matters
This structure supplies the basic object of recognition geometry and feeds directly into the module status definition that records satisfaction of the nonempty and nontriviality axioms. It implements the local setting in which geometry arises from recognition maps, providing the foundation for later steps that recover the eight-tick octave and three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.