SeparatedBy
plain-language theorem explainer
SeparatedBy declares that two configurations are distinguished precisely when a comparative recognizer does not return equivalent comparison events. Workers constructing emergent metrics from qualitative relations cite it when proving that families of recognizers separate points or induce compatible distances. The definition is a direct one-line negation of the comparativeEquiv predicate.
Claim. Let $R$ be a comparative recognizer on configuration space $C$ with event space $E$, and let $G$ be a set of greater-than events. Configurations $c_1, c_2$ are separated by $R$ when they are not comparatively equivalent under $R$ and $G$.
background
Recognition Geometry begins with comparative recognizers that output only qualitative relations between pairs of configurations rather than absolute labels or distances. The structure ComparativeRecognizer supplies a compare map $C×C→E$, a distinguished eq_event, and the axiom that self-comparison always yields the equal event. From these the module derives induced preorders, partial orders, and eventually metric approximations.
proof idea
One-line definition that negates the comparativeEquiv predicate on the supplied recognizer, event set, and configuration pair.
why it matters
The predicate feeds SeparatesPoints, which requires every distinct pair to be separated by some member of a family, and MetricCompatible, which extracts non-negative distance functions. It therefore occupies the step in RG7 that converts qualitative comparison data into the separation axioms needed for metric emergence, consistent with the broader program of deriving geometry from the forcing chain without presupposing a metric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.