pith. sign in
module module high

IndisputableMonolith.RecogGeom.Quotient

show as:
view Lean formalization →

The Quotient module constructs the recognition quotient C_R by collapsing configurations under the indistinguishability relation. Researchers in recognition geometry cite it when moving from raw configuration space to the space of observable resolution cells. The module supplies the canonical projection, lifting maps, and basic functoriality properties needed by all subsequent geometry constructions.

claimLet $C$ be a configuration space equipped with an indistinguishability relation $xsim y$. The recognition quotient is the set $C_R := C/ sim$ together with the canonical projection $pi: C to C_R$ and the induced event map.

background

This module imports the indistinguishability relation from Indistinguishable, where recognition is lossy: multiple configurations may produce the same event, so equivalence classes become the smallest distinguishable units (resolution cells, Axiom RG3). It defines RecognitionQuotient as the quotient type, recognitionQuotientMk as the constructor, and auxiliary maps such as quotientEventMap and liftToQuotient that respect the equivalence. The local setting is Recognition Geometry, which starts from recognizer structure rather than an assumed metric.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The quotient supplies the passage from configurations to events that is presupposed by DraftV1 (the paper theorem mirror) and by the downstream modules Charts, Comparative, Composition, Connectivity, Dimension, EffectiveManifold, and Examples. It realizes the first step of the recognition geometry program: replacing the raw space C with the observable space C_R.

scope and limits

used by (13)

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 (14)