Foundation Distinguishability From Specifiability Nontrivial Specification

The specification floor

In mathematics, a specification is a rule that draws a line inside a collection of objects, marking some as belonging and others as not. The Recognition Science declaration NontrivialSpecification formalizes the simplest possible version of this idea. It takes a universe of discourse, a set of objects under discussion, and asks for three things: a predicate that labels objects, at least one object that satisfies the predicate, and at least one object that does not. That is all. The declaration does not require the predicate to be computable, natural, or useful; it only requires that the line is drawn somewhere and that both sides are occupied.

The force of this small definition comes from a proved theorem. In the framework's machine-checked library of formal theorems, the theorem distinguishability_from_specification derives that any such non-trivial specification yields two distinct objects. If a predicate holds for one element and fails for another, those two elements cannot be the same, because a single object cannot both satisfy and fail the same predicate. The proof is a short argument by contradiction, and the framework records it as a fully checked theorem with no gaps.

The framework then sharpens this observation into an equivalence. On any inhabited carrier, the existence of a non-trivial specification is exactly equivalent to the existence of two distinct elements. The theorem distinguishability_iff_nontrivial_specifiability states this biconditional, and the certificate structure SpecifiabilityClosureCert packages it as a single reusable fact. The framework calls this Route B for its absolute-floor program: it shows that the ability to specify an ontology with something inside and something outside already supplies the distinction that its Law-of-Logic chain needs.

In Recognition Science, this result plays a specific role. The framework models reality as a discrete record of events, and it aims to derive physical structure from the forced cost of recognition. The equivalence here establishes that specification, not raw counting, is enough to get distinguishability off the ground. If a framework can describe a category with members and non-members, it already has two distinct objects, and from that point the framework's forcing chain can proceed.

What the declaration does not claim is equally precise. It does not claim that any particular specification is meaningful, only that a non-trivial one exists. It does not claim that the two distinct objects are physical particles or events; they are abstract elements of a type. It does not claim that specification causes distinguishability in a temporal sense; the equivalence is logical, not causal. The declaration is a floor, not a building.

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

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

The declaration does not claim any particular specification is meaningful or natural. It does not claim the two distinct objects are physical particles or events. It does not claim specification causes distinguishability in a temporal sense.

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: