symmetric_implies_factorsThrough
plain-language theorem explainer
Symmetric cost functions on pairs factor through the unordered-pair type Sym2 K. Researchers formalizing the magnitude-of-mismatch encoding cite this result to establish that symmetry is the unique reading consistent with single-valued predication on a distinguished pair. The proof is a direct term-mode construction that applies the Sym2.lift constructor to the given function and symmetry hypothesis.
Claim. Let $C : K → K → Cost$ be a comparison operator. If $C(x,y) = C(y,x)$ for all $x,y ∈ K$, then there exists $f : Sym2 K → Cost$ such that $C(x,y) = f({x,y})$ for all $x,y$.
background
SingleValuedOnUnorderedPair is the predicate that a map $C : K → K → Cost$ factors through the type of unordered pairs: there exists $f : Sym2 K → Cost$ with $C x y = f s(x,y)$ for all $x,y$. The module MagnitudeOfMismatch formalizes the claim that symmetry of $C$ is equivalent to this single-valuedness, as required by the Aristotelian non-contradiction condition (L2) in the Logic_FE rigidity theorem. The companion paper RS_Magnitude_of_Mismatch_Uniqueness.tex presents the combined equivalence as Theorem 4.
proof idea
Term-mode proof. The refine tactic supplies the pair consisting of Sym2.lift applied to the function (fun a b => C a b) together with the symmetry hypothesis, then discharges the membership goal by introducing x y and simplifying with the lemma Sym2.lift_mk.
why it matters
This supplies the right-to-left direction of singleValued_iff_symmetric, the Lean form of Theorem 4 in the companion paper. It is invoked directly by equalityCost_singleValued to conclude that the equality-induced cost is single-valued on unordered pairs. Within the Recognition Science framework the result removes interpretive freedom from the encoding of non-contradiction as symmetry of the comparison operator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.