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
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.