nonTrivial_iff_distinguishability
plain-language theorem explainer
Under scale invariance a comparison operator satisfies the non-triviality condition precisely when there exist distinct positive quantities whose comparison yields non-zero cost. Researchers formalizing the Recognition Science axioms would invoke this equivalence to substitute the algebraic non-triviality posit with the Aristotelian distinguishability predicate. The argument proceeds by composing the two one-directional implications already established in the same module.
Claim. Let $C$ be a comparison operator that is scale-invariant. Then $C$ is non-trivial (there exists a positive ratio whose derived cost is nonzero) if and only if $C$ is distinguishable (there exist positive reals $x,y$ such that $C(x,y)≠0$).
background
The module replaces the non_trivial field inside SatisfiesLawsOfLogic with a more primitive Aristotelian statement. A ComparisonOperator maps pairs of positive reals to a real cost; scale invariance reduces it to a derived cost on positive ratios. NonTrivial asserts existence of a positive ratio with nonzero derived cost, while Distinguishability asserts existence of at least one pair of positive quantities with nonzero direct cost.
proof idea
The proof is the term that pairs the two sibling implications: distinguishability_of_nonTrivial applied to C together with nonTrivial_of_distinguishability applied to C and the scale-invariance hypothesis. Each direction is established separately in the same file; the iff is assembled by the pair constructor.
why it matters
This declaration completes the move described in the module documentation: non-triviality becomes a corollary rather than an extra axiom inside SatisfiesLawsOfLogic. It therefore appears in the canonical form SatisfiesLawsOfLogicCanonical that uses distinguishability. The equivalence relies on the scale-invariance bridge already proved in LogicAsFunctionalEquation and supports the later claim that the framework rests on Identity, Non-Contradiction, and distinguishability alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.