locally_regular_cell_connected
plain-language theorem explainer
If a recognizer is locally regular at configuration c, then its resolution cell intersected with some neighborhood of c remains recognition-connected. Researchers modeling the emergence of smooth geometry from discrete recognition events cite this to guarantee coherent local clusters. The proof is a direct term extraction that unpacks the local regularity witness and applies the mutual indistinguishability condition to the intersection.
Claim. Let $L$ be a local configuration space, $r$ a recognizer from configurations to events, and $c$ a configuration. If $r$ is locally regular at $c$, then there exists a neighborhood $U$ of $c$ such that the intersection of the resolution cell of $c$ with $U$ is recognition-connected under $r$.
background
The module develops recognition geometry under the RG5 local regularity axiom. IsLocallyRegular at $c$ asserts that the preimage of the event $r.R c$ under $r$ is recognition-connected inside some neighborhood drawn from the local filter $L.N c$. IsRecognitionConnected on a set $S$ means every pair of points in $S$ is indistinguishable, i.e., maps to the identical event under $r$ and therefore lies in the same resolution cell.
proof idea
The term proof obtains the neighborhood $U$ and the connectivity witness $hconn$ directly from the hypothesis $h$. It rewrites membership in the intersection via the definition of ResolutionCell as the preimage $r.R^{-1}'{r.R c}$, then applies $hconn$ to any two points in that intersection to conclude they are indistinguishable.
why it matters
This result supplies the local coherence property required by RG5 and is invoked by the connectivity_status definition that records resolution cells as locally blob-like rather than fragmented. It supports the framework claim that recognition connectivity permits smooth structure to emerge from discrete events, consistent with the forcing chain that fixes three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.