MP_forbids_empty_recognition
plain-language theorem explainer
Empty self-recognition is impossible: there is no recognizer–recognized pair whose carrier types are both empty. Anyone arguing that the Meta Principle forces non-trivial recognition structure cites this. The proof is a one-step emptiness argument: assume such a pair, then case-split on its recognizer field, which inhabits the empty type.
Claim. There is no recognition pairing $r$ with both the recognizer and the recognized drawn from the empty type. Equivalently, $\neg\exists\, r:\mathrm{Recognize}(\emptyset,\emptyset)$ (the side condition $r.\mathrm{recognizer}=r.\mathrm{recognizer}$ is tautological and only forces existence).
background
The ambient module develops Recognition Structure Necessity: any framework that extracts observables must support distinction and identification of states, i.e. a recognition structure. The strategy is distinction from measurability, comparison as the mechanism of distinction, and internal comparison as self-recognition; the Meta Principle then rules out the trivial empty case.
A recognition pairing is the minimal structure Recognize A B with fields recognizer : A and recognized : B. The Meta Principle (MP) is the proposition that nothing cannot recognize itself: $\neg\exists,:,\mathrm{Recognize}(\mathrm{Nothing},\mathrm{Nothing})$. Here the empty type plays the role of that trivial carrier.
Upstream, MP and Recognize are the only substantive dependencies; the result is the empty-type specialization that the module summary invokes when it says MP forbids trivial empty recognition and forces non-trivial structure.
proof idea
Term/tactic hybrid, four lines. Introduce an assumed witness $\langle r,_\rangle$ of the existential (the equality on the recognizer is automatic). The field r.recognizer has type Empty. A single cases on that field discharges the goal, since the empty type has no constructors. No lemmas are applied; the argument is pure type emptiness, parallel in content to MP but stated for Lean Empty rather than the RS Nothing carrier.
why it matters
In the Recognition Necessity chain this is the MP-facing bolt: after observables force distinction and distinction forces internal comparison, one still needs that the resulting recognition structure cannot be vacuous. The module doc states explicitly that MP forbids trivial empty recognition and thereby forces non-trivial structure; this theorem is that prohibition written as a Lean fact about Recognize Empty Empty.
It sits beside siblings such as recognition_must_be_nonempty and observables_require_distinction, which assemble the larger claim that observable-bearing frameworks carry genuine recognition. No downstream uses are recorded yet, so its present role is foundational closure inside the necessity module rather than a lemma consumed by a named parent theorem. Relative to the broader RS forcing chain it is pre-physics: it secures the non-emptiness of recognition before J-cost, $\varphi$, eight-tick, or $D=3$ enter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.