Nothing
plain-language theorem explainer
Absolute nothing is encoded as the empty type: the unique type with no inhabitants. Foundation and cost-axiom developments cite it as the starting point of the T-2→T-1 forcing from nothing to distinction. The definition is a non-unfolding alias of Empty, kept as a def so the name stays opaque until explicitly expanded.
Claim. Absolute nothing is the empty type: $\mathsf{Nothing} := \emptyset$, the type with no inhabitants (the initial object of $\mathbf{Type}$).
background
The module closes the floor below the Recognition Science forcing chain (T-2 → T-1). Earlier absolute-floor work took meta-language proposition distinguishability and a non-singleton universe as given; here those preconditions are derived from the strongest encoding of absolute nothing, with no axioms.
Absolute nothing is the empty type: it has no inhabitants and a unique morphism into every type (elimination). Categorically it is the initial object—nothing inside, and maps into anything because there is no input to constrain. The module keeps the name as a definition rather than an abbreviation so it does not silently unfold; expansion is invoked only where needed.
Upstream, Recognition already had a thin abbreviation of the same empty type; this foundation definition reifies it as the named starting point of the nothing-to-distinction engine. The later forcing chain (T5–T8: J-uniqueness, φ, eight-tick, D = 3) sits above the Boolean distinction this floor produces.
proof idea
One-line definitional alias: Nothing is defined to be the empty type. No tactics, no lemmas. Opacity is intentional (def, not abbrev), so later proofs that need the empty-type API must unfold or transport explicitly.
why it matters
This is the seed of the T-2→T-1 forcing function. Naming nothing already places an object in Type, forcing Nonempty Type; Empty and Unit are then unequal, yielding the first distinction, from which object-, type-, and proposition-level distinctions follow with no premises. That discharges the meta-language fact the prior absolute floor assumed.
Downstream, cost axioms derive the Meta-Principle (“nothing cannot recognize itself”) by reading Nothing as the x → 0 limit where J diverges, and prove unity is the unique existent. Economic inevitability packages non-negative defect, unique zero at 1, infinite cost of nothing, and forced φ. Inevitability scaffolding counts and Law-of-Existence defect lemmas also consume the name. In the primer landmarks this sits strictly below T0–T8: it supplies the Boolean distinction the public bridge consumes, without importing the later spine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.