pith. sign in
theorem

absolute_floor_iff_bare_distinguishability

proved
show as:

Why this theorem is linked from The lattice of smooth sublocales as a Bruns-Lakser completion unclear

Pith linked this Lean declaration because the review connected a specific passage in the paper to this theorem. The relation tag says how strong that connection is; it is not a generic placeholder.

the admissible meets of LC(L) are exactly the joins of locally closed sublocales which are themselves locally closed

Relation between the paper passage and the cited Recognition theorem.

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.