Foundation Distinguishability From Specifiability At Most One Of No Nontrivial S

The specifiability floor

A specification is a rule that sorts the things in a universe into those that satisfy the rule and those that do not. A nontrivial specification is one that puts at least one thing inside and at least one thing outside. The declaration at_most_one_of_no_nontrivial_specification proves a small but sharp fact: if a nonempty universe admits no nontrivial specification, then every two things in it are equal. In other words, the only way to escape having at least two distinct objects is to have no rule that draws a line through the universe.

The proof is a short argument by contradiction. Suppose the universe has two distinct things, call them x and y. Then the rule “is equal to x” puts x inside and y outside, so it is a nontrivial specification. Since the declaration assumes no such specification exists, the supposition of two distinct things must fail. Hence all things are equal. The formal statement lives in the machine-checked library of formal theorems under IndisputableMonolith/Foundation/DistinguishabilityFromSpecifiability.lean.

This result is the converse of a companion theorem: any nontrivial specification already gives you two distinct objects, one inside and one outside. Taken together, the two directions form an equivalence. On a nonempty carrier, the existence of a nontrivial specification is exactly equivalent to the existence of two distinct elements. The framework calls this the specifiability floor: the ability to specify a proper part and the ability to distinguish two objects are the same underlying capacity.

What the declaration does not claim is just as important. It does not say that a universe with no nontrivial specification is empty; it only says it has at most one element. It does not construct a specification from scratch; it assumes one exists or proves one does not. And it does not say anything about what the two distinct objects are, only that they exist. The theorem is about the logical floor, not about any particular ontology.

/-- If no non-trivial specification exists on an inhabited carrier, then the
carrier has at most one element. -/
theorem at_most_one_of_no_nontrivial_specification
    {K : Type*} [Nonempty K]
    (h_no_nts : ¬ Nonempty (NontrivialSpecification K)) :
    ∀ x y : K, x = y := by
  intro x y
  by_contra hxy
  apply h_no_nts
  have hy_ne_x : y ≠ x := by
    intro hyx
    exact hxy hyx.symm
  exact ⟨
    { inOntology := fun z => z = x
      someInside := ⟨x, rfl⟩
      someOutside := ⟨y, hy_ne_x⟩ }⟩

/-- Specifiability forces distinguishability. -/
theorem distinguishability_from_specification
    {K : Type*} (S : NontrivialSpecification K) :
    ∃ x y : K, x ≠ y := by
  obtain ⟨P, ⟨x, hx⟩, ⟨y, hy⟩⟩ := S
  refine ⟨x, y, ?_⟩
  intro hxy
  have hyx : P y := by
    simpa [hxy] using hx
  exact hy hyx

/-- Non-trivial specifiability is equivalent to object-level
distinguishability on an inhabited carrier. -/
theorem distinguishability_iff_nontrivial_specifiability
    {K : Type*} [Nonempty K] :
    (∃ x y : K, x ≠ y) ↔ Nonempty (NontrivialSpecification K) := by
  constructor
  · rintro ⟨x, y, hxy⟩
    have hy_ne_x : y ≠ x := by
      intro hyx
      exact hxy hyx.symm
    exact ⟨
      { inOntology := fun z => z = x
        someInside := ⟨x, rfl⟩
        someOutside := ⟨y, hy_ne_x⟩ }⟩
  · rintro ⟨S⟩
    exact distinguishability_from_specification S

What this page does not claim

The theorem does not claim the universe is empty; it only claims at most one element. The theorem does not construct a specification from nothing; it assumes one exists or proves none does. The theorem does not identify which two distinct objects exist, only that they do.

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/DistinguishabilityFromSpecifiability.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: