of
plain-language theorem explainer
Absolute nothing, encoded as the empty type, is unstable under bare naming: writing it populates a higher universe and forces a first distinction from the unit type. The result discharges the meta-language distinguishability that AbsoluteFloorClosure previously assumed as a precondition. Anyone citing the T-2 floor or the start of the RS forcing chain needs this. The argument is pure type theory: initial versus terminal object, with no classical or RS-specific postulate.
Claim. From the empty type alone (absolute nothing: no inhabitants, unique map into every type), bare type formation with no classical or Recognition-Science postulate forces a nonempty universe of types and a first distinction: the initial object is not identical to the terminal object. Object-level, type-level, and propositional distinctions then follow with empty premise.
background
This module sits one floor below the existing absolute floor. AbsoluteFloorClosure took meta-language proposition distinguishability ($\exists P,Q:\mathrm{Prop},, P\neq Q$) and a non-singleton universe as given. Here those preconditions are derived from the strongest encoding of absolute nothing, using no axioms.
Absolute nothing is the empty type: no inhabitants, and a unique eliminator into every type (the categorical initial object). The module keeps this as a named definition so it does not silently unfold. Something is the unit type (terminal object), which has a single inhabitant.
The local engine is a forcing function, not an extra assumption: naming nothing at universe level $n$ makes it an object at level $n+1$, so the universe of types becomes inhabited; once both initial and terminal objects exist they cannot be identified, because transport would place an inhabitant in the empty type.
proof idea
No separate tactic script is attached in the extract; the module's forcing chain is the proof shape.
- Naming the empty type witnesses that
Typeis nonempty (nothing reflects upward into something). - With the initial object present, the terminal object is admitted; they are unequal because any equality would transport the unit inhabitant into the empty type, which is impossible.
- From that first inequality one obtains object distinction ($\exists x,y,, x\neq y$), type distinction ($\exists\alpha,\beta,, \alpha\neq\beta$), and propositional distinction ($\exists P,Q:\mathrm{Prop},, P\neq Q$) as theorems with no premise.
- The forced Boolean distinction is the floor consumed by the public T-1 bridge; this file stops at T-2/T-1 and does not import the later spine.
why it matters
Closes the last floor under the Recognition Science forcing chain. The prior absolute floor assumed proposition distinguishability and a non-singleton universe; those are now theorems derived from absolute nothing alone, so the chain no longer rests on a meta-language postulate at that level.
Downstream, the forced Boolean distinction is the input the public T-1 through T8 bridge consumes (J-uniqueness, $\varphi$ as self-similar fixed point, eight-tick octave, $D=3$). This file intentionally does not import that spine; it only hands off the T-1 floor.
No used-by edges are recorded for this declaration in the graph extract, so its role is foundational setup rather than a lemma cited inside later proofs. It is the zero-postulate entry point for distinction itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.