structure
definition
RecognitionDistance
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RecogGeom.Comparative on GitHub at line 209.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
206
207/-- A recognition distance is a pseudometric derived from a family of
208 comparative recognizers. -/
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 :=
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
236def comparative_status : String :=
237 "✓ ComparativeRecognizer defined (RG7)\n" ++
238 "✓ notGreaterThan, comparativeEquiv: induced relations\n" ++
239 "✓ InducesPreorder: when comparisons give a preorder\n" ++