naming_nothing_populates_universe
plain-language theorem explainer
Denoting absolute nothing (the empty type) immediately yields a witness that the universe of types is inhabited. Anyone citing the T-2→T-1 floor closure uses this as the irreversible first step: naming nothing at one level makes it an object at the level above. The proof is a one-line term witness: the empty type itself inhabits `Type`.
Claim. The universe of types is nonempty: $\mathrm{Nonempty}(\mathbf{Type})$. Explicitly, absolute nothing (the empty type) is itself a type, so $\mathbf{Type}$ has at least one inhabitant.
background
This module closes the floor below the Recognition Science forcing chain (T-2 → T-1). Earlier absolute-floor work took a non-singleton universe and propositional distinguishability as given; here both are derived from the strongest encoding of absolute nothing, with no axioms.
Absolute nothing is encoded as the empty type: no inhabitants, and a unique map into every type (the initial object). In this file it is named Nothing and defined to be Empty, kept as a definition so the name does not silently unfold.
The forcing engine begins here. To name nothing is already to place an object in Type. That single act populates the universe and is the irreversible first step toward the first distinction (nothing versus the terminal object) and the Boolean floor consumed by the public T-1–T8 bridge.
proof idea
One-line term proof. Nonempty Type is the proposition that there exists an inhabitant of Type. The proof supplies that inhabitant directly: absolute nothing (Nothing, i.e. the empty type) has type Type, so the pair constructor ⟨Nothing⟩ witnesses non-emptiness. No lemmas, no tactics, no unfolding beyond the definitional fact that nothing is a type.
why it matters
This is step 1 of the module's forcing function from absolute nothing to distinction. Downstream it is wired into nothingToDistinctionCert as the universe_populated field, alongside the forced type-, prop-, object-, and Boolean distinctions. That certificate discharges the preconditions the prior absolute floor had assumed, so the public T-1 through T8 chain no longer rests on an unproved non-singleton universe.
In framework terms it is the lowest rung below T0–T8: before J-uniqueness, φ, the eight-tick octave, or D = 3, one must already have a populated type universe. Naming nothing forces that population. The file deliberately stops at T-2/T-1 and does not import the later spine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.