pith. sign in
module module moderate

IndisputableMonolith.RecogGeom.Comparative

show as:
view Lean formalization →

The Comparative module defines comparative recognizers that map pairs of configurations to comparison events encoding their relations. Researchers constructing order structures within recognition geometry cite it when extending the quotient construction. The module supplies definitions for induced preorders, partial orders, and equivalence relations together with compatibility lemmas.

claimA comparative recognizer is a map $f: C_R^2 → E$ sending pairs of configurations in the recognition quotient to comparison events; it induces a preorder via the relation $c_1 ≼ c_2$ iff notGreaterThan$(f(c_1,c_2))$ fails, and a partial order when the induced equivalence is taken.

background

Recognition Geometry begins with the recognition quotient $C_R = C / ∼$ constructed in the Quotient module, where ∼ collapses configurations indistinguishable by the recognizer. The Comparative module sits directly on this quotient and introduces comparative recognizers together with auxiliary relations such as notGreaterThan and comparativeEquiv. These relations are shown to satisfy reflexivity, symmetry, and transitivity, yielding an induced preorder and, under additional conditions, a partial order.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the comparative structure required by the Integration module for a complete geometric framework and by the RSBridge module to instantiate Recognition Science, linking abstract order relations to ledger states, R̂ operators, and the 8-tick cycle.

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)