ResolutionCell
plain-language theorem explainer
ResolutionCell defines the equivalence class of a configuration c under the indistinguishability relation induced by recognizer r, consisting of all configurations that map to the same event. Workers on recognition geometry cite it when partitioning configuration space into minimal distinguishable units per axiom RG3. The definition is a direct set comprehension from the equivalence relation.
Claim. Let $r: C → E$ be a recognizer. The resolution cell of configuration $c ∈ C$ is the set $ {c' ∈ C | r(c') = r(c)} $.
background
Recognition Geometry module RG3 defines indistinguishability from a recognizer map $R: C → E$: configurations $c_1, c_2$ satisfy $c_1 ~ c_2$ precisely when $R(c_1) = R(c_2)$. The equivalence classes under this relation are the resolution cells, the smallest units distinguishable by the given map. Module doc states these classes realize the lossy character of recognition.
proof idea
Direct definition by set comprehension: the set of all $c'$ such that $c' ~[r] c$.
why it matters
This definition supplies the core object for downstream theorems including composite_resolutionCell (cells under tensor are intersections), isRecognitionConnected_resolutionCell (cells are recognition-connected), and separating_singleton_cells (separating recognizers yield singletons). It fills axiom RG3 in the Recognition Geometry setting and supports the framework treatment of equivalence classes as resolution units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.