composition_consistency_not_definitional

formal source

 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
 190    simp
 191  have h1val : hammingCostOnReal weight 1 1 = 0 := by
 192    unfold hammingCostOnReal equalityCost
 193    simp
 194  have left22 : hammingCostOnReal weight (2 * 2) 1
 195                  + hammingCostOnReal weight (2 / 2) 1 = weight := by
 196    rw [hxy_a, hxy_b, h4val, h1val, add_zero]
 197  have right22 : P (hammingCostOnReal weight 2 1) (hammingCostOnReal weight 2 1)
 198                  = P weight weight := by
 199    rw [h2val]
 200  have hP22 : P weight weight = weight := by
 201    rw [← right22, ← h22, left22]
 202  -- Now take x = 2, y = 3 (so xy = 6 ≠ 1, x/y = 2/3 ≠ 1).
 203  -- C(6, 1) + C(2/3, 1) = weight + weight = 2*weight.
 204  -- P(C(2, 1), C(3, 1)) = P(weight, weight) = weight (from above).