metric_from_comparisons
plain-language theorem explainer
A family of comparative recognizers that collectively separate all distinct configurations and each respect a common distance function d forces d to be strictly positive on distinct pairs. Researchers deriving geometry from qualitative recognition processes cite this when establishing that metrics can emerge without being presupposed. The proof extracts an index i from the separation hypothesis and applies the positivity clause already present in the compatibility structure at that index.
Claim. Let $C$ be a nonempty set of configurations and $E$ an event space. Let $(R_i)_{i∈ι}$ be a family of comparative recognizers, each mapping pairs from $C×C$ to events in $E$ with a distinguished equality event. Let $(G_i)_{i∈ι}$ be the associated sets of greater-than events. Suppose the family separates points: for any distinct $c_1,c_2∈C$ there exists $i$ such that $R_i$ distinguishes them via $G_i$. Suppose each $R_i$ is compatible with a function $d:C×C→ℝ$, so that $d$ is nonnegative, symmetric, vanishes on the diagonal, and is strictly positive whenever $R_i$ separates the pair. Then $d(c_1,c_2)>0$ whenever $c_1≠c_2$.
background
Recognition Geometry begins with comparative recognizers rather than a pre-given metric. A ComparativeRecognizer is a structure that assigns to every ordered pair of configurations an event in $E$, together with a fixed equality event returned on self-comparison. The predicate SeparatesPoints asserts that for any two distinct configurations there is at least one recognizer in the family whose greater-than event set distinguishes them. MetricCompatible packages the usual metric axioms for a candidate distance $d$ together with the key implication that separation by the recognizer forces $d>0$ on that pair. The module sets this construction inside the broader program of showing that metric structure is induced by families of qualitative comparisons, as in interference or balance-scale measurements.
proof idea
The proof is a direct one-line extraction. From the separation hypothesis applied to distinct $c_1,c_2$ one obtains an index $i$ together with a witness that the pair is separated by the $i$-th recognizer and its greater-than set. The compatibility hypothesis at that index supplies a field dist_pos_of_separated whose application yields the required strict inequality.
why it matters
The result occupies the MetricApproximation section of Recognition Geometry and demonstrates that a common distance function becomes visible once sufficiently many comparative recognizers are present. It supplies the positivity half of a metric without assuming any prior geometry, consistent with the module's claim that absolute metrics are derived rather than primitive. No downstream uses are recorded yet, so the declaration functions as a foundational lemma for later constructions that would add the triangle inequality or completeness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.