pith. sign in
theorem

absolute_floor_iff_bare_distinguishability

proved
show as:
module
IndisputableMonolith.Foundation.AbsoluteFloorClosure
domain
Foundation
line
47 · github
papers citing
1559 papers (below)

plain-language theorem explainer

The equivalence shows that for any nonempty type K the absolute-floor witness holds exactly when K contains at least two distinct elements. Foundational work on Recognition Science cites this result to close the absolute-floor program by reducing it to bare distinguishability without extra physical assumptions. The proof is a direct term-mode pairing of the two one-directional lemmas already proved in the same module.

Claim. For any nonempty type $K$, the absolute-floor witness on $K$ (the conjunction of meta-language distinction of propositions and existence of a nontrivial specification on $K$) holds if and only if there exist distinct $x, y : K$.

background

The module AbsoluteFloorClosure supplies a joint certificate that the absolute floor reduces to bare distinguishability. The structure AbsoluteFloorWitness $K$ on a nonempty carrier $K$ requires two components: meta_distinguishes asserting existence of distinct propositions $P, Q$ and nontrivial_specifiable asserting Nonempty(NontrivialSpecification $K$). Module documentation states that the closure is modest because distinguishability equates to non-trivial specifiability on an inhabited carrier while the meta-language already distinguishes propositions, so the floor is merely the precondition of a non-singleton universe of discourse.

proof idea

The proof is a term-mode construction returning the pair of bare_distinguishability_of_absolute_floor and absolute_floor_of_bare_distinguishability. This directly assembles the biconditional from the two directional results already established in the module.

why it matters

This theorem completes the absolute-floor closure by showing equivalence to bare distinguishability, confirming that the floor is a logical precondition rather than an RS-specific postulate as stated in the module documentation. No downstream uses appear, so the result functions as a terminal foundational fact. It touches the question of whether meta-language distinction of propositions needs further justification beyond standard logic.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.