isRecognitionConnected_resolutionCell
plain-language theorem explainer
Resolution cells satisfy the recognition-connected property by construction. A physicist deriving local regularity from discrete recognition steps would cite this when building RG5. The term proof reduces the statement to transitivity of indistinguishability after unfolding the cell definition.
Claim. Let $r$ be a recognizer and $c$ a configuration. The set of all configurations indistinguishable from $c$ under $r$ is recognition-connected, i.e., any two elements of this set are mutually indistinguishable under $r$.
background
The module develops recognition connectivity for recognizers, where a set $S$ is recognition-connected when every pair of its elements satisfies the indistinguishability relation. A resolution cell around $c$ is the set of configurations equivalent to $c$ under this relation. This places the result inside the local regularity discussion (RG5), which requires that preimages remain coherent clusters rather than scattered points so that smooth structure can emerge from discrete recognition.
proof idea
The term proof introduces two elements from the cell, simplifies membership to obtain indistinguishability from the center point, and applies transitivity together with symmetry of the indistinguishability relation.
why it matters
The result populates the connectivity_status definition, which lists resolution cells among the connected sets required for RG5. It supports the module claim that coherent cells act as atoms of recognition geometry, preventing fragmentation that would block smooth physics. The step aligns with the broader forcing chain that derives spatial dimension and local regularity from the J-cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.