resolutionCell_eq_iff
plain-language theorem explainer
Two configurations share the same resolution cell under a recognizer precisely when they produce identical events and are therefore indistinguishable. Researchers modeling lossy recognition maps or equivalence classes in configuration spaces cite this equivalence. The proof is a direct biconditional split that invokes membership in the resolution cell together with symmetry and transitivity of indistinguishability.
Claim. Let $r$ be a recognizer from configurations $C$ to events $E$. For $c_1,c_2$ in $C$, the set of all configurations producing the same event as $c_1$ equals the set producing the same event as $c_2$ if and only if $c_1$ is indistinguishable from $c_2$ under $r$.
background
Recognition geometry defines an indistinguishability relation on configurations induced by a recognizer map $R:C→E$: two configurations are related when they yield the same event. The resolution cell of a configuration $c$ is its equivalence class, the set of all configurations that map to the same event as $c$. This module encodes axiom RG3 that these cells are the smallest units distinguishable by the given recognizer.
proof idea
The tactic proof opens with constructor to split the biconditional. Forward: equality of cells places $c_2$ inside the cell of $c_1$, then symmetry of indistinguishability yields the relation. Reverse: extensionality reduces set equality to pointwise membership, which follows by transitivity from the assumed indistinguishability and reflexivity.
why it matters
The result is a basic lemma confirming that resolution cells coincide exactly with the fibers of the recognizer, implementing the core insight of RG3. It supports later statements on partitioning of configuration space, though the current dependency graph shows no direct downstream uses. The lemma closes the definitional loop between set equality and the underlying equivalence relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.