  40/-- **Distinguishability**: comparison is operative, i.e. there exists
  41at least one pair of positive quantities whose comparison is not
  42vacuous. This is the operative Aristotelian content of comparison. -/
  43def Distinguishability (C : ComparisonOperator) : Prop :=
  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. -/
  48theorem nonTrivial_of_distinguishability
  49    (C : ComparisonOperator)
  50    (hSI : ScaleInvariant C)
  51    (hDist : Distinguishability C) :
  52    NonTrivial C := by
  53  obtain ⟨x, y, hx, hy, hxy⟩ := hDist
  54  -- Use scale invariance with λ = y⁻¹ to get C(x/y, 1) = C(x, y) ≠ 0.
  55  have hyinv : (0 : ℝ) < y⁻¹ := inv_pos.mpr hy
  56  have hxoverypos : (0 : ℝ) < x / y := div_pos hx hy
  57  have hkey : C (y⁻¹ * x) (y⁻¹ * y) = C x y := hSI x y y⁻¹ hx hy hyinv
  58  have hyne : (y : ℝ) ≠ 0 := ne_of_gt hy
  59  have hyinv_y : y⁻¹ * y = 1 := inv_mul_cancel₀ hyne
  60  have hyinv_x : y⁻¹ * x = x / y := by
  61    field_simp
  62  rw [hyinv_y, hyinv_x] at hkey
  63  refine ⟨x / y, hxoverypos, ?_⟩
  64  show derivedCost C (x / y) ≠ 0
  65  unfold derivedCost
  66  rw [hkey]
  67  exact hxy
  68
  69/-- **Equivalence (backward)**: the algebraic non-triviality predicate
  70implies distinguishability. -/
  71theorem distinguishability_of_nonTrivial
  72    (C : ComparisonOperator)
  73    (hNT : NonTrivial C) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.