type_distinction_forced
plain-language theorem explainer
Type-level distinction is forced: there exist two unequal types. The witnesses are absolute nothing (Empty) and the terminal object (Unit). Anyone discharging AbsoluteFloorWitness preconditions or assembling NothingToDistinctionCert cites this. The proof is a one-line existential introduction via the already-proved inequality Nothing ≠ Something.
Claim. There exist types $\alpha$ and $\beta$ such that $\alpha \neq \beta$. The witnesses are absolute nothing (the empty type) and the minimal something (the unit type), which are necessarily unequal.
background
This module sits at the T-2 → T-1 floor of the Recognition Science forcing chain. The prior absolute floor took meta-language proposition distinguishability and a non-singleton universe as given preconditions; here those are derived from the strongest encoding of absolute nothing, with no axioms.
Absolute nothing is encoded as the empty type: no inhabitants, unique morphism into every type (the initial object). Naming it already places an object in Type, so the universe is populated. The minimal something is the terminal object (unit type), with exactly one inhabitant.
The upstream inequality states that nothing and something are necessarily different types: identifying them would transport the unit inhabitant into the empty type, which is impossible. That is the first distinction; type-level, object-level, and propositional distinctions all follow from it.
proof idea
One-line term proof. The existential is introduced by the pair of types Nothing (def equal to Empty) and Something (def equal to Unit), with the inequality supplied by the already-proved theorem nothing_ne_something. No tactics, no further lemmas.
why it matters
This is one of the four distinction fields packed into nothingToDistinctionCert (universe populated, type distinction, prop distinction, object distinction, bool distinction). That certificate is the theorem-backed discharge of the preconditions AbsoluteFloorWitness previously assumed: meta-language proposition distinguishability and nontrivial specification.
In the forcing narrative, type-level distinction is step 3 of the engine that runs from absolute nothing to the Boolean floor consumed by the public T-1 through T8 bridge. The module itself stays at T-2/T-1 and does not import the later spine (J-uniqueness, phi, eight-tick, D = 3). Closing this floor means the absolute floor is no longer an external hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.