Recognize
plain-language theorem explainer
The Recognize abbreviation re-exports the minimal recognizer-recognized pairing structure from the base Recognition module into the RRF namespace. Researchers building the Recognition Forcing theorems cite it to access the core type without crossing module boundaries. The declaration is a direct alias that carries the structure definition forward with no added content or computation.
Claim. The type $Recognize(A, B)$ is the structure consisting of a recognizer element of type $A$ and a recognized element of type $B$.
background
This module re-exports definitions from the Recognition module to bridge the existing framework with the RRF namespace. The Recognize structure supplies the minimal pairing of recognizer and recognized, while the related MP definition asserts that it is impossible for Nothing to recognize itself, written as the negation of an existential claim over Recognize Nothing Nothing. The local setting supplies RecognitionStructure, Chain, Ledger, and AtomicTick as supporting concepts for discrete recognition steps.
proof idea
This declaration is a direct re-export alias with no lemmas applied and no tactic steps.
why it matters
The re-export supports the master theorem recognition_forcing_complete, which derives existence of recognition pairings from observable distinctions, and the recognition_necessary result, which identifies recognition as the unique extraction mechanism. It supplies the base pairing required for the metaphysical primitive and the forcing chain that begins with the impossibility of self-recognition by Nothing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.