pith. the verified trust layer for science. sign in
module module high

IndisputableMonolith.RecogGeom.Recognizer

show as:
view Lean formalization →

The Recognizer module defines the basic map from configuration spaces to observable events as the central object of Recognition Geometry. Researchers in emergent geometry and foundations of physics would cite it when building dimension or indistinguishability results from recognition structure. The module states axiom RG2 on the existence of at least one nontrivial recognizer and supplies the type declarations that downstream modules import directly.

claimA recognizer is a map $R: C → E$ from configurations to events such that recognition is performed within finite neighborhoods (RG1) and at least one nontrivial recognizer exists (RG2).

background

Recognition Geometry treats space as emergent from recognition maps rather than primitive. The Core module supplies the foundational types for configurations and events. The Locality module introduces axiom RG1, which requires that every recognition act occurs inside a finite neighborhood of configurations rather than globally.

proof idea

This is a definition module, no proofs. It declares the recognizer type and states the existence claim RG2 as an axiom.

why it matters in Recognition Science

This module supplies the central object for the entire Recognition Geometry framework. It directly feeds the Dimension module on recognition dimension, the Foundations module on fundamental theorems, the Indistinguishable module on RG3, the Integration module for synthesis, and the Examples module for concrete cases. The declaration encodes axiom RG2 on nontrivial recognizer existence.

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)