98theorem asymmetric_not_singleValued 99 {K Cost : Type*} (C : K → K → Cost) 100 (h : ∃ x y : K, C x y ≠ C y x) : 101 ¬ SingleValuedOnUnorderedPair C := by
proof body
Term-mode proof.
102 rintro hSV 103 rcases h with ⟨x, y, hxy⟩ 104 exact hxy (singleValued_implies_symmetric C hSV x y) 105 106/-! ## Connection to PrimitiveDistinction 107 108The `PrimitiveDistinction.equalityCost` is the canonical equality-induced 109cost. By the equivalence above, it is single-valued on the unordered pair 110iff it is symmetric — and `non_contradiction_from_equality` already proves 111symmetry of the equality-induced cost. So the equality-induced cost is in 112the canonical magnitude-of-mismatch shape automatically, with no further 113choice. -/ 114 115open IndisputableMonolith.Foundation.PrimitiveDistinction 116 117/-- The equality-induced cost is single-valued on the unordered pair. -/
depends on (22)
Lean names referenced from this declaration's body.