Foundation Non Triviality From Distinguishability Const Zero Non Contradiction

The constant-zero comparison

A comparison operator is a rule that takes two positive quantities and returns a number meant to measure how far apart they are. The simplest possible rule is the constant-zero operator: no matter which two quantities you feed it, it always returns 0. In the Recognition Science framework, this operator is a genuine candidate for the role of comparison, and it passes several of the basic logical tests. The declaration constZero_nonContradiction is a machine-checked proof that this always-zero rule satisfies the non-contradiction law, meaning it never assigns a non-zero cost to a pair that are actually the same quantity. It also satisfies identity, scale invariance, and the excluded-middle condition, so it is not ruled out by those laws alone.

The problem is that the constant-zero operator is vacuous: it treats every pair of quantities as equally indistinguishable, returning zero even for two clearly different values. If the framework allowed this operator, comparison would be meaningless. To block it, the framework adds a condition called distinguishability, which requires that there exists at least one pair of distinct positive quantities whose comparison cost is non-zero. The declaration constZero_not_distinguishable proves that the constant-zero operator fails this condition, and constZero_not_nonTrivial proves it also fails the older non-triviality predicate. A theorem called nonTrivial_iff_distinguishability shows that, under scale invariance, these two conditions are equivalent, so distinguishability is the more fundamental way to state the requirement.

In Recognition Science, this move replaces a bare assumption with a principle that has content: comparison must actually distinguish some pair of quantities. The framework's library of machine-checked theorems proves that the canonical set of laws, which includes distinguishability, is equivalent to the existing set that used non-triviality. This makes the framework's foundation slightly more principled, since the residual assumption is now stated in terms of what comparison is for, rather than as an algebraic condition on the derived cost function.

What constZero_nonContradiction does not claim is any positive result about real comparisons. It does not say that any particular comparison operator is the right one, nor does it establish that a non-zero comparison cost exists for any specific pair of quantities. It only shows that the always-zero operator is not eliminated by the non-contradiction law alone; the real work of ruling it out falls to the distinguishability condition.

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

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

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

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

/-- Constant zero fails distinguishability. -/
theorem constZero_not_distinguishable : ¬ Distinguishability constZero := by
  intro ⟨_, _, _, _, h⟩
  exact h rfl

/-- **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⟩

/-- The canonical form is equivalent to the existing form. -/
theorem canonical_iff_existing (C : ComparisonOperator) :
    SatisfiesLawsOfLogicCanonical C ↔ SatisfiesLawsOfLogic C := by
  constructor
  · intro h
    refine
      { identity := h.identity
      , non_contradiction := h.non_contradiction
      , excluded_middle := h.excluded_middle
      , scale_invariant := h.scale_invariant
      , route_independence := h.route_independence
      , non_trivial := nonTrivial_of_distinguishability C h.scale_invariant h.distinguishability }
  · intro h
    refine
      { identity := h.identity
      , non_contradiction := h.non_contradiction
      , excluded_middle := h.excluded_middle
      , scale_invariant := h.scale_invariant
      , route_independence := h.route_independence
      , distinguishability := distinguishability_of_nonTrivial C h.non_trivial }

What this page does not claim

No particular comparison operator is shown to be the correct one. No specific pair of quantities is shown to have a non-zero comparison cost. The non-contradiction law alone is not sufficient to rule out the constant-zero operator.

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: