Recognizer
plain-language theorem explainer
A recognizer is a surjective map from configurations to events whose many-to-one character produces an indistinguishability kernel on the event space. Researchers deriving Aristotelian logic from recognition geometry cite this structure as the geometric starting point that supplies the primitive observer. The definition is given directly by the type signature together with surjectivity; all subsequent cost and equivalence properties follow from equality on the codomain.
Claim. Let $C$ be a configuration space and $E$ an event space. A recognizer is a surjective function $o:C→E$.
background
Recognition Science treats a recognizer as the geometric primitive that maps configurations onto events, thereby inducing an indistinguishability quotient. The module shows that any such surjection automatically equips the event space with the equality-induced cost of PrimitiveDistinction, which in turn yields the three definitional Aristotelian conditions. Upstream results from ObserverFromRecognition supply the primitive observer once the event space contains at least two distinct events; MagnitudeOfMismatch supplies single-valuedness of the induced cost.
proof idea
The structure is introduced by two fields: the observe map and a surjectivity witness. The kernel is defined pointwise by equality of observations and proved an equivalence by the reflexivity, symmetry and transitivity of equality. The cost is set equal to equalityCost; the identity, non-contradiction and totality theorems are one-line applications of the corresponding lemmas from the equality cost. The primitive-observer theorem uses the non-triviality hypothesis to construct the required interface.
why it matters
This definition supplies the geometric input to the Recognition-Geometry-to-Logic unification, feeding the claim that a recognizer is the primitive observer. It realizes the module's statement that (L1), (L2) and (L3a) arise for free from the type signature plus equality, reducing the remaining content of the Aristotelian framework to a single named compositional axiom. In the broader T0-T8 chain it corresponds to the observer step that forces the logical realization without further assumptions on dimensions or constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.