RecognitionDistance
plain-language theorem explainer
RecognitionDistance packages the axioms of a pseudometric on a configuration space C, with nonnegative symmetric distance obeying the triangle inequality and vanishing on diagonals. Recognition Geometry workers cite it when metric structure is extracted from comparative recognizers. The declaration is a direct structure definition encoding those axioms with no further computation.
Claim. A recognition distance on a set $C$ is a map $d: C×C→ℝ$ satisfying $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 elements of $C$.
background
Recognition Geometry (RG7) starts from comparative recognizers that output only qualitative relations (≤ or >) between pairs of configurations rather than presupposing a metric. The module shows how such recognizers induce preorders, partial orders, and eventually metric approximations; physical measurements such as phase comparisons or mass balances are treated as instances of this comparative structure. The structure RecognitionDistance is the target type into which J-cost functions are mapped, as indicated by the downstream bridge that supplies nonnegativity, self-zero, and symmetry fields from the cost definition in MultiplicativeRecognizerL4.
proof idea
The declaration is a structure definition that directly encodes the four pseudometric axioms as fields; no lemmas are applied and no tactics are used.
why it matters
The structure is the codomain of toRecognitionDistance, which exhibits a J-cost as an instance, and it is referenced in the module status summary comparative_status. It advances the RG7 program of deriving geometry from recognizers and sits inside the larger chain that extracts metric-like separation from the J-cost function. The embedded TODO records that the full formal bridge from J-cost to this structure remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.