Indistinguishable
plain-language theorem explainer
Indistinguishability equates two configurations precisely when a recognizer maps them to the same event. Workers constructing quotient spaces, charts, and composite recognizers cite this as the base equivalence of recognition geometry. The definition is a direct equality on the recognizer's output function.
Claim. Let $r$ be a recognizer with recognition map $R: C → E$. Configurations $c_1, c_2 ∈ C$ are indistinguishable under $r$, written $c_1 ∼_{[r]} c_2$, precisely when $R(c_1) = R(c_2)$.
background
Recognition geometry treats recognition as a map from configuration space $C$ to event space $E$. The map is lossy, so distinct configurations can produce identical events; the resulting equivalence classes are the resolution cells, the smallest units distinguishable by this particular recognizer. Module RG3 codifies this as axiom RG3: $c_1 ∼ c_2$ if and only if $R(c_1) = R(c_2)$.
Upstream material on collision-free empirical programs and edge lengths derived from psi supplies the simplicial and empirical setting in which recognizers are instantiated. The definition itself introduces no further structure on $C$ or $E$.
proof idea
The declaration is a direct definition: the body is the equality $r.R c_1 = r.R c_2$. Reflexivity, symmetry, and transitivity are proved in sibling theorems by applying Eq.refl, Eq.symm, and Eq.trans to that equality.
why it matters
The definition realizes axiom RG3 and supplies the equivalence relation used by every subsequent construction in the module. It is invoked to prove that charts on quotients are well-defined, that orders descend to quotients under compatibility, and that composite recognizers commute with indistinguishability. In the broader framework it encodes the lossy character of recognition that forces the passage from configurations to resolution cells.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.