pith. sign in
module module high

IndisputableMonolith.RecogGeom.Comparative

show as:
view Lean formalization →

The Comparative module defines comparative recognizers that map pairs of configurations to comparison events encoding their relationships. It extends the recognition quotient by adding induced preorders and partial orders. Researchers extending Recognition Geometry to relational structures cite it when preparing the framework for integration with physical models. The module is definitional with supporting lemmas for reflexivity, symmetry, and transitivity.

claimLet $C$ be the space of configurations. A comparative recognizer is a map from $C$ times $C$ to comparison events that encodes relative status between pairs, inducing a preorder on the quotient space.

background

Recognition Geometry starts from the recognition quotient $C_R = C / {~}$ in the Quotient module, where ${~}$ collapses configurations that cannot be distinguished. The Comparative module sits on this quotient and introduces comparative recognizers to detect ordered relationships between pairs. It defines induced preorders, partial orders, and compatibility conditions that turn raw comparisons into structured relations.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module supplies the relational layer used by the Integration module to assemble the complete Recognition Geometry summary. It also feeds the RSBridge module that instantiates the framework with Recognition Science elements including the 8-tick cycle and R̂ operators. It fills the gap between the abstract quotient and concrete comparison-based geometry in the overall chain.

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