asymmetric_not_singleValued
plain-language theorem explainer
If a binary comparison operator C on K is asymmetric for some pair, then C cannot factor through the unordered-pair type Sym2 K. Recognition Science researchers cite this to show that single-valued predication on distinguished pairs forces symmetry, ruling out directed-revision readings. The term proof assumes single-valuedness, applies the symmetry implication lemma, and obtains an immediate contradiction with the given asymmetry witness.
Claim. Let $C : K → K → Cost$. If there exist $x, y ∈ K$ such that $C(x, y) ≠ C(y, x)$, then there is no function $f : Sym_2 K → Cost$ satisfying $C(x, y) = f({x, y})$ for all $x, y$.
background
The module establishes that symmetry of a comparison operator is equivalent to its factoring through the unordered-pair type Sym2 K. SingleValuedOnUnorderedPair C is defined to mean there exists f : Sym2 K → Cost such that C x y equals f applied to the unordered pair for every ordered pair. The upstream lemma singleValued_implies_symmetric states that any such factoring forces C x y = C y x for all x, y. Module documentation ties this equivalence to the Logic_FE rigidity theorem, which encodes the Aristotelian non-contradiction condition (L2) directly as symmetry of the comparison operator.
proof idea
The proof is a short term-mode contradiction. It assumes SingleValuedOnUnorderedPair C, invokes singleValued_implies_symmetric to obtain symmetry, and substitutes the asymmetry witness to derive C x y = C y x, contradicting the hypothesis.
why it matters
This declaration is the Lean form of Theorem 3 in the companion paper RS_Magnitude_of_Mismatch_Uniqueness.tex. It shows that asymmetry splits a binary function into two distinct directional functions, preventing single-valued predication. The result closes one direction of the symmetry-single-valuedness equivalence in the module, reinforcing that the magnitude-of-mismatch encoding is the unique reading consistent with single-valued predication on a distinguished pair and with the non-contradiction condition in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.