recognition_must_be_nonempty
plain-language theorem explainer
If a recognition pairing between two types is inhabited, both the recognizer type and the recognized type are inhabited. Necessity and exclusivity arguments cite this to rule out empty carriers once a recognition event is assumed. The proof is a one-step projection: unpack the Recognize witness and return its two fields as nonempty witnesses.
Claim. Let $A$ and $B$ be types. If there exists a recognition pairing $\mathrm{Recognize}(A,B)$ (a pair consisting of a recognizer in $A$ and a recognized element in $B$), then $A$ is nonempty and $B$ is nonempty.
background
The ambient module develops Recognition Structure Necessity: any framework that extracts observables must support distinction and identification of states, culminating in a recognition structure. The strategy is three-step (observables imply distinction, distinction needs comparison, internal comparison is self-recognition), after which the Meta Principle (MP) forbids trivial empty recognition.
The core datatype is Recognize A B, the minimal recognizer→recognized pairing: a structure with fields recognizer : A and recognized : B. MP is stated upstream as: it is impossible for Nothing to recognize itself. This lemma is the purely structural half of that story: inhabitation of a pairing forces inhabitation of both carriers.
It sits among sibling facts such as MP_forbids_empty_recognition and ComparisonIsRecognition, which together turn measurement-style distinction into a forced recognition event with nonempty sides.
proof idea
Term-mode, two lines. From the hypothesis Nonempty (Recognize Recognizer Recognized), obtain a concrete witness r. The structure fields supply r.recognizer : Recognizer and r.recognized : Recognized, which are packaged as Nonempty Recognizer and Nonempty Recognized. No external lemmas beyond the structure definition of Recognize are required.
why it matters
This is a small but load-bearing gate in the necessity chain. Downstream, MP_essential_for_physics uses recognition necessity plus nonemptiness to conclude that nontrivial observables force a recognition pairing whose carriers are not both empty: "The Meta Principle is essential for non-trivial physics." Without this projection, one could posit a recognition event on empty types and evade MP.
In the module narrative it closes the MP half of Step 3: once comparison without external reference is identified with recognition, empty recognition is forbidden and both sides must carry actual states. That is the bridge from abstract distinction to a concrete, inhabited recognition structure required by any observable-deriving framework. It does not itself invoke the forcing chain T0–T8 or the RCL; it is pure verification infrastructure under MP.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.