113theorem non_contradiction_from_equality (K : Type*) (weight : ℝ) : 114 ∀ x y : K, equalityCost K weight x y = equalityCost K weight y x := by
proof body
Term-mode proof.
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. -/
used by (6)
From the project-wide theorem graph. These declarations reference this one in their body.