`RecognitionGeometry`

definition

show as: view math explainer →

module: IndisputableMonolith.RecogGeom.Integration
domain: RecogGeom
line: 72 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RecogGeom.Integration on GitHub at line 72.

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

  69
  70/-- A complete recognition geometry bundles all the structures together.
  71    This is the main type-theoretic definition of a recognition geometry. -/
  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 -/
 102def complete_summary : String :=

papers checked against this theorem

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