pith. machine review for the scientific record. sign in
def definition def or abbrev

toRecognitionDistance

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 205def toRecognitionDistance {L : Type*} [RSConfigSpace L]
 206    (j : JCostComparative L) : RecognitionDistance L where
 207  dist := j.J

proof body

Definition body.

 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 |
 223| RG2 (Recognizers) | Measurement maps |
 224| RG3 (Indistinguishability) | Same measurement outcomes |
 225| RG4 (Finite resolution) | 8-tick cycle |
 226| RG6 (Composition) | Multiple measurements |
 227| RG7 (Comparative) | J-cost function |
 228
 229Physical space and time emerge as recognition quotients.
 230The metric emerges from the J-cost comparative recognizer.
 231Gauge symmetries are exactly recognition-preserving ledger transformations.
 232-/
 233
 234/-! ## Module Status -/
 235

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (34)

Lean names referenced from this declaration's body.

… and 4 more