totality_from_function_type

formal source

 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
 144/-! ## The Substantive Condition: Composition Consistency
 145
 146The fourth Aristotelian condition, Composition Consistency, is not
 147type-theoretic. It requires the cost to be compatible with the
 148carrier's algebraic structure. We make this precise by exhibiting a
 149comparison operator that satisfies the three definitional conditions
 150but fails Composition Consistency, demonstrating that (L4) is
 151genuinely substantive.
 152-/
 153
 154/-- The Aristotelian condition (L4) **Composition Consistency** in
 155abstract form: there exists a combiner `P` such that the cost of any
 156composite operation is determined by the costs of its components,