Foundation Distinguishability From Specifiability Specifiability Closure Cert

The specifiability certificate

In logic and mathematics, a specification is a rule that picks out some objects and excludes others. A non-trivial specification is one that actually does both: it names at least one object that satisfies the rule and at least one that does not. The framework's machine-checked library of formal theorems contains a small but sharp result about this idea. It proves that on any inhabited carrier, meaning any non-empty collection of objects, the existence of a non-trivial specification is exactly equivalent to the existence of two distinct objects in that collection.

The proof is direct and does not depend on any special assumptions. Suppose a specification holds for some object x and fails for some object y. If x and y were the same object, then the specification would both hold and fail for that single object, which is impossible. Therefore x and y must be distinct. The reverse direction is equally simple: if two distinct objects exist, then the rule that holds for exactly one of them is a non-trivial specification. The framework packages this equivalence into a structure it calls the specifiability closure certificate, a formal record that the two notions, specifiability and distinguishability, are the same floor.

This certificate matters because the framework's broader program tries to show that certain basic distinctions are forced rather than chosen. The result establishes that the ability to specify an ontology with something inside and something outside already gives you the distinction the program needs. It is a route to distinguishability that does not presuppose any particular structure on the carrier, only that the carrier is non-empty and that a non-trivial specification exists.

The certificate does not claim that any particular specification exists, only that if one does, distinct objects follow. It does not establish that the carrier has any particular size beyond being non-singleton, and it says nothing about what the objects are or how they relate. The result is purely logical: it connects two ways of saying that a collection is not a single undifferentiated point.

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

/-- Route B certificate: specifiability is exactly the same floor as a
non-singleton universe of discourse. -/
structure SpecifiabilityClosureCert (K : Type*) [Nonempty K] : Prop where
  equivalence :
    (∃ x y : K, x ≠ y) ↔ Nonempty (NontrivialSpecification K)

What this page does not claim

The certificate does not establish that any non-trivial specification actually exists. The certificate does not determine how many distinct objects exist beyond requiring at least two. The certificate does not connect specifiability to the cost function or the golden ratio in this file.

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: