discrete_indist_iff_eq
plain-language theorem explainer
The theorem states that for the discrete recognizer on Fin n with n at least 2, two configurations are indistinguishable exactly when they coincide. Recognition geometry researchers cite it to verify that the discrete case produces the trivial quotient space. The proof is a one-line simplification that unfolds the definitions of Indistinguishable and the recognizer.
Claim. For the discrete recognizer $R$ on the finite set $Fin(n)$ with $n$ a natural number at least 2, two configurations $c_1, c_2$ satisfy $c_1$ indistinguishable from $c_2$ under $R$ if and only if $c_1 = c_2$.
background
Recognition Geometry supplies concrete examples to illustrate the general framework. The discrete recognizer on Fin n is defined by the identity map, so it distinguishes every pair of configurations. Indistinguishable is the relation that holds when a recognizer maps two inputs to the same output event. The module develops this case first because the resulting quotient is isomorphic to the original space, providing a baseline before sign and magnitude recognizers on the integers.
proof idea
The proof is a one-line wrapper that applies simp to the definitions of Indistinguishable and discreteRecognizer. Unfolding shows that the recognizer applies the identity, so the indistinguishability predicate reduces directly to equality on Fin n.
why it matters
This result anchors the discrete example in the module and feeds the corollary that each configuration occupies its own resolution cell. It confirms the module claim that the discrete recognizer yields the trivial quotient. The example sits at the start of the concrete illustrations before the sign and magnitude cases that demonstrate composition refining distinctions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.