pith. sign in
module module high

IndisputableMonolith.RecogGeom.Foundations

show as:
view Lean formalization →

The RecogGeom.Foundations module collects the core pillars of Recognition Geometry, beginning with Pillar 1 that the event map on the recognition quotient is injective. Researchers integrating recognition-based geometry cite it to guarantee that events fix equivalence classes uniquely. The module assembles imported results from locality, indistinguishability, quotient, composition and finite-resolution modules into a single foundation without new proofs.

claimThe event map $e: C_R → E$ on the recognition quotient $C_R = C / ∼$ is injective: $e([c_1]) = e([c_2])$ implies $[c_1] = [c_2]$.

background

Recognition Geometry treats space as emergent from recognition maps rather than primitive. Upstream modules supply the setting: Locality (RG1) equips configuration spaces with neighborhood structure; Indistinguishability (RG3) defines the lossy equivalence ∼ whose classes are resolution cells; Finite Resolution (RG4) requires only finitely many distinguishable configurations inside any bounded neighborhood; Quotient constructs $C_R = C/∼$; Composition develops composite recognizers and the Refinement Theorem; Core supplies the basic types.

proof idea

This is a definition module, no proofs. It organizes the imported modules into named pillars and fundamental theorems listed among its siblings.

why it matters in Recognition Science

The module supplies Pillar 1 to the complete integration performed by IndisputableMonolith.RecogGeom.Integration. It anchors the framework in which the quotient map preserves event information, allowing downstream work to treat equivalence classes as the observable units from which geometry is built.

scope and limits

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.

declarations in this module (10)