pith. sign in
module module high

IndisputableMonolith.Recognition

show as:
view Lean formalization →

The Recognition module defines the minimal recognizer-to-recognized pairing that serves as the entry point for all recognition concepts. Modules deriving forcing results and ledger models cite it as the base layer. It consists entirely of definitions with no theorems or proofs.

claimMinimal pairing recognizer $\to$ recognized, together with RecognitionStructure, Chain, Ledger, and $\phi$-based objects.

background

The module supplies the core definitions for recognition as a directed pairing. Sibling declarations include Recognize, RecognitionStructure, Chain (with head and last), Ledger, and phi. These establish the basic objects before any composition law or forcing is applied.

The local setting is the Recognition domain, which imports only Mathlib and is imported by eight downstream modules. No upstream results are depended on; the module is the root of the recognition hierarchy.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

It supplies the base pairing fed to Foundation.RecognitionForcing (which proves recognition is forced by the cost foundation) and to LedgerPostingAdjacency (which upgrades to explicit ledger states with one-bit adjacency). It also supports LedgerUniqueness and Potential. The module fills the initial recognition step before the T0-T8 forcing chain or RCL is invoked.

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)