nothing_ne_something
plain-language theorem explainer
Absolute nothing (the empty type) is necessarily unequal to the minimal something (the unit type). Identifying them would transport the unique inhabitant of Unit into Empty, which is impossible. Anyone citing the T-2/T-1 floor or the first forced distinction uses this inequality. The proof is a short contradiction via transport and Empty.elim, with no premises.
Claim. The empty type $\mathsf{Empty}$ (absolute nothing) is not definitionally or propositionally equal to the unit type $\mathsf{Unit}$ (the minimal something): $\mathsf{Empty} \neq \mathsf{Unit}$.
background
This module sits at the T-2 → T-1 floor of Recognition Science: it derives distinction from the strongest encoding of absolute nothing, using no axioms. Absolute nothing is encoded as the empty type Empty (here named Nothing): it has no inhabitants and is initial, with a unique map Empty.elim into every type. The minimal something is the terminal object Unit (here named Something), which has exactly one inhabitant ().
The module doc states the forcing engine: naming nothing already populates the universe (Nonempty Type), and once both the initial and terminal objects exist they cannot coincide. Prior absolute-floor work took propositional distinguishability as a precondition; this file derives it. The two local definitions are kept as defs so the names do not silently unfold.
proof idea
Assume h : Nothing = Something. Rewrite along h to obtain Nonempty Nothing from the canonical inhabitant of Something (Unit), namely ⟨()⟩. Unpack that nonempty witness to an element e : Nothing. Since Nothing is Empty, Empty.elim e discharges the goal. The argument is pure transport-plus-elimination; no external lemmas are required beyond the definitions of the two types.
why it matters
This is the first distinction in the Recognition forcing chain: the inequality that turns absolute nothing into a typed pair of unequal objects. Downstream, type_distinction_forced packages it as ∃ α β : Type, α ≠ β, and nothingForcesDistinction states the forcing arrow from IsEmpty Nothing to that existential. Those results discharge the meta-language precondition previously assumed by AbsoluteFloorClosure, closing the last floor below T-1 through T8. In the primer landmarks this is pre-T0 groundwork: without a forced distinction there is no ledger, no J-cost, and no path to phi, the eight-tick octave, or D = 3. 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.