Pith. sign in
module module high

IndisputableMonolith.RecogGeom.Locality

show as:
view Lean formalization →

The Locality module introduces local configuration spaces as configuration spaces equipped with neighborhood structures, implementing RG1 of recognition geometry. Workers on emergent space from recognition maps cite it to ground locality discussions. It is a definition module that sets up the basic objects without proofs or theorems.

claimA local configuration space is a configuration space $C$ equipped with a neighborhood structure $\mathcal{N}$ on $C$.

background

Recognition Geometry treats space as emergent from recognition maps rather than primitive, as set out in the Core module. The Locality module supplies the RG1 definition: a local configuration space augments a configuration space with neighborhoods so that nearby configurations can be discussed. These neighborhoods operate without any metric or full topology.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the RG1 objects required by the Fundamental Theorems in Foundations. It is imported by Integration for the complete framework summary and by Recognizer for the RG2 recognition maps. It fills the first recognition-geometry axiom by introducing neighborhood structures on configuration spaces.

scope and limits

used by (3)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)