IsRecognizerInduced
plain-language theorem explainer
A setoid s on configuration space C is recognizer-induced when it equals the equivalence relation produced by some recognizer r to a codomain E. Researchers applying Zorn's Lemma to the refinement lattice of recognition geometry cite this predicate to isolate setoids that arise from actual recognizers. The definition is realized directly as an existential quantifier over recognizers and equality of their induced setoids.
Claim. A setoid $s$ on configuration space $C$ is recognizer-induced if there exists a type $E$ and a recognizer $r : C → E$ such that the setoid induced by $r$ equals $s$.
background
Recognition Geometry starts from the RG3 indistinguishability axiom: each recognizer $r : C → E$ partitions configuration space $C$ into equivalence classes. The module studies the resulting collection of setoids ordered by refinement, with composition of recognizers corresponding to the infimum in the complete lattice of setoids. recognizerSetoid is the setoid induced by a recognizer (synonym for indistinguishableSetoid). The definition isolates precisely those setoids that arise from some recognizer.
proof idea
The definition is a direct existential statement: $s$ is recognizer-induced precisely when there exist $E$ and $r$ such that recognizerSetoid $r = s$. No lemmas are invoked; the predicate is introduced by abbreviation to label the objects of the refinement partial order.
why it matters
This definition supplies the predicate for the refinement lattice on which Zorn's Lemma is applied to guarantee a maximal recognizer setoid. It directly supports the module's main results on maximal elements and the infimum property of composite setoids, formalizing Theorem 4.1 and Theorem 5.1 of the paper on Maximal Recognizers and Zorn's Lemma in Recognition Geometry. It anchors the connection between recognizers and the complete lattice of setoids used throughout the RG3 development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.