Foundation Non Triviality From Distinguishability Distinguishability Of Non Triv

Distinguishability

In logic, a comparison operator takes two quantities and returns a value. The constant-zero operator returns 0 for every pair. It satisfies several formal laws of logic, because it never disagrees with anything. But it is useless: it cannot tell two quantities apart. Distinguishability, the requirement that comparison is operative, states that there exists at least one pair of distinct positive quantities whose comparison cost is non-zero. This is the plain meaning of comparison being non-vacuous.

The Recognition Science framework builds its foundation from this idea. Its machine-checked library of formal theorems proves that, under the laws of identity, non-contradiction, and scale invariance, distinguishability is equivalent to the older predicate NonTrivial, which said the derived cost function is not identically zero on positive ratios. The theorem distinguishability_of_nonTrivial proves one direction: if a comparison operator is NonTrivial, then it is distinguishable. The converse, nonTrivial_of_distinguishability, also holds under scale invariance. Together they form the equivalence nonTrivial_iff_distinguishability.

The point is architectural. The framework's earlier formulation carried non_trivial as a posit, an extra commitment. The constant-zero operator vacuously satisfies the four Aristotelian conditions, so without that commitment it could not be ruled out. Distinguishability replaces that posit with a more natural Aristotelian content: comparison is not vacuous. The equivalence proves the two formulations carry the same force, so the framework becomes slightly more fundamental, stating its residual assumption in genuinely logical language rather than in terms of the derived cost definition.

What the theorem does not claim is equally important. It does not assert that any particular pair of quantities is distinguishable, only that at least one such pair exists. It does not derive the value of any comparison cost. It does not prove that the constant-zero operator is the only one excluded; other operators may also fail distinguishability. The theorem is a structural equivalence between two ways of stating a minimal requirement, not a claim about which quantities the universe actually compares.

/-- **Distinguishability**: comparison is operative, i.e. there exists
at least one pair of positive quantities whose comparison is not
vacuous. This is the operative Aristotelian content of comparison. -/
def Distinguishability (C : ComparisonOperator) : Prop :=
  ∃ x y : ℝ, 0 < x ∧ 0 < y ∧ C x y ≠ 0

/-- **Equivalence theorem**: under scale invariance, distinguishability
and non-triviality are the same condition. -/
theorem nonTrivial_iff_distinguishability
    (C : ComparisonOperator) (hSI : ScaleInvariant C) :
    NonTrivial C ↔ Distinguishability C :=
  ⟨distinguishability_of_nonTrivial C, nonTrivial_of_distinguishability C hSI⟩

/-- **Equivalence (backward)**: the algebraic non-triviality predicate
implies distinguishability. -/
theorem distinguishability_of_nonTrivial
    (C : ComparisonOperator)
    (hNT : NonTrivial C) :
    Distinguishability C := by
  obtain ⟨x, hx, hxne⟩ := hNT
  refine ⟨x, 1, hx, one_pos, ?_⟩
  show C x 1 ≠ 0
  exact hxne

/-- Constant zero satisfies identity. -/
theorem constZero_identity : Identity constZero := by
  intro x _; rfl

/-- Constant zero satisfies non-contradiction. -/
theorem constZero_nonContradiction : NonContradiction constZero := by
  intro x y _ _; rfl

/-- Constant zero is continuous on the positive quadrant. -/
theorem constZero_continuous : ExcludedMiddle constZero := by
  unfold ExcludedMiddle
  exact continuousOn_const

/-- Constant zero is scale-invariant. -/
theorem constZero_scaleInvariant : ScaleInvariant constZero := by
  intro _ _ _ _ _ _; rfl

/-- **Equivalence (forward)**: distinguishability implies the algebraic
non-triviality predicate, given Scale Invariance. -/
theorem nonTrivial_of_distinguishability
    (C : ComparisonOperator)
    (hSI : ScaleInvariant C)
    (hDist : Distinguishability C) :
    NonTrivial C := by
  obtain ⟨x, y, hx, hy, hxy⟩ := hDist
  -- Use scale invariance with λ = y⁻¹ to get C(x/y, 1) = C(x, y) ≠ 0.
  have hyinv : (0 : ℝ) < y⁻¹ := inv_pos.mpr hy
  have hxoverypos : (0 : ℝ) < x / y := div_pos hx hy
  have hkey : C (y⁻¹ * x) (y⁻¹ * y) = C x y := hSI x y y⁻¹ hx hy hyinv
  have hyne : (y : ℝ) ≠ 0 := ne_of_gt hy
  have hyinv_y : y⁻¹ * y = 1 := inv_mul_cancel₀ hyne
  have hyinv_x : y⁻¹ * x = x / y := by
    field_simp
  rw [hyinv_y, hyinv_x] at hkey
  refine ⟨x / y, hxoverypos, ?_⟩
  show derivedCost C (x / y) ≠ 0
  unfold derivedCost
  rw [hkey]
  exact hxy

What this page does not claim

This theorem does not identify any specific pair of distinguishable quantities. This theorem does not compute the value of any comparison cost. This theorem does not rule out operators other than constant-zero that also fail distinguishability.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/NonTrivialityFromDistinguishability.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: