Recognize
plain-language theorem explainer
The Recognize structure supplies the minimal recognizer-recognized pairing that serves as the primitive for all recognition statements in the framework. It is cited by the recognition forcing theorems and by the MP definition that rules out self-recognition of the empty type. The declaration is a direct structure with two fields and no proof obligations.
Claim. Let $A$ and $B$ be types. The structure Recognize$(A,B)$ consists of an element recognizer of type $A$ together with an element recognized of type $B$.
background
The module opens with T1 (MP): Nothing cannot recognize itself. Nothing is the empty type Empty. The sibling definition MP asserts the negation of the existence of any Recognize Nothing Nothing instance. Upstream results supply the active-edge count A and coherence units that later appear in forcing statements built on Recognize.
proof idea
This is a structure definition that introduces the two fields recognizer and recognized; no tactics or lemmas are applied.
why it matters
Recognize supplies the basic object used by recognition_necessary and recognition_forcing_complete to convert observable differences into nonempty recognition pairs. It directly realizes the T1 MP step that Nothing cannot recognize itself and is re-exported in the RRF core. The structure closes the minimal pairing needed before cost or forcing axioms are added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.