Distinguishability
plain-language theorem explainer
The predicate that a comparison operator on positive reals is operative asserts the existence of at least one pair of positive quantities whose comparison yields a nonzero cost. Researchers deriving the functional equation from Aristotelian logic would cite this predicate when replacing the algebraic non-triviality field inside SatisfiesLawsOfLogic. It is introduced as a direct existential definition with no lemmas or reduction steps required.
Claim. Let $C$ be a comparison operator on the positive reals. The predicate that $C$ is operative holds if and only if there exist positive real numbers $x$ and $y$ such that the comparison cost $C(x,y)$ is nonzero.
background
In NonTrivialityFromDistinguishability the module replaces the algebraic non_trivial field of SatisfiesLawsOfLogic with a more primitive Aristotelian notion. A ComparisonOperator is defined as the type ℝ → ℝ → ℝ that returns a real-valued cost for comparing two positive quantities, subject to the four Aristotelian constraints listed in the upstream LogicAsFunctionalEquation module. The module documentation states that this predicate supplies the operative content of comparison without reference to the derived-cost definition, so that non-triviality becomes a corollary rather than a posit.
proof idea
The definition is the direct existential statement: there exist x, y > 0 with C x y ≠ 0. No lemmas are invoked and no tactics are applied; the body is simply the unpacked Prop.
why it matters
This definition supplies the canonical Aristotelian content for the non-triviality condition inside SatisfiesLawsOfLogic. It is invoked by the equivalence nonTrivial_iff_distinguishability (under scale invariance) and by the forward and backward implications distinguishability_of_nonTrivial and nonTrivial_of_distinguishability. In the Recognition framework it grounds the functional equation in operative comparison rather than an algebraic posit, completing the move described in the module documentation from a posited non_trivial field to a statement about distinguishability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.