Foundation Absolute Floor Closure Absolute Floor Iff Bare Distinguishability

The floor of distinction

The declaration absolute_floor_iff_bare_distinguishability is a formal theorem in the framework's machine-checked library of formal theorems. It states that, for any inhabited universe of discourse, the existence of two distinct elements is logically equivalent to the existence of a non-trivial specification. In plain terms: if you can point to two different things, you can specify something non-trivially; and if you can specify something non-trivially, then there must be at least two different things. The theorem is proved in both directions, so it is a genuine equivalence, not just a one-way implication.

The proof rests on two ingredients. First, the meta-language, the logical system in which the theorem is written, already distinguishes between true and false propositions; this is a basic feature of any classical logic. Second, the theorem connects this logical distinction to the existence of distinct elements in the universe of discourse. The minimal concrete example is the two-element type Bool, whose two values, false and true, are distinct. The library proves that this two-element world realizes the absolute floor: it is the smallest possible setting in which non-trivial specification can occur.

In Recognition Science, this theorem is called the absolute floor because it pins down the most basic precondition for the framework's ledger, a discrete record of events. The framework models a universe that keeps such a ledger, and the cost of recognition, the act of distinguishing one thing from another, is forced. This theorem shows that the floor of that program is not a physical postulate about space or time. It is the logical precondition that there is a non-singleton universe of discourse in which any non-vacuous specification can be stated. The theorem reduces the framework's foundational floor to two plain facts: the meta-language distinguishes propositions, and the universe of discourse has at least two elements.

What this theorem does not claim is equally important. It does not assert that the universe of discourse is physically non-singleton; that is a separate question about the actual world. It does not derive any specific physical content, such as the value of a constant or the number of dimensions. It only establishes the logical equivalence between bare distinguishability and non-trivial specifiability. The theorem is deliberately modest, and the framework's own documentation describes it as a joint certificate that reduces the forcing-chain floor to meta-language proposition distinguishability plus a non-singleton universe of discourse.

/-- Bare distinguishability and the absolute-floor witness are equivalent on
an inhabited carrier. -/
theorem absolute_floor_iff_bare_distinguishability
    {K : Type*} [Nonempty K] :
    AbsoluteFloorWitness K ↔ ∃ x y : K, x ≠ y :=
  ⟨bare_distinguishability_of_absolute_floor, absolute_floor_of_bare_distinguishability⟩

/-- Bare distinguishability and the absolute-floor witness are equivalent on
an inhabited carrier. -/
theorem absolute_floor_iff_bare_distinguishability
    {K : Type*} [Nonempty K] :
    AbsoluteFloorWitness K ↔ ∃ x y : K, x ≠ y :=
  ⟨bare_distinguishability_of_absolute_floor, absolute_floor_of_bare_distinguishability⟩

/-- The minimal concrete carrier `Bool` realizes the absolute floor. -/
theorem bool_absolute_floor : AbsoluteFloorWitness Bool :=
  absolute_floor_of_bare_distinguishability ⟨false, true, bool_distinguishable⟩

/-- The absolute-floor closure certificate is theorem-backed. -/
theorem absoluteFloorClosureCert : AbsoluteFloorClosureCert where
  routeA := selfBootstrapCert
  routeB := fun K _ => distinguishability_iff_nontrivial_specifiability (K := K)
  bool_witness := bool_absolute_floor

What this page does not claim

This theorem does not assert that the physical universe has more than one element. This theorem does not derive any specific physical constant or dimension. This theorem does not claim that the framework's ledger is a physical object; it only establishes a logical precondition.

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