distinguishability_of_nonTrivial
plain-language theorem explainer
Non-triviality of a comparison operator implies distinguishability: if the derived cost is nonzero at some positive ratio then there exist positive quantities with nonzero direct comparison cost. Foundation researchers in Recognition Science cite this to replace the algebraic non-triviality posit with the more primitive Aristotelian distinguishability condition. The term-mode proof directly constructs the distinguishing pair by pairing the non-trivial witness with the multiplicative unit 1.
Claim. Let $C$ be a comparison operator. If $C$ is non-trivial, i.e. there exists $x > 0$ such that the derived cost of $C$ at $x$ is nonzero, then $C$ is distinguishable, i.e. there exist $x, y > 0$ such that $C(x, y) ≠ 0$.
background
The module NonTrivialityFromDistinguishability promotes NonTrivial from a posit to a corollary of distinguishability. Distinguishability asserts that comparison is operative: there exist positive quantities $x$ and $y$ such that $C(x, y) ≠ 0$. NonTrivial asserts that the derived cost function, obtained by fixing the second argument at the multiplicative identity, is not identically zero on positive ratios. The module doc states that this replaces the residual posit in SatisfiesLawsOfLogic with genuinely Aristotelian content, with no reference to the derived-cost definition. Upstream, ComparisonOperator is the type ℝ → ℝ → ℝ and NonTrivial is defined via the derived cost.
proof idea
The proof is a one-line wrapper in term mode. It obtains the witness triple from the NonTrivial hypothesis, then refines it to a Distinguishability witness by setting the second argument to 1 and using the fact that nonzero derived cost at $x$ directly yields $C x 1 ≠ 0$.
why it matters
This theorem supplies the backward direction for nonTrivial_iff_distinguishability, which in turn supports the canonical form SatisfiesLawsOfLogicCanonical via canonical_iff_existing. It feeds into real_supports_logic by ensuring the logic supported on ℝ is non-vacuous. In the Recognition framework it advances the move to state the residual posit in Aristotelian language rather than an algebraic condition, closing the replacement of the non-triviality field in SatisfiesLawsOfLogic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.