SeparatedBy
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not presuppose a metric or topology on the configuration space.
- Does not construct or calibrate the comparative recognizer itself.
- Does not guarantee that separation produces a positive real-valued distance.
- Does not address continuity, completeness, or embedding into Euclidean space.
formal statement (Lean)
161def SeparatedBy (R_cmp : ComparativeRecognizer C E) (gt_events : Set E) (c₁ c₂ : C) : Prop :=
proof body
Definition body.
162 ¬comparativeEquiv R_cmp gt_events c₁ c₂
163
164/-- A family of comparative recognizers separates points if any two distinct
165 configurations are separated by at least one recognizer -/