recognizerSetoid
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove reflexivity, symmetry or transitivity of the induced relation.
- Does not fix the cardinality or structure of the event space E.
- Does not relate the setoid to any concrete dimension or forcing-chain step.
- Does not construct an explicit model of a recognizer.
Lean usage
theorem composite_setoid_iff {E₁ E₂ : Type*} (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c₁ c₂ : C) : (recognizerSetoid (r₁ ⊗ r₂)).Rel c₁ c₂ ↔ (recognizerSetoid r₁).Rel c₁ c₂ ∧ (recognizerSetoid r₂).Rel c₁ c₂formal statement (Lean)
39def recognizerSetoid {E : Type*} (r : Recognizer C E) : Setoid C :=
proof body
Definition body.
40 indistinguishableSetoid r
41
42/-- The setoid relation unfolds to R(c₁) = R(c₂). -/