separating_singleton_cells
plain-language theorem explainer
If a recognizer is separating, its recognition map is injective, so each resolution cell reduces to a singleton containing only the input configuration. Dimension theorists cite the result when linking recognizer count to geometric dimension in recognition geometry. The argument proceeds by set extensionality, membership simplification, and direct application of injectivity in one direction with reflexivity in the other.
Claim. Let $r$ be a recognizer from configuration space $C$ to evidence space $E$. If $r$ is separating (i.e., its recognition map is injective), then for every configuration $c$ the resolution cell of $r$ at $c$ equals the singleton set containing only $c$.
background
Recognition Geometry defines dimension as the smallest number of independent recognizers needed to distinguish every configuration. A recognizer separates when its map is injective on $C$, so no two distinct points remain indistinguishable. The resolution cell of $r$ at $c$ is the set of all configurations that $r$ cannot separate from $c$. The module states that spacetime dimension equals four precisely because four coordinates separate events completely.
proof idea
The proof applies set extensionality to equate the two sets. After simplification of the membership predicate inside ResolutionCell and the singleton, the forward direction invokes the separating hypothesis directly on the membership assumption. The reverse direction substitutes the equality hypothesis and concludes by reflexivity.
why it matters
The lemma feeds the dimension_status definition, which identifies quantum dimension with the number of independent observables required for separation. It realizes the module claim that four recognizers suffice for spacetime events. Within the Recognition framework it supplies the operational content of dimension as the minimal separating set size, consistent with the eight-tick octave and D=3 emergence from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.