nothing_eliminates
plain-language theorem explainer
Absolute nothing admits a map into every sort: the empty-type eliminator. Workers on the T-2 floor of the Recognition forcing chain cite this as the categorical signature of the initial object. The body is a one-line wrapper around Empty.elim, with no extra hypotheses.
Claim. For every sort $C$, there is a map $\mathrm{Nothing} \to C$ given by empty elimination. Absolute nothing (the type with no inhabitants) is initial: it maps into every target because there is no element that could constrain the map.
background
The module closes the floor below the Recognition Science forcing chain (T-2 to T-1). Absolute nothing is encoded as the empty type: Nothing is defined to be Empty, the type with no inhabitants. That encoding is the strongest formal stand-in for "there is no object."
Categorically, the empty type is the initial object. Its defining property is a unique morphism into every target type, obtained by empty elimination: from a hypothetical inhabitant of Nothing one may conclude anything. The module doc states this signature explicitly: nothing maps into everything because there is no input to constrain the map.
Upstream, the sibling definition of Nothing keeps the name as a def (not an abbrev) so unfolding is deliberate. The later engine of the file uses that initiality together with the fact that naming Empty already places an object in Type, forcing the first distinction.
proof idea
One-line definitional wrapper. The body is fun e => Empty.elim e: given a hypothetical inhabitant of Nothing (which is Empty), apply the standard empty eliminator to inhabit the arbitrary target sort C. No lemmas beyond the kernel eliminator are required.
why it matters
This definition is the categorical half of the absolute-nothing encoding that the module uses to discharge preconditions previously assumed by AbsoluteFloorClosure. The module derives nonempty Type, the inequality Nothing \neq Unit, and then object-, type-, and proposition-level distinctions with no axioms; the unique arrow out of nothing is the initial-object half of that signature.
It sits at the T-2/T-1 floor and does not import the later T0-T8 spine. Downstream siblings in the same file (naming_nothing_populates_universe, nothing_ne_something, type_distinction_forced, prop_distinction_forced, bool_distinction_from_nothing) build the forcing function that turns this initiality into the first distinction consumed by the public bridge. No external used_by edges are recorded yet; the declaration is local foundation scaffolding for that engine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.