recognizerSetoid
plain-language theorem explainer
recognizerSetoid supplies the equivalence relation on configuration space C induced by a recognizer r, equating inputs that map to the same event under the RG3 axiom. Researchers formalizing the refinement lattice and Zorn applications in Recognition Geometry cite it when denoting kernels of recognizers. The definition is a direct one-line alias to the indistinguishableSetoid construction.
Claim. Let $r : C → E$ be a recognizer. The induced setoid on $C$ is the equivalence relation under which $c_1 ∼ c_2$ if and only if $r(c_1) = r(c_2)$.
background
The module formalizes the refinement lattice of Recognition Geometry by connecting Zorn's Lemma to the RG3 (Indistinguishability) axiom. Each recognizer induces an equivalence relation on configuration space C, with the collection of such relations partially ordered by refinement; composition of recognizers corresponds to the meet operation. recognizerSetoid is introduced as a convenient synonym for the setoid whose relation is given by Indistinguishable r and whose equivalence proof is supplied by indistinguishable_equivalence r.
proof idea
one-line wrapper that applies indistinguishableSetoid r
why it matters
It forms the basic object for the lattice of recognizer-induced setoids, directly feeding composite_setoid_iff, composite_setoid_is_inf, composite_setoid_le_left, composite_setoid_le_right, IsRecognizerInduced, maximal_unique_setoid, and recognizer_meet_semilattice. The module states that these results formalize Theorem 4.1 and Theorem 5.1 of the paper on Maximal Recognizers and Zorn's Lemma in Recognition Geometry, linking to the RG3 axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.