indistinguishableSetoid
plain-language theorem explainer
The definition equips the configuration space C with the setoid whose relation identifies two points precisely when a recognizer maps them to the same event. Workers constructing quotient spaces or resolution cells in recognition geometry cite it to pass from raw configurations to distinguishable events. It is realized as a direct wrapper that installs the Indistinguishable predicate and re-uses the already-verified equivalence proof.
Claim. Let $r$ be a recognizer from configurations $C$ to events $E$. The indistinguishability setoid on $C$ is the setoid whose underlying relation is $c_1 sim_r c_2$ if and only if $r(c_1)=r(c_2)$, together with the standard reflexivity, symmetry and transitivity of that relation.
background
Recognition Geometry module RG3 starts from a recognizer map $R:Cto E$ and defines two configurations to be indistinguishable when they yield identical events. The resulting relation is an equivalence, so its equivalence classes become the resolution cells: the indivisible units that the given recognizer can separate. The module axiom RG3 therefore reads: $c_1 sim c_2$ precisely when $R(c_1)=R(c_2)$.
proof idea
The definition is a one-line wrapper that populates the relation field of Setoid with the Indistinguishable predicate and supplies the iseqv field by direct appeal to the sibling lemma that already establishes reflexivity, symmetry and transitivity.
why it matters
It supplies the concrete setoid required by the RecognitionQuotient construction and by the canonical projection in the Quotient sibling module. The definition therefore realizes axiom RG3 and feeds the passage from configuration space to the quotient that encodes observable events. It is referenced by quotientMk_eq_iff, RecognitionQuotient and recognizerSetoid.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.