isSeparating_iff
plain-language theorem explainer
The equivalence states that a recognizer separates configurations precisely when indistinguishability implies equality of the underlying points. Researchers in recognition geometry cite this to connect injectivity of the recognizer map to the absence of distinct indistinguishable pairs. The proof is a one-line reflexivity that follows directly from unfolding the definitions of separation and indistinguishability.
Claim. Let $r$ be a recognizer from configuration space $C$ to evidence space $E$. Then $r$ separates $C$ if and only if for all $c_1, c_2$ in $C$, if $c_1$ and $c_2$ are indistinguishable under $r$ then $c_1 = c_2$.
background
Recognition geometry defines dimension as the minimum number of independent recognizers needed to distinguish all configurations. A recognizer $r$ separates when its map $r.R$ is injective on $C$, so distinct configurations produce distinct recognitions. The indistinguishability relation holds precisely when two configurations yield the same output under $r$ and therefore cannot be told apart by that recognizer.
proof idea
The proof is a one-line wrapper that applies reflexivity. It follows immediately once IsSeparating is unfolded to Function.Injective r.R and the indistinguishability predicate is recognized as the kernel of r.R.
why it matters
This equivalence feeds the dimension_status definition and closes the definitional link between separation and the absence of distinct indistinguishable pairs. It supports the module claim that spacetime dimension equals four because four independent recognizers suffice to separate events, consistent with the recognition dimension theory developed in the RecogGeom.Dimension module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.