distinguishable_iff_not_indistinguishable
plain-language theorem explainer
Two configurations are distinguishable exactly when they map to distinct events under the recognizer. Recognition-geometry work on resolution cells cites this duality to partition configuration space. The proof is a one-line term that applies reflexivity of logical equivalence to the definition of Distinguishable as negation of the induced relation.
Claim. Let $r$ be a recognizer from configurations $C$ to events $E$. For $c_1,c_2$ in $C$, $r.R(c_1)≠r.R(c_2)$ if and only if it is not the case that $c_1∼_r c_2$, where $∼_r$ is the equivalence $r.R(c_1)=r.R(c_2)$.
background
Module RecogGeom.Indistinguishable develops the indistinguishability relation induced by a recognizer $r:Recognizer C E$. By definition, $c_1∼_r c_2$ holds precisely when the recognizer maps both to the same event. The equivalence classes are the resolution cells, the smallest units that the recognizer can separate.
proof idea
The proof is a direct term-mode application of Iff.rfl. It holds because the definition of Distinguishable is exactly the negation of the indistinguishability relation on the same recognizer.
why it matters
The result anchors the basic duality between distinguishability and indistinguishability in recognition geometry. It supports the construction of resolution cells as equivalence classes under axiom RG3. No downstream uses appear, so the lemma functions as a foundational fact for any later partitioning of configuration space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.