nothingForcesDistinction
plain-language theorem explainer
From emptiness of absolute nothing, a type-level distinction is forced: two unequal types exist. Foundation authors of the T-2→T-1 bridge cite this as the forcing arrow itself. The proof is a one-line existential packing Nothing, Something, and their already-proved inequality.
Claim. If absolute nothing (the empty type) is empty, then there exist types $\alpha$ and $\beta$ such that $\alpha \neq \beta$.
background
This module sits at T-2→T-1, the floor below the Recognition Science forcing chain. Absolute nothing is encoded as the empty type: no inhabitants, unique map into every type (the initial object). The module defines Nothing as that empty type and Something as the terminal object (unit type, one inhabitant).
The prior absolute-floor development took meta-language proposition distinguishability and a non-singleton universe as given preconditions. Here those are derived from nothing with no axioms. Naming nothing already populates the universe of types; once both the initial and terminal objects sit in that universe, they cannot be identified, because transport would push the unit inhabitant into the empty type.
Upstream, nothing_ne_something records that first inequality with no premise: identifying Nothing with Something yields a nonempty empty type, which is absurd. Propositional distinction (True ≠ False) and Boolean distinction are derived siblings.
proof idea
Pure term proof. The existential is witnessed by the pair of types Nothing and Something; the inequality proof obligation is discharged by the already-established lemma nothing_ne_something. The hypothesis that Nothing is empty is unused in the term (it is the conceptual premise of the forcing arrow, not a computational input). No tactics, no further lemmas.
why it matters
This is the forcing function of the module: emptiness of nothing produces a distinction. It closes the last floor under the RS chain by deriving, rather than assuming, the type-level distinction that AbsoluteFloorClosure previously took as a meta-language precondition. Downstream in the same file, the absolute-floor Bool witness has its meta_distinguishes field supplied by the sibling propositional distinction, now discharged from nothing. The forced Boolean distinction is the floor consumed by the public T-1 through T8 bridge; this declaration stays at T-2/T-1 and does not import the later spine (T5 J-uniqueness, T6 phi, T7 eight-tick, T8 D=3).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.