recognizerSetoid_iff
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of maximal recognizers.
- Does not assume structure on the codomain E beyond being a type.
- Does not address transitivity or reflexivity of the setoid beyond the relation unfolding.
- Does not connect to the forcing chain T0-T8 or phi-ladder constants.
formal statement (Lean)
43theorem recognizerSetoid_iff {E : Type*} (r : Recognizer C E) (c₁ c₂ : C) :
44 (recognizerSetoid r).Rel c₁ c₂ ↔ r.R c₁ = r.R c₂ :=
proof body
Term-mode proof.
45 Iff.rfl
46
47/-! ## Section 2: Composition Refines Both Components
48
49In Mathlib's ordering on `Setoid C`, we have `s ≤ t` iff `∀ a b, s.Rel a b → t.Rel a b`.
50This means s ≤ t when s is *at least as fine as* t (s-related implies t-related, so
51t has at least as many related pairs, i.e., t is coarser). The composite recognizer
52R₁ ⊗ R₂ is finer than both R₁ and R₂, so its setoid is ≤ both component setoids. -/
53
54/-- The composite setoid relates c₁, c₂ iff both components do. -/