non_contradiction_from_equality

formal source

 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]
 121
 122/-- **(L3a) Totality, derived.** The equality-induced cost is total:
 123it is defined and returns a value for every ordered pair in `K × K`.
 124This follows from the function type signature alone; there are no
 125input pairs on which the cost is undefined. -/
 126theorem totality_from_function_type (K : Type*) (weight : ℝ) :
 127    ∀ x y : K, ∃ c : ℝ, equalityCost K weight x y = c := by
 128  intro x y
 129  exact ⟨equalityCost K weight x y, rfl⟩
 130
 131/-- **(L1)+(L2)+(L3a) packaged.** The equality-induced cost satisfies
 132the three definitional Aristotelian conditions (Identity,
 133Non-Contradiction, Totality) automatically, with no structural
 134assumption beyond the existence of an equality predicate on `K`. -/
 135theorem equality_cost_satisfies_definitional_conditions
 136    (K : Type*) (weight : ℝ) :
 137    (∀ x : K, equalityCost K weight x x = 0) ∧
 138    (∀ x y : K, equalityCost K weight x y = equalityCost K weight y x) ∧
 139    (∀ x y : K, ∃ c : ℝ, equalityCost K weight x y = c) :=
 140  ⟨identity_from_equality K weight,
 141   non_contradiction_from_equality K weight,
 142   totality_from_function_type K weight⟩
 143