pith. sign in
module module high

IndisputableMonolith.RecogGeom.Foundations

show as:
view Lean formalization →

Recognition Geometry Foundations assembles the core axioms to prove that the event map on the recognition quotient is injective, so each event fixes a unique equivalence class of configurations. The module imports locality, indistinguishability, and quotient constructions, then composes them with recognizer properties to obtain this injectivity. It organizes the argument into pillars that feed the later integration of the full framework.

claimLet $C$ be a configuration space equipped with a recognizer $R$. The quotient map $q: C_R = C / {}_R$ to the event space $E$ satisfies: if $q(c_1) = q(c_2)$ then the events coincide, i.e., the induced event map is injective.

background

Recognition Geometry treats space as emergent from recognition maps rather than primitive. The module draws on the locality axiom defining finite neighborhoods on configuration spaces, the indistinguishability relation whose equivalence classes are the resolution cells, and the quotient construction that collapses indistinguishable configurations into $C_R$. Upstream results supply the basic recognizer and event types together with the refinement theorem for composite recognizers. Finite local resolution ensures only finitely many distinctions occur inside any bounded neighborhood.

proof idea

The module structures its argument around the three pillars. Pillar 1 proceeds by importing the quotient construction and applying the injectivity property of the event map directly to the equivalence classes. The remaining pillars invoke monotonicity of information and the obstruction from finite resolution, each reduced to the core definitions via one-line applications of the imported lemmas.

why it matters in Recognition Science

This module supplies the foundational injectivity and uniqueness results that the Integration module assembles into a complete summary of Recognition Geometry. It directly supports the universal property and quotient uniqueness statements among its siblings and fills the first pillar required for any downstream derivation of observables from recognition 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)