Pith. sign in
module module high

IndisputableMonolith.Foundation.DistinguishabilityFromSpecifiability

show as:
view Lean formalization →

The module defines NontrivialSpecification as a predicate on type K that holds for some element and fails for another, then establishes its equivalence to distinguishability. AbsoluteFloorClosure cites the result to close the foundation layer. The development consists of the core definition plus equivalence and closure theorems proved in Mathlib.

claimLet $K$ be a type. A predicate $P:K o\mathrm{Prop}$ is nontrivial when $\exists x\,P(x)\land\exists y\,\neg P(y)$. Distinguishability on $K$ holds if and only if a nontrivial specification exists.

background

The module belongs to the Foundation domain and imports only Mathlib. It introduces NontrivialSpecification as a predicate on a universe of discourse K that is true for at least one element and false for at least one. Sibling declarations include distinguishability_from_specification, distinguishability_iff_nontrivial_specifiability, and SpecifiabilityClosureCert.

The local theoretical setting treats distinguishability as a meta-linguistic precondition rather than an RS-specific axiom. The module therefore supplies the logical bridge used by downstream certificates.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds AbsoluteFloorClosure, whose doc-comment states that distinguishability is equivalent to non-trivial specifiability on an inhabited carrier and that the remaining floor is therefore not an RS-specific physical postulate. It closes the absolute-floor program by reducing the precondition to the meta-language's ability to distinguish propositions.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (8)