Pith. sign in
module module high

IndisputableMonolith.RecogGeom.Quotient

show as:
view Lean formalization →

Defines the recognition quotient C_R = C/~ obtained by collapsing configurations that a recognizer cannot tell apart. Supplies the quotient type, the canonical projection, event maps that descend to the quotient, and lift/project utilities for sets and neighborhoods. Downstream composition and finite-resolution modules import this construction as the space on which refinement and discreteness statements live.

claimGiven a configuration space $C$ and an indistinguishability relation $\sim$ induced by a recognizer, form the recognition quotient $C_R = C/\sim$. The module provides the quotient map $q: C \to C_R$, the descended event map on $C_R$, injectivity of that map on the image, and the standard lift/project operations for functions and neighborhoods.

background

Recognition Geometry treats measurement as a lossy map from configurations to events. The upstream Indistinguishable module (RG3) fixes the equivalence relation $\sim$: two configurations are equivalent when no recognizer event separates them. Equivalence classes are the resolution cells, the smallest distinguishable units of configuration space.

This module packages that relation into a quotient type $C_R = C/\sim$. The canonical projection sends each configuration to its cell. Because events are constant on cells, they factor through $C_R$, yielding a well-defined event map on the quotient. The construction is the geometric substrate for later axioms: finite local resolution (only finitely many cells in a bounded neighborhood) and composition of recognizers (refinement of cells under joint measurement).

proof idea

Definition module built on Mathlib quotients. It introduces RecognitionQuotient as $C/\sim$, the maker recognitionQuotientMk, and the characterization quotientMk_eq_iff. Events respect $\sim$, so quotientEventMap descends; quotientEventMap_spec and quotientEventMap_injective record the universal property and injectivity on the image. liftToQuotient and projectSet are the standard quotient-induction and set-projection helpers; quotientNeighborhoods equips $C_R$ with the quotient topology data needed by finite-resolution arguments. No deep theorems here: the work is packaging and the usual quotient lemmas.

why it matters in Recognition Science

Every later RecogGeom statement that speaks of distinguishable states works on $C_R$, not raw $C$. Composition (RG6) imports the quotient to state the Refinement Theorem for composite recognizers: joint measurement refines cells rather than inventing new continuum structure. FiniteResolution (RG4) imports it to assert that only finitely many quotient points sit in any bounded neighborhood, the bridge from lossy recognition to apparent discreteness at fundamental scales.

In the broader Recognition Science chain this is geometric scaffolding rather than a forcing step (T5–T8). It makes precise the claim that physics sees resolution cells, not bare configurations, which is the setting in which eight-tick and dimension-forcing arguments later operate.

scope and limits

used by (2)

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)