Foundation Distinguishability From Specifiability Nontrivial Specification Of Pr

Specification and distinction

In mathematics, a specification is a rule that picks out some elements of a collection and leaves others out. The declaration nontrivial_specification_of_proper_subtype concerns a special kind of specification: one where the rule holds for at least one element and fails for at least one element. The statement is that such a specification, on any collection, immediately yields two distinct elements. The proof is direct: if the rule holds for some x and fails for some y, then x and y cannot be the same object, because a single object cannot both satisfy and fail the same rule.

The declaration constructs a ledger, a discrete record of events or objects, from a proper non-empty subset of a universe of discourse. If a framework can specify an ontology with something inside and something outside, it already has the distinction needed by the Law-of-Logic chain. The formal statement is: given a set S with an element in it and an element not in it, the predicate "is in S" forms a non-trivial specification. This is a definitional construction, not a theorem about the physical world; it shows that the abstract ability to specify a boundary between inside and outside already implies the existence of at least two distinct objects.

The result is part of a larger equivalence in the framework's machine-checked library of formal theorems. On any inhabited collection, the existence of two distinct elements is equivalent to the existence of a non-trivial specification. This equivalence is a proved theorem, not a definitional choice. It means that the ability to distinguish objects and the ability to specify a non-trivial subset are the same logical floor. The certificate structure bundles this equivalence as a formal object, and the theorem backing it is the equivalence itself.

What the declaration does not claim is equally sharp. It does not claim that any particular physical system has two distinct elements; it only shows that if a specification exists, then distinction follows. It does not claim that the specification is unique or that the two elements are named; it only asserts their existence. The construction is purely logical, with no empirical content about which objects exist in the world.

/-- Any non-empty proper subtype is a non-trivial specification. -/
def nontrivial_specification_of_proper_subtype
    {K : Type*} (S : Set K)
    (hin : ∃ x : K, x ∈ S) (hout : ∃ x : K, x ∉ S) :
    NontrivialSpecification K where
  inOntology := fun x => x ∈ S
  someInside := hin
  someOutside := hout

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

/-- The specifiability closure certificate is theorem-backed. -/
theorem specifiabilityClosureCert (K : Type*) [Nonempty K] :
    SpecifiabilityClosureCert K where
  equivalence := distinguishability_iff_nontrivial_specifiability

What this page does not claim

No claim that any particular physical system has two distinct elements. No claim that the specification is unique or that the two elements are named. No empirical content about which objects exist in the world.

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: