recognizerSetoid
plain-language theorem explainer
RecognizerSetoid equips configuration space C with the equivalence relation induced by any recognizer r, declaring two configurations equivalent exactly when they map to the same event. Workers on the refinement lattice of recognizers and Zorn's lemma applications cite this alias when manipulating induced setoids in the partial order. It is realized as a direct one-line alias to the indistinguishability setoid construction.
Claim. For a recognizer $r : C → E$, 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
In Recognition Geometry a recognizer is a map from configuration space C to an event space E. RG3 supplies the indistinguishability predicate: two configurations are related precisely when they produce identical events. The module builds the refinement lattice on these induced setoids, with composition of recognizers corresponding to the meet operation in the lattice of equivalences. Upstream, the indistinguishability setoid is constructed by lifting the indistinguishability predicate to a Setoid instance equipped with the standard equivalence proofs.
proof idea
The definition is a one-line wrapper that applies the indistinguishability setoid construction.
why it matters
This supplies the basic object for the refinement lattice, feeding directly into the infimum property of composite setoids, the left and right refinement lemmas, and the uniqueness result for maximal recognizers. It formalizes the setoid induced via RG3 as required by Theorem 4.1 of the paper on Maximal Recognizers and Zorn's Lemma. The alias supports the subsequent application of Zorn's lemma to guarantee existence of finest recognizers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.