exists_distinguishable
plain-language theorem explainer
The theorem guarantees existence of two configurations that a recognizer maps to distinct events, following from the recognizer's nontriviality. Recognition geometers cite it to confirm that the induced equivalence on configurations is not universal. The proof is a one-line term that invokes the nontrivial property of the recognizer.
Claim. Let $r$ be a recognizer from configurations $C$ to events $E$. There exist $c_1, c_2$ in $C$ such that the recognition map of $r$ sends $c_1$ and $c_2$ to different events.
background
Recognition Geometry (RG3) equips a recognizer $r$ with a map $R: C → E$. Indistinguishability holds when $R(c_1) = R(c_2)$, so the equivalence classes are the resolution cells—the minimal units separable by this map. Distinguishability is the negation: the recognizer sends the pair to unequal events. The module states that recognition is inherently lossy and that these cells form the basis for further geometry. Upstream, the nontrivial list from kinship graph cohomology enumerates the seven non-trivial kinship systems that supply concrete instances of non-degenerate recognizers. The Status inductive type classifies declarations as spec, derived, hypothesis or scaffold.
proof idea
The proof is a one-line wrapper that applies the nontrivial property of the recognizer $r$ to witness the existential claim over distinguishable pairs.
why it matters
This theorem anchors axiom RG3 by ensuring resolution cells are proper when the recognizer is nontrivial, preventing collapse of the configuration space. It supplies the existence step required before defining LocalResolution or resolutionCell partitions in the same module. Within Recognition Science it supports the lossy character of recognition that precedes the forcing chain and the eight-tick octave. No downstream theorems are recorded, so the result functions as a foundational existence lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.