Foundation Distinguishability From Specifiability Distinguishability Iff Nontriv

The specification floor

A specification is a rule that sorts objects into two groups: those inside a chosen collection and those outside it. A non-trivial specification is one where both groups are non-empty: the rule admits at least one object and rejects at least one. In plain terms, it is a boundary that has something on each side.

The formal result is an equivalence. On any inhabited universe of discourse, the existence of two distinct objects is logically equivalent to the existence of a non-trivial specification. If you have two different things, you can define a rule that puts one inside and the other outside. Conversely, if a rule separates at least one object from at least one other, those two objects are distinct. The proof is short: the separating rule supplies the two witnesses of distinctness directly.

This equivalence has a structural consequence. If a carrier has no non-trivial specification, then it cannot contain two distinct elements; it has at most one. A universe with exactly one object cannot support any boundary, because there is nothing to exclude. The capacity to specify a sub-ontology is therefore the same capacity as having a non-singleton universe.

In Recognition Science, this result is a floor for the framework's ledger, a discrete record of events. The framework's machinery requires distinguishability among objects before it can assign cost or track recognition events. The theorem shows that the ability to specify an ontology already delivers that required distinction. A framework that can describe something inside and something outside already possesses the elementary separation its logic needs.

The declaration does not claim that specification creates objects, nor that it explains why any particular objects exist. It only states an equivalence: given a universe that is inhabited, the existence of a non-trivial specification and the existence of two distinct elements are the same fact. The theorem is a logical bridge, not a metaphysical one.

/-- A non-trivial specification of a sub-ontology inside a universe of
discourse `K`: a predicate that holds for at least one element and fails
for at least one element. -/
structure NontrivialSpecification (K : Type*) where
  inOntology : K → Prop
  someInside : ∃ x : K, inOntology x
  someOutside : ∃ x : K, ¬ inOntology x

/-- 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

/-- 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⟩ }⟩

What this page does not claim

The theorem does not claim that specification creates objects or explains why any particular objects exist. The theorem does not claim that a singleton universe is impossible, only that it cannot support a non-trivial specification. The theorem does not claim that distinguishability is sufficient for the full Recognition Science framework, only that it is equivalent to non-trivial specifiability.

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: