singleValued_iff_symmetric
plain-language theorem explainer
A binary comparison operator C on any carrier K is single-valued on unordered pairs exactly when it is symmetric. Researchers formalizing the Recognition Science treatment of logical non-contradiction cite this equivalence to close the encoding of condition (L2). The proof is a direct term-level pairing of the two one-directional lemmas already proved in the same module.
Claim. Let $C : K → K → Cost$ be any binary operator. Then $C$ factors through the type of unordered pairs $Sym_2(K)$ if and only if $C(x,y) = C(y,x)$ for all $x,y ∈ K$.
background
The module establishes that the magnitude-of-mismatch operator must be symmetric because single-valued predication on an unordered pair forces the two orderings to return identical values. SingleValuedOnUnorderedPair is defined by the existence of a function $f : Sym_2 K → Cost$ such that $C x y = f s(x,y)$ for the unordered-pair constructor $s$. The module document states that this equivalence is the Lean form of Theorem 4 of the companion paper RS_Magnitude_of_Mismatch_Uniqueness.tex and that it leaves the encoding of (L2) Non-Contradiction without interpretive freedom once (L1) and (L3a) are fixed by PrimitiveDistinction.
proof idea
The term proof pairs the two directions already established in the module: singleValued_implies_symmetric supplies the left-to-right implication while symmetric_implies_factorsThrough supplies the right-to-left implication. No additional tactics or reductions are required.
why it matters
This equivalence is the immediate parent of magnitude_of_mismatch_forced, the combined statement that single-valuedness on unordered pairs is equivalent to symmetry. It therefore supplies the final step that converts the Aristotelian non-contradiction condition into the unique operator consistent with single-valued predication. The result sits inside the Logic_FE rigidity chain and removes any remaining freedom in the magnitude-of-mismatch encoding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.