pith. sign in
module module high

IndisputableMonolith.RecogGeom.Recognizer

show as:
view Lean formalization →

The Recognizer module defines the recognition map from configurations to events as the central object of Recognition Geometry. It connects configuration space to observable events and asserts RG2 on the existence of at least one nontrivial recognizer. Downstream modules on dimension, examples, foundations, indistinguishability, and integration import it to build geometric structure. This is a definition module with no proofs.

claimA recognizer is a map $R: \mathcal{C} \to \mathcal{E}$ from configurations to events. RG2 asserts that at least one nontrivial recognizer exists.

background

Recognition Geometry derives space from the structure of recognition maps rather than taking it as primitive. The Core module supplies the foundational types for configurations and events. The Locality module adds neighborhood structure on configuration spaces and states axiom RG1 that recognition is always local.

This module introduces the recognizer as the map linking the two worlds and records RG2 on nontrivial instances. It is the basic interface between configuration space and the event world.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module supplies the central object that feeds Dimension for recognition dimension, Examples for concrete cases, Foundations for the fundamental theorems, Indistinguishable for RG3, and Integration for the complete framework. It directly encodes RG2 on the existence of nontrivial recognizers, which anchors the RG1-RG3 axiom chain.

scope and limits

used by (5)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (4)