Foundation Nothing To Distinction Nothing Ne Something

The first distinction

In mathematics, the empty type is the type with no inhabitants at all, and the unit type is the type with exactly one inhabitant. The Recognition Science framework's declaration nothing_ne_something is a machine-checked proof that these two types are distinct: the type with no members is not the same as the type with one member. The proof works by contradiction. If the two types were identical, the single inhabitant of the unit type could be transported across that equality into the empty type, producing an inhabitant of a type that by definition has none, which is impossible.

This theorem is the concrete anchor of a more general floor for the framework, called T-1: the claim that there exist two distinct types and two distinct propositions. The framework needs this floor because its entire structure, the ledger of recognition events and the cost forced on them, depends on being able to make distinctions. Nothing being distinct from something is the extremal case, the widest possible gap between two types, so it serves as the chosen witness for the type half of that floor. The framework's library proves this in a formal system that reports no axioms beyond the ambient type theory's standard postulates; the audit is a statement about postulates, not a claim that the result stands on nothing.

What the theorem does not claim is equally precise. It does not derive distinction from its own absence; writing down there is no distinction already requires the sentence and the thing it denies. The framework makes no such move. It also does not sit beneath the T-1 floor as a further foundation. T-1 is the absolute floor, and nothing_ne_something is one witness of it, not a rung below it. The framework's actual constructive claim about the initial object of its distinction signature, that it is rigid and unique up to unique isomorphism, is proved elsewhere.

/-- T-2 as a witness for the type half of the T-1 floor. -/
theorem type_floor_witness : ∃ α β : Type, α ≠ β :=
  ⟨Nothing, Something, nothing_ne_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

This theorem does not derive distinction from its own absence. This theorem is not a rung below the T-1 floor, but a witness of it. This theorem does not establish the framework's constructive claims about rigidity or uniqueness of its initial object.

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: