ResolutionCell
plain-language theorem explainer
ResolutionCell assigns to each configuration c the equivalence class of all configurations that map to the identical event under recognizer r. Researchers analyzing quotient spaces or connectivity in recognition geometry cite this when partitioning configuration space into minimal distinguishable units. The definition is realized directly as a set comprehension over the indistinguishability relation.
Claim. For a recognizer $r: C → E$, the resolution cell of configuration $c ∈ C$ is the set $ { c' ∈ C | r(c') = r(c) } $.
background
The module defines Recognition Geometry axiom RG3: given recognition map $R: C → E$, two configurations are indistinguishable precisely when they produce the same event. Equivalence classes under this relation are the resolution cells, the smallest units of configuration distinguishable by the given map. The definition relies on the Recognizer type and the induced equivalence relation, with upstream results on active edge counts and spectral structure supplying the surrounding dimensional and integration context.
proof idea
The declaration is a direct definition via set comprehension: the collection of all $c'$ such that $c'$ is indistinguishable from $c$ under $r$. No lemmas or tactics are applied; the body encodes the equivalence class explicitly.
why it matters
This definition feeds theorems establishing that composite resolution cells equal intersections of component cells, that each resolution cell is recognition-connected, and that separating recognizers produce singleton cells. It implements axiom RG3 of the Recognition Science framework, supplying the geometric partitioning of configuration space into lossy equivalence classes that later connect to dimensional emergence and the phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.