RecognitionDistance
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not prove the triangle inequality for any concrete J-cost.
- Does not show that d(c1,c2)=0 implies c1=c2.
- Does not construct the distance from a specific family of comparative recognizers.
- Does not address completeness or other metric-space properties.
Lean usage
def d : RecognitionDistance L := toRecognitionDistance jformal statement (Lean)
209structure RecognitionDistance (C : Type*) where
210 /-- The distance function -/
211 dist : C → C → ℝ
212 /-- Non-negativity -/
213 dist_nonneg : ∀ c₁ c₂, 0 ≤ dist c₁ c₂
214 /-- Self-distance is zero -/
215 dist_self : ∀ c, dist c c = 0
216 /-- Symmetry -/
217 dist_symm : ∀ c₁ c₂, dist c₁ c₂ = dist c₂ c₁
218 /-- Triangle inequality -/
219 dist_triangle : ∀ c₁ c₂ c₃, dist c₁ c₃ ≤ dist c₁ c₂ + dist c₂ c₃
220
221/-- A recognition distance is a metric (not just pseudometric) when
222 d(c₁, c₂) = 0 implies c₁ = c₂ -/
223def RecognitionDistance.IsMetric (d : RecognitionDistance C) : Prop :=
proof body
Definition body.
224 ∀ c₁ c₂, d.dist c₁ c₂ = 0 → c₁ = c₂
225
226/-!
227**Physical Interpretation (documentation)**: In Recognition Science, the J-cost function
228is intended to provide a natural recognition distance. The cost of transitioning between
229states defines their “separation” in recognition space.
230
231TODO: formalize the RS bridge showing how a J-cost induces a `RecognitionDistance`.
232-/
233
234/-! ## Module Status -/
235