equalityCost_singleValued
plain-language theorem explainer
The equality-induced cost function on type K with parameter weight is single-valued on unordered pairs. Logicians and physicists working on the uniqueness of the magnitude-of-mismatch encoding cite this to close interpretive freedom for the (L2) Non-Contradiction condition. The proof is a one-line term application of the symmetric-implies-factors-through lemma together with the non-contradiction property of equality.
Claim. Let $C$ be the cost function induced by equality on type $K$ with weight parameter. Then $C$ factors through the unordered-pair type Sym2 $K$: there exists $f :$ Sym2 $K$ $→$ Cost such that $C(x,y) = f(s(x,y))$ for all $x,y$.
background
This theorem lives in the MagnitudeOfMismatch module, whose module doc states that symmetry of a comparison operator is forced by single-valued predication on unordered pairs, formalizing Theorem 4 of the companion paper RS_Magnitude_of_Mismatch_Uniqueness.tex. The central definition SingleValuedOnUnorderedPair asserts that a map $C : K → K →$ Cost is single-valued precisely when it factors through Sym2 $K$, i.e., $C(x,y) = f(s(x,y))$ for some $f$. Upstream, non_contradiction_from_equality (imported via PrimitiveDistinction) supplies the symmetry witness for equalityCost, while symmetric_implies_factorsThrough is the general implication used here.
proof idea
The proof is a term-mode one-liner: it applies symmetric_implies_factorsThrough directly to equalityCost K weight and the non_contradiction_from_equality K weight witness. No further tactics or reductions are required; the general lemma that symmetry implies factoring through Sym2 K discharges the goal.
why it matters
The result feeds the Recognizer structure in RecognizerInducesLogic, confirming that the magnitude-of-mismatch encoding is the unique reading consistent with single-valued predication on a distinguished pair. It thereby closes the (L2) Non-Contradiction clause of the Logic_FE rigidity theorem without interpretive latitude, aligning with the Recognition Science forcing chain that derives symmetry from the requirement that comparisons return a single value on unordered pairs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.