IsRecognitionConnected
plain-language theorem explainer
Recognition connectivity holds for a set S under recognizer r exactly when every pair of elements in S produces the identical event. Researchers establishing RG5 local regularity cite this predicate to guarantee that resolution cells remain coherent clusters. The definition directly encodes mutual indistinguishability as a universal condition over the set.
Claim. A set $S$ of configurations is recognition-connected under recognizer $r$ if for all $c_1, c_2$ in $S$, the event map satisfies $r.R(c_1) = r.R(c_2)$.
background
Recognition geometry develops connectivity to ensure resolution cells do not fragment into scattered points. The module defines IsRecognitionConnected so that all members of S are pairwise equivalent under the recognizer's event map. This rests on the upstream Indistinguishable relation, which states that two configurations are equivalent precisely when they produce the same event.
proof idea
The declaration is a direct definition that states the universal quantifier over pairs in S using the Indistinguishable predicate. No lemmas or tactics are invoked; it functions as the base predicate for the module's subsequent theorems on empty sets, singletons, and resolution cells.
why it matters
This definition supplies the core predicate for RG5 by ensuring preimages of events form connected clusters within neighborhoods. It feeds directly into IsLocallyRegular and the connectivity_status summary, which lists the empty-set, singleton, and resolution-cell cases. In the framework it prevents pathological fragmentation so that smooth geometric structure can emerge from discrete recognition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.