recognizerSetoid_iff
plain-language theorem explainer
The theorem states that a recognizer r from configurations C to E induces a setoid whose relation holds between c1 and c2 exactly when r maps them to the same output. Researchers formalizing the refinement lattice of recognizers under the RG3 indistinguishability axiom cite this equivalence to connect the setoid to the underlying map. The proof is a direct one-line term applying reflexivity of the biconditional.
Claim. Let $r : C → E$ be a recognizer. For configurations $c_1, c_2 ∈ C$, the equivalence relation induced by the recognizer setoid holds between $c_1$ and $c_2$ if and only if $r(c_1) = r(c_2)$.
background
Recognition Geometry equips each recognizer with an equivalence relation on configuration space C via the RG3 indistinguishability axiom. The recognizerSetoid is defined as this induced setoid (synonymous with indistinguishableSetoid), and the module orders such setoids by refinement, with composition acting as the meet operation in the lattice. The local setting formalizes Theorems 4.1 and 5.1 on maximal recognizers via Zorn's Lemma.
proof idea
The proof is a one-line term that applies reflexivity of logical equivalence (Iff.rfl) to confirm the setoid relation matches equality of recognizer outputs by definition.
why it matters
This unfolding anchors the partial order on recognizer-induced setoids and supports the composite_setoid lemmas showing that composition refines both components. It fills the explicit link required for the refinement preorder and the application of Zorn's Lemma to guarantee a finest recognizer, as stated in the module's reference to the paper on Maximal Recognizers and Zorn's Lemma in Recognition Geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.