Foundation Magnitude Of Mismatch Single Valued On Unordered Pair

The symmetry of comparison

A comparison operator takes two things and returns a value, like a cost or a distance. Such an operator is single-valued on the unordered pair, meaning it returns the same value whether you feed it (x, y) or (y, x). This is a property of the operator, not a choice about how to interpret it. The framework's machine-checked library of formal theorems proves that this property is exactly the same as symmetry: the operator satisfies C x y = C y x for all x and y.

The proof runs in both directions. If a comparison factors through the unordered pair, then swapping the arguments cannot change the result, so it is symmetric. Conversely, if a comparison is symmetric, it can be expressed as a single function on the unordered pair. The combined theorem, singleValued_iff_symmetric, states this equivalence formally. A corollary shows that if a comparison is asymmetric on even one pair, it fails to be single-valued: it splits into two distinct directional functions, one for each order.

This result matters because it removes interpretive freedom. In the framework's account, the Aristotelian principle of non-contradiction, in operator form, is encoded as symmetry. The theorem shows this encoding is not arbitrary. Any comparison that is a single-valued predicate on a distinguished pair must be symmetric. The asymmetric "directed revision" reading does not produce a single binary function; it produces two. The equality-induced cost, which measures how different two things are, is shown to be single-valued automatically, with no further choice required.

The theorem is general: it holds for any carrier type and any cost type. It does not depend on the specific values of the cost, only on the structure of the comparison. This is a formal result, checked by the machine, not a philosophical assertion. It establishes a structural necessity within the framework, and it does so without invoking any specific cost function or physical constant.

/-- **Equivalence: single-valuedness on the unordered pair is symmetry.** -/
theorem singleValued_iff_symmetric
    {K Cost : Type*} (C : K → K → Cost) :
    SingleValuedOnUnorderedPair C ↔ ∀ x y : K, C x y = C y x :=
  ⟨singleValued_implies_symmetric C,
   fun h => symmetric_implies_factorsThrough C h⟩

/-- The negation: if `C` is asymmetric on at least one pair, it cannot
factor through the unordered pair. Single-valuedness fails the moment the
two orderings give different values.

This is the Lean form of Theorem 3 of the companion paper: asymmetry
splits a single binary function into two directional functions. -/
theorem asymmetric_not_singleValued
    {K Cost : Type*} (C : K → K → Cost)
    (h : ∃ x y : K, C x y ≠ C y x) :
    ¬ SingleValuedOnUnorderedPair C := by
  rintro hSV
  rcases h with ⟨x, y, hxy⟩
  exact hxy (singleValued_implies_symmetric C hSV x y)

/-- The equality-induced cost is single-valued on the unordered pair. -/
theorem equalityCost_singleValued (K : Type*) (weight : ℝ) :
    SingleValuedOnUnorderedPair (equalityCost K weight) :=
  symmetric_implies_factorsThrough (equalityCost K weight)
    (non_contradiction_from_equality K weight)

What this page does not claim

This theorem does not specify what the cost function is. This theorem does not claim that all comparisons in the framework are symmetric. This theorem does not derive any physical constants.

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/MagnitudeOfMismatch.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: