Foundation Non Triviality From Distinguishability

From a posit to a corollary

In the Recognition Science framework, the laws of logic are not taken as given axioms but are themselves derived from a more basic structure: a comparison operator that assigns a cost to any pair of positive quantities. The framework's central theorem shows that any cost function satisfying five plain conditions must take a specific form. But a subtle gap remained. One of those conditions, called non-triviality, was simply posited: the cost function is not identically zero. That posit was needed because the constant-zero operator, which assigns zero cost to every comparison, vacuously satisfies the other four Aristotelian conditions. Without an extra commitment, the framework could not rule it out.

The module NonTrivialityFromDistinguishability closes this gap by replacing the posit with a more natural Aristotelian claim: distinguishability, the assertion that comparison is not vacuous, meaning there exists at least one pair of distinct positive quantities whose comparison cost is non-zero. This is the operative content of comparison: it actually tells things apart. The module proves the equivalence: under the conditions of Identity, Non-Contradiction, and Scale Invariance, distinguishability is equivalent to the original non-triviality predicate. So distinguishability is the canonical Aristotelian content, and non-triviality is an algebraic reformulation of the same fact.

This shift makes the framework slightly more fundamental. The residual posit in the earlier formulation is now stated in genuinely Aristotelian language, with no reference to the derived-cost definition. The module also shows that the constant-zero operator fails distinguishability, confirming that the new condition does the work it was designed to do. The framework's machine-checked library of formal theorems now carries this result as a proved theorem, not an assumption.

In plain language: the framework no longer needs to assume that comparison is meaningful. It derives that meaningfulness from the single, self-evident claim that comparison distinguishes things. This is a small but significant step in the framework's program of deriving physical and mathematical structure from the forced cost of recognition.

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

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

/-- The canonical Aristotelian form of the Law of Logic, with
distinguishability replacing the algebraic non-triviality predicate. -/
structure SatisfiesLawsOfLogicCanonical (C : ComparisonOperator) : Prop where
  identity            : Identity C
  non_contradiction   : NonContradiction C
  excluded_middle     : ExcludedMiddle C
  scale_invariant     : ScaleInvariant C
  route_independence  : RouteIndependence C
  distinguishability  : Distinguishability C

What this page does not claim

This module does not prove that the cost function takes its specific closed form; that remains a separate theorem. Distinguishability is not claimed to be a physical observation; it is a formal condition on the comparison operator. The equivalence holds only under the stated conditions of Identity, Non-Contradiction, and Scale Invariance, not in general.

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: