mem_resolutionCell_self
plain-language theorem explainer
Every configuration belongs to its own resolution cell under the equivalence relation induced by a recognizer. Researchers formalizing partitions of configuration space in Recognition Geometry cite this membership fact when establishing that cells are non-empty and cover the space. The proof is a direct one-line application of reflexivity for the indistinguishability relation.
Claim. For a recognizer $r : C → E$, let $c_1 ∼_r c_2$ denote the relation $r(c_1) = r(c_2)$. The resolution cell of $c$ is the set $ {c' : C | c' ∼_r c} $. Then $c$ belongs to this set.
background
The module formalizes axiom RG3: given a recognizer map from configurations $C$ to events $E$, indistinguishability is the equivalence $c_1 ∼ c_2$ iff the recognizer sends both to the same event. ResolutionCell $r$ $c$ is defined as the equivalence class $ {c' | c' ∼_r c} $, the smallest unit of configuration distinguishable by this recognizer.
proof idea
The proof is a one-line term that applies the reflexivity lemma for the indistinguishability relation induced by the recognizer.
why it matters
This supplies the reflexivity needed to prove that resolution cells partition configuration space and cover arbitrary subsets. It is invoked in the downstream theorems establishing local covers and unique cell membership. In the Recognition Science framework it anchors the geometric content of RG3 by guaranteeing every configuration sits inside its own cell, with no open scaffolding questions attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.