nothing_has_no_object
plain-language theorem explainer
Absolute nothing, encoded as the empty type, has no inhabitants. Foundation work on the T-2→T-1 floor cites this as the categorical emptiness witness before naming forces a higher-universe object. The proof is a one-line term that packages Empty-elimination into an IsEmpty structure.
Claim. The type $\mathsf{Nothing}$ (defined as the empty type) is empty: there is no inhabitant $e : \mathsf{Nothing}$. Equivalently, $\mathsf{IsEmpty}(\mathsf{Nothing})$ holds.
background
This module sits at the absolute floor of Recognition Science: it derives distinction from the strongest encoding of nothing, with no axioms, closing preconditions that AbsoluteFloorClosure previously took as given.
Absolute nothing is the empty type. In-module, Nothing is a def equal to Empty (kept as a def so the name does not silently unfold). Categorically it is the initial object: no inhabitants, and a unique morphism into every type via elimination.
IsEmpty α is the standard Mathlib witness that a type has no elements. The doc-comment stresses the reflexive point: the witness that nothing is empty is already an object, so asserting emptiness produces something.
proof idea
Term-mode construction of an IsEmpty structure. The single field is a function Nothing → False (or the empty type). Any hypothetical inhabitant e is eliminated by Empty.elim e after unfolding Nothing := Empty. No lemmas beyond empty-type elimination are required.
why it matters
This is the first concrete fact about the encoding of absolute nothing in the T-2→T-1 forcing function. The module engine is: name nothing → populate Type → obtain Unit as something → force Nothing ≠ Unit → derive object-, type-, and proposition-level distinctions, discharging the meta-language precondition of the prior absolute floor.
Sibling theorems (nothing_eliminates, naming_nothing_populates_universe, nothing_ne_something, type_distinction_forced, prop_distinction_forced, bool_distinction_from_nothing) build on emptiness. The Boolean distinction is the floor consumed by the public T-1 through T8 bridge; this file stays at T-2/T-1. No downstream edges are recorded yet for this exact lemma, but it is the emptiness half of the initial-object signature used throughout the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.