identity_from_equality

formal source

 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]
 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`. -/