MetricCompatible
plain-language theorem explainer
MetricCompatible encodes the five axioms making a function d a metric compatible with a given comparative recognizer R_cmp and greater-than events set. Recognition-geometry researchers cite it when deriving quantitative distances from qualitative comparison data. The declaration is a direct structure definition that axiomatizes the required properties without invoking lemmas or reductions.
Claim. Let $R$ be a comparative recognizer on configuration space $C$ with event type $E$, let $G$ be a set of greater-than events, and let $d:C→ C→ℝ$. Then $d$ is metric-compatible with $R$ and $G$ when $d(c,c)=0$ for every $c$, $d(c_1,c_2)≥0$ for all pairs, $d$ is symmetric, $d(c_1,c_2)>0$ whenever $c_1$ and $c_2$ are separated by $R$ and $G$, and $d(c_1,c_3)≤ d(c_2,c_3)$ for all $c_3$ whenever $c_1$ is not greater than $c_2$ under $R$ and $G$.
background
A comparative recognizer is a structure that maps each ordered pair of configurations to a comparison event while sending every self-pair to a fixed equal event. SeparatedBy holds precisely when two configurations fail to be comparatively equivalent under the recognizer and the supplied greater-than event set. The module develops the induced preorder and partial-order structures before introducing metric compatibility. This local setting treats comparative recognition as primary data from which metric-like functions are extracted, mirroring how physical measurements (phase comparison, mass balance) begin with relational judgments rather than absolute scales.
proof idea
The declaration is a structure definition whose five fields directly state the metric axioms adapted to the comparative setting: self-distance zero, non-negativity, symmetry, strict positivity on separated pairs, and monotonicity with respect to the induced not-greater-than relation. No upstream lemmas are applied; the structure simply packages the required properties for later use in approximation theorems.
why it matters
MetricCompatible supplies the compatibility hypothesis for the downstream theorem metric_from_comparisons, which shows that a family of comparative recognizers that collectively separate points and share a common compatible distance function yields a metric approximation. The definition therefore closes one step in the Recognition Geometry program (RG7) by making precise how qualitative comparison data can recover quantitative distance, consistent with the broader Recognition Science stance that metric structure emerges from recognition rather than being presupposed. It directly supports the physical interpretation that measurements such as interference or balance scales are fundamentally comparative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.