pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.RecogGeom.Locality

show as:
view Lean formalization →

The Locality module defines local configuration spaces as configuration spaces equipped with neighborhood structures, establishing axiom RG1 of Recognition Geometry. Neighborhoods permit statements about nearby configurations without metrics or full topologies. Researchers developing recognition maps or foundational theorems cite this module for its minimal locality structure. The module supplies type definitions together with discrete and trivial instances.

claimA local configuration space is a pair $(C, N)$ where $C$ is a configuration space and $N$ is a neighborhood structure on $C$ that assigns to each point a collection of subsets containing it.

background

Recognition Geometry derives spatial notions from the structure of recognition maps rather than taking space as primitive. The upstream Core module supplies the basic configuration space types. This module augments those types with neighborhood structures, allowing local comparisons while remaining agnostic about metrics or continuity.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the locality structure RG1 required by the fundamental theorems in Foundations, the integration summary in Integration, and the recognition maps in Recognizer. It supplies the minimal neighborhood data needed before recognition maps can compare nearby configurations and before spatial dimensions emerge in the larger Recognition Science framework.

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)