Foundation Nothing To Distinction Nothing Eliminates

The empty type's one power

The empty type is the type with no inhabitants. It is the type-theoretic counterpart of the number zero, the empty set, or the false proposition: it exists, but nothing lives inside it. The declaration nothing_eliminates states that from a value of the empty type, one can construct a value of any type. This is the principle of explosion, also called ex falso quodlibet: from a contradiction, anything follows. In the Recognition Science library, this is not a new axiom but a definition, built from the standard eliminator for the empty type.

The definition is short: for any type C, a function from the empty type to C exists. Because the empty type has no elements, the function has no cases to handle, so it is vacuously defined. The library names this function nothing_eliminates, and it is the unique such function, a fact that follows from the universal property of the empty type as the initial object in the category of types. This uniqueness matters: it means the empty type's behavior is fully determined, with no choices to make.

The library also proves two companion facts. The theorem nothing_has_no_object states that the empty type is indeed empty, and the theorem something_has_object states that the unit type, the type with exactly one inhabitant, is nonempty. Together with nothing_eliminates, these support the theorem nothing_ne_something, which states that the empty type and the unit type are distinct. This distinction is the type-theoretic floor: it witnesses that the ambient category of types is nondegenerate, that not everything collapses into the same thing.

In Recognition Science, this declaration anchors the framework's starting point. The framework models reality as maintaining a ledger, a discrete record of recognition events, and it needs a base against which all distinctions are measured. The empty type serves as that base, the extremal object from which cost is measured. The declaration nothing_eliminates establishes the mechanical fact that makes this base usable: from nothing, one can derive anything, vacuously, without adding content. It is the concrete anchor of the floor, not a rung below it.

What nothing_eliminates does not claim is broader than what it does. It does not claim that distinction arises from nothing, or that the framework derives its structure from the absence of structure. The declaration is a formal fact about the empty type, not a metaphysical statement about creation. It does not claim that the empty type is the same as the unit type, nor does it claim that the framework's cost function or its forcing chain follows from this declaration alone. The framework's deeper theorems, such as the uniqueness of the cost function and the derivation of the golden ratio, are proved elsewhere, from the five conditions on cost, not from this single declaration.

/-- The unique morphism out of the initial object. -/
def nothing_eliminates {C : Sort _} : Nothing → C :=
  fun e => Empty.elim e

theorem nothing_has_no_object : IsEmpty Nothing :=
  ⟨fun e => Empty.elim e⟩

theorem something_has_object : Nonempty Something :=
  ⟨()⟩

/-- **T-2.** The initial and terminal objects are distinct. Identifying them
would transport the inhabitant of `Unit` into `Empty`. -/
theorem nothing_ne_something : Nothing ≠ Something := by
  intro h
  have hn : Nonempty Nothing := by
    rw [h]; exact ⟨()⟩
  obtain ⟨e⟩ := hn
  exact Empty.elim e

What this page does not claim

Nothing_eliminates does not claim that distinction arises from nothing, only that from an empty type a value of any type can be constructed. The declaration does not derive the framework's cost function or its forcing chain; those are proved from five conditions elsewhere. The theorem does not claim the empty type and the unit type are the same; it proves they are distinct.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/NothingToDistinction.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: