pith. machine review for the scientific record. sign in
def definition def or abbrev high

Distinguishability

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  43def Distinguishability (C : ComparisonOperator) : Prop :=

proof body

Definition body.

  44  ∃ x y : ℝ, 0 < x ∧ 0 < y ∧ C x y ≠ 0
  45
  46/-- **Equivalence (forward)**: distinguishability implies the algebraic
  47non-triviality predicate, given Scale Invariance. -/

used by (11)

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

depends on (1)

Lean names referenced from this declaration's body.