singleValued_implies_symmetric
plain-language theorem explainer
A cost function on pairs that factors through the unordered-pair type Sym2 K must satisfy C x y = C y x. Researchers formalizing the Logic_FE rigidity theorem cite this to encode Aristotelian non-contradiction as symmetry of comparison. The proof extracts the unique factoring map f from the single-valuedness hypothesis and rewrites both orderings against the built-in swap equality of Sym2.
Claim. Let $C : K → K → Cost$ be a comparison operator. If there exists a function $f : Sym_2 K → Cost$ such that $C(x,y) = f(s(x,y))$ for the unordered-pair constructor $s$, then $C(x,y) = C(y,x)$ holds for all $x,y ∈ K$.
background
The module formalizes symmetry of comparison as the Lean encoding of condition (L2) non-contradiction inside the Logic_FE rigidity theorem. SingleValuedOnUnorderedPair is the predicate that a map $C : K → K → Cost$ factors through Sym2 K: there exists $f$ with $C x y = f s(x,y)$ for every ordered pair, so the value is independent of presentation order. The companion paper RS_Magnitude_of_Mismatch_Uniqueness.tex treats this factorization as the only reading consistent with single-valued predication on a distinguished pair.
proof idea
The term proof introduces arbitrary x and y, destructures the hypothesis to obtain the factoring function f together with its defining equation, instantiates that equation on both (x,y) and (y,x), and rewrites using the library fact that s(x,y) equals s(y,x) inside Sym2. The two applications of f therefore coincide.
why it matters
This implication supplies one direction of the equivalence singleValued_iff_symmetric, which the module identifies as the Lean statement of Theorem 4 in the companion paper. Together with the PrimitiveDistinction results that (L1), (L2) and (L3a) are definitional, the equivalence removes interpretive latitude from the magnitude-of-mismatch encoding: symmetry is forced by single-valuedness on unordered pairs. The result sits inside the foundation layer that later feeds the eight-tick octave and D = 3 derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.