composition_consistency_not_definitional

proof body

Tactic-mode proof.

 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).
 205  -- Contradiction: 2*weight ≠ weight when weight ≠ 0.
 206  have hxy_c : (2 : ℝ) * 3 = 6 := by norm_num
 207  have h23 : hammingCostOnReal weight (2 * 3) 1
 208              + hammingCostOnReal weight (2 / 3) 1
 209              = P (hammingCostOnReal weight 2 1) (hammingCostOnReal weight 3 1) :=
 210    hP 2 3 (by norm_num) (by norm_num)
 211  have h6val : hammingCostOnReal weight 6 1 = weight := by
 212    unfold hammingCostOnReal equalityCost
 213    have : (6 : ℝ) ≠ 1 := by norm_num
 214    simp [this]
 215  have h23val : hammingCostOnReal weight (2/3 : ℝ) 1 = weight := by
 216    unfold hammingCostOnReal equalityCost
 217    have : (2/3 : ℝ) ≠ 1 := by norm_num
 218    simp [this]
 219  have h3val : hammingCostOnReal weight 3 1 = weight := by
 220    unfold hammingCostOnReal equalityCost
 221    have : (3 : ℝ) ≠ 1 := by norm_num
 222    simp [this]
 223  have left23 : hammingCostOnReal weight (2 * 3) 1
 224                  + hammingCostOnReal weight (2 / 3) 1 = 2 * weight := by
 225    rw [hxy_c, h6val, h23val]
 226    ring
 227  have right23 : P (hammingCostOnReal weight 2 1) (hammingCostOnReal weight 3 1)
 228                  = P weight weight := by
 229    rw [h2val, h3val]
 230  have hP23 : P weight weight = 2 * weight := by
 231    rw [← right23, ← h23, left23]
 232  -- Combine: weight = 2*weight, so weight = 0, contradicting hw.
 233  have : weight = 2 * weight := hP22.symm.trans hP23
 234  have : weight = 0 := by linarith
 235  exact hw this
 236
 237/-! ## The Aristotelian Decomposition
 238
 239The headline result of this module: the four classical Aristotelian
 240conditions, when applied to an equality-derived cost on a carrier with
 241multiplicative structure, decompose into three definitional facts and
 242one substantive structural condition.
 243-/
 244
 245/-- **The Aristotelian Decomposition.** On any carrier with an
 246equality-induced cost:
 247
 248* (L1) Identity is **definitional**, forced by reflexivity of equality.
 249* (L2) Non-Contradiction is **definitional**, forced by symmetry of
 250  equality.
 251* (L3a) Totality is **definitional**, forced by the function type
 252  signature.
 253* (L4) Composition Consistency is **substantive**, requiring non-trivial
 254  compatibility between the cost and the carrier's algebraic structure;
 255  it is not derivable from the type signature alone, as witnessed by
 256-- ... 4 more lines elided ...