isRecognitionConnected_singleton
plain-language theorem explainer
A singleton set satisfies recognition connectivity for any recognizer. Workers on recognition geometry cite this when establishing that resolution cells remain coherent at the smallest scale. The proof reduces the claim to reflexivity of indistinguishability after rewriting singleton membership.
Claim. Let $r$ be a recognizer and $c$ a configuration. Then the singleton set $S = {c}$ is recognition-connected: for all $c_1, c_2$ in $S$, $c_1$ and $c_2$ are indistinguishable under $r$.
background
Recognition connectivity is defined so that a set $S$ is recognition-connected for recognizer $r$ precisely when every pair of its elements is mutually indistinguishable. The module develops this notion to support local regularity (RG5), ensuring that resolution cells do not fragment into scattered points and thereby allowing smooth geometric structure to emerge from discrete recognition steps.
proof idea
The term proof introduces two points $c_1, c_2$ in the singleton, applies the membership simplification lemma for singletons to obtain $c_1 = c = c_2$, and concludes by reflexivity of the indistinguishability relation.
why it matters
The result feeds the connectivity_status definition that lists singleton connectivity among the verified properties of recognition geometry. It supplies the base case for the RG5 development in the module, confirming that single-point cells remain coherent and thereby supporting the emergence of continuous structure from the recognition process.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.