nonTrivial_of_distinguishability
plain-language theorem explainer
Distinguishability of a comparison operator implies its non-triviality when scale invariance holds. Researchers formalizing the equivalence between Aristotelian distinguishability and algebraic non-triviality in the Recognition Science foundation would cite this result. The proof extracts a distinguishing pair from the hypothesis, applies scale invariance with the inverse of the second argument to normalize to unity, and verifies that the derived cost is nonzero at the resulting ratio.
Claim. Let $C : ℝ → ℝ → ℝ$ be a comparison operator. If $C$ is scale-invariant, meaning $C(λx, λy) = C(x,y)$ for all $x,y,λ > 0$, and distinguishable, meaning there exist $x,y > 0$ with $C(x,y) ≠ 0$, then $C$ is non-trivial: there exists $r > 0$ such that $C(r,1) ≠ 0$.
background
A ComparisonOperator is a map from pairs of positive reals to reals that assigns a comparison cost. ScaleInvariant requires the cost to depend only on the ratio: $C(λx, λy) = C(x,y)$ whenever $x,y,λ > 0$. Distinguishability asserts that comparison is operative, i.e., there exist positive $x,y$ with nonzero cost. NonTrivial asserts existence of a positive ratio whose derived cost is nonzero, where derivedCost(C,r) is defined as C(r,1).
proof idea
The proof obtains the witness pair x,y from the Distinguishability hypothesis. It applies scale invariance with λ = y^{-1} to obtain C(x/y,1) = C(x,y) ≠ 0, using positivity of the inverse and division together with field simplification to confirm the normalization. Unfolding derivedCost then directly yields the required NonTrivial witness.
why it matters
This theorem supplies the forward direction of the equivalence between distinguishability and non-triviality, which is used in nonTrivial_iff_distinguishability to equate the two predicates under scale invariance. It thereby supports the canonical form SatisfiesLawsOfLogicCanonical, shown equivalent to the original SatisfiesLawsOfLogic in canonical_iff_existing. The module documentation states that this replaces the algebraic non_trivial posit with the more natural Aristotelian content of distinguishability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.