ResolutionCell
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not assume the recognizer separates points.
- Does not specify the internal structure of the event space E.
- Does not address how cells behave under changes of recognizer.
- Does not extend the construction to continuous or infinite-dimensional configuration spaces.
formal statement (Lean)
71def ResolutionCell {C E : Type*} (r : Recognizer C E) (c : C) : Set C :=
proof body
Definition body.
72 {c' : C | c' ~[r] c}
73
74/-- A configuration is in its own resolution cell -/
used by (15)
-
composite_cell_subset_left -
composite_cell_subset_right -
composite_resolutionCell -
isRecognitionConnected_resolutionCell -
locally_regular_cell_connected -
separating_singleton_cells -
discrete_singleton_cells -
indistinguishable_status -
LocalResolution -
localResolution_covers -
mem_resolutionCell_self -
resolutionCell_eq_fiber -
resolutionCell_eq_iff -
resolutionCells_partition -
symmetry_maps_cells