We formalize and prove a single theorem in a standard dependent type setting: there is no term of type Recognition(Nothing, Nothing). The result follows immediately from the definitions (the empty type has no inhabitants), and we provide a Lean proof with an archived, pinned artifact. We state the intended interpretation and its limits: types denote sorts of possible entities, terms denote existents, and the empty type denotes a sort with no existents. Under this conventional interpretation, the theorem says that a recognition event requires existents and therefore cannot arise from emptiness. This note focuses on the formal theorem and reproducibility; broader physical consequences are deferred to a companion work.