pith. sign in
module module high

IndisputableMonolith.Recognition

show as:
view Lean formalization →

The Recognition module supplies the minimal recognizer-to-recognized pairing that initiates the Recognition Science framework. Workers on the cost foundation and ledger models cite it as the entry point before J-uniqueness or phi-ladder constructions. The module consists entirely of definitions with no proofs or theorems.

claimA minimal pairing between a recognizer and the object it recognizes, written as recognizer → recognized.

background

Recognition Science derives all physics from one functional equation. This module opens the Recognition namespace by fixing the basic recognizer-recognized relation as the starting object. It is imported by eight downstream modules and precedes any mention of J-cost, defect distance, or the eight-tick octave.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds Core.Recognition, Foundation.RecognitionForcing (which proves recognition is forced by the cost foundation), LedgerPostingAdjacency, LedgerUniqueness, Potential, Recognition.Cycle3, and RRF.Core.Recognition. It supplies the initial pairing required for the T0–T8 forcing chain and the Recognition Composition Law.

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)