IndisputableMonolith.Foundation.NonTrivialityFromDistinguishability
This module establishes that operative distinguishability in the comparison operator domain is equivalent to non-trivial specifiability on an inhabited carrier. It supplies the Aristotelian content of comparison as the precondition for the Law of Logic. Researchers building the Recognition Science foundation cite it to justify the absolute floor without adding physical postulates. The argument consists of direct equivalence theorems that close the meta-language distinction already present in the carrier.
claimDistinguishability holds when there exist positive $x, y > 0$ such that the comparison $C(x, y)$ is not vacuous, where $C : ℝ → ℝ → ℝ$ is the comparison operator of the Law of Logic. This is equivalent to non-trivial specifiability on an inhabited carrier.
background
The module belongs to the Foundation layer and imports LogicAsFunctionalEquation, which encodes the Law of Logic via the comparison operator $C$, together with AbsoluteFloorClosure, whose joint certificate states that distinguishability is equivalent to non-trivial specifiability on an inhabited carrier. Distinguishability is introduced as the operative content of comparison: at least one pair of positive quantities yields a non-vacuous result. The meta-language already distinguishes propositions, so the remaining floor is not an RS-specific postulate.
proof idea
This is a definition module containing equivalence theorems. The core results are nonTrivial_of_distinguishability, distinguishability_of_nonTrivial, and nonTrivial_iff_distinguishability. Each direction follows from the closure properties certified in AbsoluteFloorClosure; the iff form is obtained by composing the two one-line implications.
why it matters in Recognition Science
The module feeds the root IndisputableMonolith theorem and the DomainBootstrap move that recovers the comparison-operator domain. It closes the precondition that the meta-language distinguishes propositions, allowing the Law of Logic to proceed from the recovered real line without circularity. Downstream DomainBootstrap explicitly invokes this equivalence to bootstrap the domain.
scope and limits
- Does not introduce new physical postulates beyond meta-language distinction.
- Does not specify the explicit functional form of the comparison operator.
- Does not derive the real-line structure or the functional equation itself.
- Does not address inhabitedness of the carrier beyond the equivalence.
used by (2)
depends on (2)
declarations in this module (18)
-
def
Distinguishability -
theorem
nonTrivial_of_distinguishability -
theorem
distinguishability_of_nonTrivial -
theorem
nonTrivial_iff_distinguishability -
structure
SatisfiesLawsOfLogicCanonical -
theorem
canonical_iff_existing -
abbrev
PositiveRatio -
structure
SatisfiesLawsOfLogicAbsoluteFloor -
theorem
distinguishability_of_absoluteFloor -
theorem
canonical_of_absoluteFloor -
theorem
existing_of_absoluteFloor -
def
constZero -
theorem
constZero_identity -
theorem
constZero_nonContradiction -
theorem
constZero_continuous -
theorem
constZero_scaleInvariant -
theorem
constZero_not_distinguishable -
theorem
constZero_not_nonTrivial