RecognitionDistance
plain-language theorem explainer
A recognition distance on configuration space C is a pseudometric whose distance function satisfies non-negativity, zero self-distance, symmetry, and the triangle inequality. Recognition Geometry researchers cite it when showing how metric structure emerges from comparative recognizers rather than being presupposed. The declaration is a structure definition that directly encodes the four pseudometric axioms with no additional lemmas.
Claim. A recognition distance on a set $C$ is a function $d:C×C→ℝ$ obeying $d(c_1,c_2)≥0$, $d(c,c)=0$, $d(c_1,c_2)=d(c_2,c_1)$, and $d(c_1,c_3)≤d(c_1,c_2)+d(c_2,c_3)$ for all $c_1,c_2,c_3$.
background
Recognition Geometry (RG7) begins with comparative recognizers that output only qualitative orderings between pairs of configurations, as described in the module documentation. From these, preorder and partial-order structures are extracted before metric-like distances appear. The supplied upstream results include the J-cost function from MultiplicativeRecognizerL4.cost, which is intended to induce such a distance, and the Physical structure from Bridge.DataCore that supplies the underlying constants.
proof idea
This is a structure definition that packages the distance function together with its four required properties; no tactics or lemmas are applied.
why it matters
The structure is instantiated by toRecognitionDistance in RSBridge to turn a JCostComparative into a RecognitionDistance, and it appears in comparative_status to record the RG7 status. It therefore supplies the concrete pseudometric object that the framework claims arises from J-cost functions, linking directly to the Recognition Composition Law and the intended physical interpretation that transition cost defines separation in recognition space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.