SingleValuedOnUnorderedPair
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.