`JCostComparative`

definition

show as: view math explainer →

module: IndisputableMonolith.RecogGeom.RSBridge
domain: RecogGeom
line: 192 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RecogGeom.RSBridge on GitHub at line 192.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 189    - Smaller J means "closer" states
 190
 191    This provides the metric-like structure on configuration space. -/
 192structure JCostComparative (L : Type*) [RSConfigSpace L] where
 193  /-- The J-cost function -/
 194  J : L → L → ℝ
 195  /-- J(ℓ, ℓ) = 0 -/
 196  self_zero : ∀ ℓ, J ℓ ℓ = 0
 197  /-- J ≥ 0 -/
 198  nonneg : ∀ ℓ₁ ℓ₂, 0 ≤ J ℓ₁ ℓ₂
 199  /-- Symmetry (for undirected version) -/
 200  symm : ∀ ℓ₁ ℓ₂, J ℓ₁ ℓ₂ = J ℓ₂ ℓ₁
 201  /-- Triangle inequality -/
 202  triangle : ∀ ℓ₁ ℓ₂ ℓ₃, J ℓ₁ ℓ₃ ≤ J ℓ₁ ℓ₂ + J ℓ₂ ℓ₃
 203
 204/-- J-cost gives a recognition distance -/
 205def toRecognitionDistance {L : Type*} [RSConfigSpace L]
 206    (j : JCostComparative L) : RecognitionDistance L where
 207  dist := j.J
 208  dist_nonneg := j.nonneg
 209  dist_self := j.self_zero
 210  dist_symm := j.symm
 211  dist_triangle := j.triangle
 212
 213/-! ## Summary: RS Instantiates Recognition Geometry
 214
 215**Master Theorem**: Recognition Science instantiates Recognition Geometry.
 216
 217RS provides a concrete model of all the RG axioms:
 218
 219| RG Axiom | RS Instantiation |
 220|----------|------------------|
 221| RG0 (Nonempty) | Ledger space is nonempty |
 222| RG1 (Locality) | R̂ neighborhoods |

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.