Foundation Magnitude Of Mismatch Single Valued Implies Symmetric

The forced symmetry of comparison

In mathematics, a function that takes two inputs is symmetric when swapping the inputs leaves the output unchanged: C(x, y) = C(y, x). The Recognition Science declaration singleValued_implies_symmetric proves a simple but consequential fact: if a comparison operator C yields a single value for an unordered pair {x, y}, then C must be symmetric. The proof is immediate from the definition of an unordered pair, where the order of elements is irrelevant by construction.

The declaration is one half of an equivalence. The companion theorem symmetric_implies_factorsThrough shows the converse: any symmetric function on pairs can be represented as a single function on unordered pairs. Combined, they form the theorem singleValued_iff_symmetric, which states that single-valuedness on the unordered pair and symmetry are exactly the same property. A further theorem, asymmetric_not_singleValued, makes the contrapositive explicit: if C(x, y) differs from C(y, x) for some pair, then C cannot be single-valued on the unordered pair.

In Recognition Science, this result is used to argue that the Aristotelian principle of non-contradiction, encoded as symmetry of a comparison operator, is not an arbitrary interpretive choice. The framework's library shows that any comparison that returns one value for an unordered pair must be symmetric; the asymmetric "directed revision" reading would not produce a single binary function but two distinct directional functions. The equality-induced cost, a canonical construction in the framework, is shown to be single-valued on the unordered pair automatically, with no further choice required.

The theorem is not a claim about any particular cost function or about the world. It is a purely structural statement about functions between arbitrary types K and Cost. It does not assert that symmetry is desirable, nor that any actual comparison in physics must be symmetric. It establishes only the logical equivalence between two ways of saying the same thing about a function.

/-- **Single-valued predication forces symmetry.**

If a comparison operator factors through the unordered pair, then the
order of its arguments does not matter. The asymmetric reading (where
`C x y` and `C y x` are different values) is not a single function on
pairs; it is two distinct directional functions. -/
theorem singleValued_implies_symmetric
    {K Cost : Type*} (C : K → K → Cost)
    (h : SingleValuedOnUnorderedPair C) :
    ∀ x y : K, C x y = C y x := by
  intro x y
  rcases h with ⟨f, hf⟩
  have hxy := hf x y
  have hyx := hf y x
  have hsym : (s(x, y) : Sym2 K) = s(y, x) := Sym2.eq_swap
  rw [hxy, hyx, hsym]

/-- **Conversely: symmetric comparisons factor through unordered pairs.**

Any symmetric function on `K × K` is the lift of a single function on
`Sym2 K`. So symmetry and single-valuedness on the unordered pair are
equivalent. -/
theorem symmetric_implies_factorsThrough
    {K Cost : Type*} (C : K → K → Cost)
    (hsymm : ∀ x y : K, C x y = C y x) :
    SingleValuedOnUnorderedPair C := by
  refine ⟨Sym2.lift ⟨fun a b => C a b, fun a b => hsymm a b⟩, ?_⟩
  intro x y
  simp [Sym2.lift_mk]

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

The theorem does not claim that any actual comparison operator in physics is symmetric. The theorem does not derive the specific form of the cost function J(x). The theorem does not claim that symmetry is a desirable property, only a logical consequence of single-valuedness on unordered pairs.

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: