discrete_singleton_cells
plain-language theorem explainer
Each configuration in the discrete recognizer on Fin n (n at least 2) forms its own singleton resolution cell. Researchers checking that the discrete example achieves full distinguishability would cite this corollary. The proof is a one-line term applying set extensionality followed by simplification with the indistinguishability-equals-equality equivalence.
Claim. Let $n$ be a natural number with $ngeq 2$. For the discrete recognizer on the finite set $mathrm{Fin},n$, the resolution cell containing any configuration $c$ is the singleton set $lbrace c rbrace$.
background
Recognition Geometry equips a configuration space with a recognizer that induces an indistinguishability relation. The discrete recognizer on Fin n is the identity map, so two configurations are indistinguishable precisely when they are equal. ResolutionCell of a recognizer at a point is the equivalence class of configurations indistinguishable from that point under the induced relation. The module develops this as the first concrete example, where the quotient recovers the original space exactly. Upstream, ConfigSpace supplies the nonempty type of states, while discrete_indist_iff_eq supplies the key equivalence used in the simplification.
proof idea
The proof is a one-line wrapper. It applies the ext tactic to reduce the set equality to pointwise membership, then invokes simp with ResolutionCell and the upstream theorem discrete_indist_iff_eq that rewrites indistinguishability to equality.
why it matters
The corollary confirms the discrete case of the module's first example, where every configuration is distinguishable and the quotient is isomorphic to the original space. It is referenced inside the downstream examples_status definition that summarizes the discrete, sign, and magnitude recognizers. In the Recognition framework this supplies the base case of perfect recognition before composition is applied to refine coarser partitions such as sign and magnitude on Z.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.