pith. sign in
module module high

IndisputableMonolith.RecogGeom.Quotient

show as:
view Lean formalization →

The Quotient module defines the recognition quotient C_R by collapsing the configuration space under the indistinguishability relation from a recognizer. Researchers formalizing Recognition Geometry under axiom RG3 cite it when moving from raw configurations to resolution cells. It is a definition module containing no proofs.

claim$C_R := C / \sim$, where $\sim$ is the indistinguishability equivalence relation on configuration space $C$ induced by a recognizer.

background

The upstream Indistinguishable module introduces axiom RG3: recognition is lossy, so multiple configurations map to the same event and form equivalence classes called resolution cells. The Quotient module takes this relation as given and constructs the quotient space whose points are these classes.

Recognition Geometry begins with qualitative detection rather than a pre-existing metric. The quotient supplies the first derived object on which later modules impose charts, connectivity, and dimension.

No additional structure such as a metric or topology is assumed at this stage; the construction remains purely set-theoretic on the equivalence classes.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the quotient object required by downstream modules including RecogGeom.Charts for local coordinates, RecogGeom.Dimension for recognition dimension, RecogGeom.Connectivity for paths within cells, and RecogGeom.Composition for refinement. It mirrors the quotient construction appearing in DraftV1.tex under the Recognition Geometry section tied to axiom RG3.

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)