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

RecognitionGeometry

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)

  72structure RecognitionGeometry (C E : Type*) [ConfigSpace C] [EventSpace E] where
  73  /-- Local structure from neighborhoods -/
  74  locality : LocalConfigSpace C
  75  /-- The recognizer -/
  76  recognizer : Recognizer C E
  77  /-- Finite resolution property (RG4) -/
  78  finite_resolution : HasFiniteResolution locality recognizer
  79
  80/-! ## The Master Theorem -/
  81
  82/-- **Master Theorem**: Recognition Geometry is Complete.
  83
  84    All core components are defined and connected:
  85    1. Configuration and event spaces (RG0, RG2)
  86    2. Locality structure (RG1)
  87    3. Indistinguishability relation (RG3)
  88    4. Quotient construction
  89    5. Finite resolution (RG4)
  90    6. Local regularity (RG5)
  91    7. Composition (RG6)
  92    8. Comparative structure (RG7)
  93    9. Charts and atlases
  94    10. RS bridge
  95
  96    This constitutes a complete new geometry. -/
  97/-! **Recognition Geometry Complete**: All core components defined and connected. -/
  98
  99/-! ## Module Summary -/
 100
 101/-- Summary of all Recognition Geometry modules -/

used by (2)

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

depends on (27)

Lean names referenced from this declaration's body.