equalityCost

formal source

  87/-- The **canonical cost induced by equality**: assigns 0 to identical
  88pairs and a positive weight to distinct pairs. This is a function on
  89pairs whose form is determined entirely by the equality predicate. -/
  90noncomputable def equalityCost (K : Type*) (weight : ℝ) : K → K → ℝ :=
  91  fun x y => if x = y then 0 else weight
  92
  93/-! ## The Three Definitional Facts
  94
  95The following three theorems show that an equality-induced cost
  96automatically satisfies three of the four Aristotelian conditions
  97without any structural assumption beyond the type signature.
  98-/
  99
 100/-- **(L1) Identity, derived.** The equality-induced cost satisfies
 101`C(x, x) = 0` definitionally. This is not an axiom; it is the
 102definitional content of "comparing a thing with itself takes no work,"
 103forced by reflexivity of equality. -/
 104theorem identity_from_equality (K : Type*) (weight : ℝ) :
 105    ∀ x : K, equalityCost K weight x x = 0 := by
 106  intro x
 107  unfold equalityCost
 108  simp
 109
 110/-- **(L2) Non-Contradiction, derived.** The equality-induced cost is
 111symmetric in its arguments. This follows from the symmetric definition
 112of equality: `x = y` iff `y = x`. -/
 113theorem non_contradiction_from_equality (K : Type*) (weight : ℝ) :
 114    ∀ x y : K, equalityCost K weight x y = equalityCost K weight y x := by
 115  intro x y
 116  unfold equalityCost
 117  by_cases h : x = y
 118  · subst h; rfl
 119  · have hSymm : ¬ y = x := fun heq => h heq.symm
 120    simp [h, hSymm]