pith. sign in
module module high

IndisputableMonolith.RecogGeom.Foundations

show as:
view Lean formalization →

Foundations module assembles Recognition Geometry axioms into pillars, with Pillar 1 showing the event map on the quotient is injective. It imports Core, Locality, Indistinguishability, Quotient, Composition, and FiniteResolution to organize how recognition induces equivalence classes. Physicists deriving emergent geometry from recognition maps would cite it for the quotient injectivity result. The module acts as an organizational hub whose siblings contain the actual pillar statements.

claimThe event map on the recognition quotient $C/\sim_R$ is injective, so each event determines a unique equivalence class under the indistinguishability relation induced by recognizer $R$.

background

Recognition Geometry treats space as emergent from recognition maps on configuration spaces rather than primitive. The module imports the locality structure (RG1) restricting recognition to finite neighborhoods, the indistinguishability relation (RG3) whose classes form resolution cells, the quotient construction collapsing indistinguishable configurations, finite local resolution (RG4) limiting distinctions inside bounded regions, and the composition theory (RG6) for multiple recognizers acting on one space. Upstream Core states the framework where space emerges from recognition map structure; upstream Quotient states the construction of $C_R = C/\sim$.

proof idea

This is a definition module, no proofs. It declares imports of the seven core RecogGeom modules and lists sibling declarations that state the pillars and fundamental theorems.

why it matters in Recognition Science

The module feeds the Integration module that supplies the complete framework summary. It records Pillar 1 from its doc comment: the event map on the quotient is injective, so events determine equivalence classes uniquely. This step supports the chain from locality and indistinguishability axioms to the full geometric structure.

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)