Pith. sign in
module module high

IndisputableMonolith.Foundation.NonTrivialityFromDistinguishability

show as:
view Lean formalization →

Equates operative distinguishability (a non-vacuous comparison of positive quantities) with non-triviality of the logical specification on an inhabited carrier. Absolute-floor satisfaction implies both, and yields the canonical and existing Law-of-Logic packages. Domain-bootstrap and absolute-floor work cite this bridge. Arguments are short equivalences and implications from the imported floor and functional-equation modules.

claimDistinguishability: there exist positive quantities whose comparison is non-vacuous. Non-triviality of a logical specification is equivalent to distinguishability. Satisfaction of the absolute-floor package implies distinguishability and both the canonical and existing Law-of-Logic packages.

background

The Law of Logic is cast as a functional equation on a comparison operator $C$. That equation lives on a real carrier recovered from the same law, so the foundation must first secure that comparison is not vacuous: at least one pair of positive quantities is actually distinguished. The module names that operative content Distinguishability (Aristotelian comparison, not a physical postulate).

AbsoluteFloorClosure supplies the joint certificate that distinguishability is equivalent to non-trivial specifiability on an inhabited carrier, and that the meta-language already distinguishes propositions. LogicAsFunctionalEquation supplies the Law-of-Logic packaging (canonical and existing forms) against which non-triviality is measured.

Sibling objects include the bidirectional bridge nonTrivial iff distinguishability, PositiveRatio, SatisfiesLawsOfLogicAbsoluteFloor, and the implications from absolute-floor satisfaction into distinguishability and the canonical/existing packages.

proof idea

The module is a short bridge layer, not a deep derivation. It defines Distinguishability as existence of a non-vacuous positive comparison, then proves non-triviality of the logical specification iff distinguishability by mutual implication. Absolute-floor satisfaction is shown to imply distinguishability, hence the canonical and existing Law-of-Logic packages, by applying the imported AbsoluteFloorClosure certificate and the LogicAsFunctionalEquation packaging lemmas. Remaining names (PositiveRatio, constZero, SatisfiesLawsOfLogicCanonical) are supporting defs and one-line wrappers around those equivalences.

why it matters in Recognition Science

DomainBootstrap imports this module as Move 2 of the comparison-operator domain bootstrap: the Law of Logic is stated with $C:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$, while the reals themselves are recovered from that law, so one must first know comparison is operative. By tying distinguishability to non-triviality and to the absolute floor, the module discharges the modest precondition that AbsoluteFloorClosure isolates: the remaining floor is not an RS-specific physical postulate, only that there is something to compare. It sits under the Foundation forcing chain ahead of T5 J-uniqueness and the Recognition Composition Law, securing that the carrier is inhabited and non-trivial before J, phi, and the eight-tick structure are forced.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (18)