something_has_object
plain-language theorem explainer
The minimal something (the terminal type, Unit) is inhabited. Anyone building the first distinction between absolute nothing and something cites this witness. The proof is a one-constructor term: the unique unit value.
Claim. The type Something, defined as the unit type, is nonempty: there exists an inhabitant of Something.
background
This module closes the floor below the Recognition Science forcing chain (T-2 to T-1). Absolute nothing is encoded as the empty type: no inhabitants, unique map into every type. The minimal something is the terminal object: exactly one inhabitant.
Something is defined as Unit. The companion Nothing is Empty. Naming nothing already populates a universe (Type is nonempty), after which both the initial and terminal objects sit in that universe. Their inequality is the first distinction; the present theorem supplies the positive side of that pair.
The absolute-floor closure previously took propositional distinguishability as a precondition. Here the precondition is derived from the empty type with no axioms.
proof idea
Term-mode proof. Something unfolds to Unit, so Nonempty Something is witnessed by the unique constructor of Unit: the unit value. No lemmas are applied; the inhabitant is written directly as an anonymous constructor.
why it matters
Supplies the positive witness in the first distinction: Nothing has no object, Something has one. The sibling inequality Nothing ≠ Something then follows because any identification would transport the unit inhabitant into Empty, which is impossible. From that inequality the module derives object-level, type-level, and propositional distinctions with no premise, discharging the meta-language fact AbsoluteFloorClosure assumed. The forced Boolean distinction is the floor consumed by the public T-1 through T8 bridge; this file stays at T-2/T-1. No downstream consumers are recorded yet in the graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.