discreteRecognizer
plain-language theorem explainer
The discrete recognizer on a finite set of n elements with n at least 2 is the structure whose recognition map is the identity, so that every pair of distinct points remains distinguishable. Researchers constructing concrete recognition geometries cite this as the base case where the induced quotient space recovers the original set exactly. The definition is a direct construction that assigns the identity function to the recognizer map and checks the nontriviality condition by naming two distinct elements.
Claim. For a natural number $n$ with $n$ at least 2, the discrete recognizer on the finite set with $n$ elements is the recognizer whose recognition map $R$ is the identity function on that set.
background
Recognition geometry equips a configuration space with a map that induces an indistinguishability relation, turning the space into a recognizer whose quotient encodes the distinguishable classes. The module supplies concrete examples, beginning with the discrete case on finite sets where every configuration is kept separate. In this setting the recognizer map is required only to be nontrivial, meaning at least two distinct points exist.
proof idea
The definition is a direct construction that sets the recognizer component to the identity function. Nontriviality is discharged by exhibiting the elements 0 and 1, which are distinct under the Fin extensionality lemma once $n$ is at least 2.
why it matters
This supplies the base example in which the quotient is isomorphic to the original space, feeding the theorem that indistinguishability coincides with equality and the corollary that every resolution cell is a singleton. It realizes the module insight that discrete recognition yields perfect distinguishability and serves as the zero-defect reference point before sign and magnitude recognizers introduce coarser partitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.