CompositionConsistency

formal source

 156composite operation is determined by the costs of its components,
 157with the components combined under the carrier's algebraic structure.
 158Specialised to `(ℝ_{>0}, ·)`: -/
 159def CompositionConsistency (C : ℝ → ℝ → ℝ) : Prop :=
 160  ∃ P : ℝ → ℝ → ℝ,
 161    ∀ x y : ℝ, 0 < x → 0 < y →
 162      C (x * y) 1 + C (x / y) 1 = P (C x 1) (C y 1)
 163
 164/-- The equality-induced cost on `ℝ`, taken with the multiplicative
 165identity `1` as base point. -/
 166noncomputable def hammingCostOnReal (weight : ℝ) : ℝ → ℝ → ℝ :=
 167  equalityCost ℝ weight
 168
 169/-- **The substantive content of (L4).** The equality-induced cost on
 170`(ℝ_{>0}, ·)` with positive weight does **not** satisfy Composition
 171Consistency. This shows that (L4) is not a definitional fact: it is a
 172genuine structural condition that imposes non-trivial compatibility
 173between the cost and the carrier's multiplicative structure. -/
 174theorem composition_consistency_not_definitional (weight : ℝ) (hw : weight ≠ 0) :
 175    ¬ CompositionConsistency (hammingCostOnReal weight) := by
 176  intro ⟨P, hP⟩
 177  -- Take x = 2, y = 2 (so xy = 4 ≠ 1, x/y = 1).
 178  -- Then C(4, 1) + C(1, 1) = weight + 0 = weight.
 179  -- And P(C(2, 1), C(2, 1)) = P(weight, weight).
 180  have hxy_a : (2 : ℝ) * 2 = 4 := by norm_num
 181  have hxy_b : (2 : ℝ) / 2 = 1 := by norm_num
 182  have h22 : hammingCostOnReal weight (2 * 2) 1 + hammingCostOnReal weight (2 / 2) 1
 183              = P (hammingCostOnReal weight 2 1) (hammingCostOnReal weight 2 1) :=
 184    hP 2 2 (by norm_num) (by norm_num)
 185  have h2val : hammingCostOnReal weight 2 1 = weight := by
 186    unfold hammingCostOnReal equalityCost
 187    simp
 188  have h4val : hammingCostOnReal weight 4 1 = weight := by
 189    unfold hammingCostOnReal equalityCost