SingleValuedOnUnorderedPair
A binary operator C from carrier K to cost type is single-valued on unordered pairs exactly when it factors through Sym2 K, so C x y equals some f applied to the set {x, y}. Recognition Science researchers formalizing the Logic_FE rigidity theorem cite this definition when they encode non-contradiction as symmetry of comparison operators. The declaration is introduced directly as an existential lift to the unordered-pair type.
claimA function $C : K → K → Cost$ is single-valued on unordered pairs if there exists $f : Sym_2 K → Cost$ such that $C(x, y) = f({x, y})$ for all $x, y ∈ K$.
background
The MagnitudeOfMismatch module treats the comparison operator C as the object whose symmetry encodes Aristotelian non-contradiction (L2) from the Logic_FE rigidity theorem. Single-valued predication on an unordered pair is defined to be equivalent to the symmetry condition C x y = C y x. The module proves both directions and combines them into the iff statement that appears as Theorem 4 of the companion paper RS_Magnitude_of_Mismatch_Uniqueness.tex.
proof idea
The declaration is a direct definition that introduces the predicate as the existence of a lift f : Sym2 K → Cost satisfying C x y = f s(x, y). It is used verbatim by the surrounding theorems singleValued_implies_symmetric and symmetric_implies_factorsThrough to establish the equivalence with symmetry.
why it matters in Recognition Science
This definition supplies the base predicate for magnitude_of_mismatch_forced and for the RecognizerInducesLogic results on unification. It closes the interpretive gap left by PrimitiveDistinction by showing that any single-valued reading of a comparison on a distinguished pair must be symmetric. In the Recognition framework it therefore fixes the magnitude-of-mismatch encoding as the unique reading consistent with single-valued predication.
scope and limits
- Does not assert existence of any concrete operator C on a given K.
- Does not restrict the cost type beyond being an arbitrary Type.
- Does not address decidability or computability of the predicate.
- Does not incorporate physical constants such as phi or alpha.
formal statement (Lean)
48def SingleValuedOnUnorderedPair {K Cost : Type*} (C : K → K → Cost) : Prop :=
proof body
Definition body.
49 ∃ f : Sym2 K → Cost, ∀ x y, C x y = f s(x, y)
50
51/-! ## Symmetry Forced by Single-Valuedness -/
52
53/-- **Single-valued predication forces symmetry.**
54
55If a comparison operator factors through the unordered pair, then the
56order of its arguments does not matter. The asymmetric reading (where
57`C x y` and `C y x` are different values) is not a single function on
58pairs; it is two distinct directional functions. -/