Something
plain-language theorem explainer
Defines the minimal something as the unit type: the terminal object with exactly one inhabitant. Paired with absolute nothing (the empty type), it supplies the first forced distinction in the T-2→T-1 floor. Downstream lemmas cite it to prove nothing ≠ something and to discharge type-, object-, and proposition-level distinctions with no premises. The body is a one-line type synonym.
Claim. Let $\mathrm{Something}$ be the unit type $\mathbf{1}$ (equivalently $\mathrm{Unit}$): the terminal object of $\mathbf{Type}$, which has exactly one inhabitant $()$.
background
The module closes the floor beneath the Recognition Science forcing chain (T-2 → T-1). Absolute nothing is encoded as the empty type: the initial object with no inhabitants and a unique map into every type. Naming that empty type already populates the universe of types, so Type is nonempty.
Once Type contains the initial object, it also admits the terminal object. The present definition simply names that terminal object. Its single inhabitant is the canonical point $()$. The module then shows that the initial and terminal objects cannot be identified: transporting the point of the terminal object into the empty type is impossible. That inequality is the first distinction; type-level, object-level, and propositional distinctions all follow with no extra hypotheses.
proof idea
Pure definitional abbreviation: Something is declared equal to Unit. No proof obligations arise. Downstream theorems (something_has_object, nothing_ne_something) immediately exploit the single constructor () and Empty.elim.
why it matters
Supplies the positive pole of the first forced distinction. nothing_ne_something, type_distinction_forced, and nothingForcesDistinction all pair Nothing with Something to obtain ∃ α β, α ≠ β from the emptiness of Nothing alone. That type distinction discharges the meta-language precondition previously assumed by AbsoluteFloorClosure, closing T-2 into T-1. The Boolean distinction produced here is the floor consumed by the public T-1–T8 bridge and by the LogicFromCost summaries (mp_from_cost_and_logic, logic_from_cost_summary) that derive the Meta-Principle from cost and consistency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.