Foundation Absolute Floor Closure

The absolute floor

Before any system can recognize anything, its universe of discourse must contain at least two distinguishable elements. If everything were identical, there would be nothing to tell apart, and no recognition event could occur. This is the absolute floor: the minimal precondition that a non-singleton universe exists in which any non-vacuous specification can be stated.

The framework's module AbsoluteFloorClosure proves that this floor is equivalent to bare distinguishability on an inhabited carrier. In plain terms, a universe supports recognition if and only if it contains two distinct elements. The theorem absolute_floor_iff_bare_distinguishability establishes this equivalence: the absolute-floor witness, a structure asserting both that the meta-language distinguishes propositions and that a non-trivial specification exists, holds exactly when there exist two unequal elements.

The module also shows that the minimal concrete carrier, the two-element type Bool with values false and true, realizes this floor. This is not a physical postulate; it is a logical precondition. The meta-language already distinguishes propositions, so the remaining floor is simply that there is a non-singleton universe of discourse in which any non-vacuous specification can be stated.

In Recognition Science, this closure certificate is deliberately modest. It reduces the forcing-chain floor to meta-language proposition distinguishability plus a non-singleton universe. The actual mathematical receipt is the equivalence theorem; a self-equality between status strings adds no theorem. The floor is thus not an RS-specific axiom but the precondition that recognition has anything to work on.

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

What this page does not claim

The absolute floor is not a physical postulate about the actual universe. This module does not establish that any particular physical system satisfies the floor.

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: