pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.RecogGeom.Dimension

show as:
view Lean formalization →

The RecogGeom.Dimension module defines separating recognizers as injective maps on configuration spaces. Researchers building geometric models from recognition maps cite it to establish when a recognizer fully resolves configurations. The module assembles definitions and equivalences from core recognizer, indistinguishability, quotient, and composition imports without new proofs.

claimA recognizer $R: C → E$ separates the configuration space if it is injective: $R(c_1) = R(c_2)$ implies $c_1 = c_2$ for all $c_1, c_2 ∈ C$. Related notions include the separating quotient being bijective and independent recognizers strictly refining one another.

background

Recognition Geometry constructs space from recognition maps rather than taking it as primitive. The Core module supplies the basic type of a recognizer as a function from configurations to events. The Indistinguishable module defines the induced equivalence relation whose classes are resolution cells. The Quotient module collapses indistinguishable configurations into the recognition quotient $C_R$. The Composition module develops composite recognizers and proves the Refinement Theorem. This Dimension module adds the separating property on top of those foundations.

proof idea

This is a definition module, no proofs. It introduces IsSeparating as the predicate that a recognizer is injective on C, supplies the equivalence isSeparating_iff, proves separating_quotient_bijective and separating_singleton_cells, and defines PairSeparates together with independent_strict_refines. The final dimension_status aggregates these into a status flag for the recognizer.

why it matters in Recognition Science

The module supplies the separating and dimension_status concepts that feed directly into the complete integration summary in IndisputableMonolith.RecogGeom.Integration. It fills the dimension-related slot in the Recognition Geometry framework, where injectivity of recognizers determines whether the induced quotient recovers the original configuration space.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (9)