Foundation Magnitude Of Mismatch

The forced symmetry of comparison

A comparison between two items asks how far apart they are. If the answer is a single number, the order in which you name the items cannot matter: comparing a circle to a square yields the same distance as comparing a square to a circle. This symmetry, written C(x, y) = C(y, x), is so natural that it often goes unnoticed. In Recognition Science, the framework treats this not as a convention but as a forced consequence of the act of comparison itself.

The framework's recognition (a discrete record of events) begins with a primitive distinction: two things are either the same or different. From that distinction, the framework builds a cost (a number measuring the mismatch between two items). The question is what form a comparison operator C can take. The answer, proved in the framework's machine-checked library of formal theorems, is that any comparison returning a single value for an unordered pair must be symmetric. The proof runs both directions: if a comparison factors through the unordered pair type, it is symmetric; and any symmetric comparison factors through that same type. The two conditions are equivalent.

The alternative reading, called directed revision, would allow C(x, y) to differ from C(y, x). That reading does not produce one comparison function; it produces two distinct directional functions, one for each order. The framework's theorem shows that asymmetry splits the operator and fails single-valuedness. This is the formal content of the Aristotelian principle of non-contradiction applied to operator structure: a comparison that gives one answer cannot also give a different answer when the arguments are swapped.

The result matters because it removes interpretive freedom. Once a comparison is single-valued on a distinguished pair, its symmetry is not a choice but a necessity. The framework's library proves this equivalence for any carrier type K and any cost type Cost, with no special assumptions. The equality-induced cost, which measures whether two items are the same, automatically satisfies this condition. The magnitude-of-mismatch encoding is therefore the unique consistent reading of comparison in the framework, not one option among many.

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

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

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

/-- 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 does not claim that all comparisons in mathematics must be symmetric. This does not claim that the framework derives the specific cost function J(x) from this module alone. This does not claim that directed revision is impossible, only that it is not a single-valued comparison.

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: