IndisputableMonolith.Foundation.DistinguishabilityFromSpecifiability
The module defines non-trivial specifications on a carrier K and establishes their equivalence to distinguishability. Recognition Science foundation work cites it to ground the absolute floor in logical preconditions rather than physical postulates. The argument proceeds by introducing the predicate definition and proving direct equivalences to distinguishability statements.
claimLet $K$ be a type. A predicate $P : K → Prop$ is a nontrivial specification if $∃ x : K, P x$ and $∃ y : K, ¬P y$.
background
Recognition Science begins with distinguishability inside a universe of discourse before introducing J-cost, defect measures, or the phi-ladder. This module supplies the logical reduction showing that distinguishability on an inhabited carrier is equivalent to the existence of a predicate that holds for some elements and fails for others. The setting is the meta-language precondition that propositions can already be distinguished, as referenced in the downstream closure argument.
proof idea
This is a definition module. It introduces NontrivialSpecification as the predicate with the stated existence properties, then proves distinguishability_from_specification and related equivalences by direct unfolding of the definitions and logical manipulation of existence statements.
why it matters in Recognition Science
The module feeds AbsoluteFloorClosure, which concludes that the absolute floor is not an RS-specific physical postulate but the precondition that the meta-language already distinguishes propositions. It fills the foundational step establishing distinguishability iff nontrivial specifiability on an inhabited carrier.
scope and limits
- Does not assume any algebraic or topological structure on the carrier K.
- Does not assign physical meaning to the predicates themselves.
- Does not address existence of nontrivial specifications in concrete models.
- Does not extend the equivalence beyond inhabited carriers.
used by (1)
declarations in this module (8)
-
structure
NontrivialSpecification -
theorem
distinguishability_from_specification -
def
nontrivial_specification_of_proper_subtype -
def
nontrivial_spec_from_proper_ontology -
theorem
at_most_one_of_no_nontrivial_specification -
theorem
distinguishability_iff_nontrivial_specifiability -
structure
SpecifiabilityClosureCert -
theorem
specifiabilityClosureCert