Pith. sign in
module module high

IndisputableMonolith.Recognition

show as:
view Lean formalization →

Recognition module defines the minimal recognizer-to-recognized pairing as the base object. Forcing and ledger modules cite it to anchor their constructions. The module supplies definitions and elementary properties with no elaborate proofs.

claimThe module introduces the minimal pairing in which a recognizer $r$ stands in relation to a recognized object $o$.

background

The module supplies the entry-point definitions for recognition structures. It introduces the core pairing, chains, ledgers, and the basic recognition relation used by all downstream files. The setting is the minimal axioms required before the Recognition Composition Law or the T0-T8 forcing chain can be applied.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module is imported by Foundation.RecognitionForcing to establish that recognition is forced by the cost foundation, and by LedgerPostingAdjacency and LedgerUniqueness for ledger models. It supplies the base step of the T0-T8 chain.

scope and limits

used by (8)

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

declarations in this module (24)