identity_implies_normalized

formal source

 164/-- **Translation lemma 1 (Identity ⇒ Normalization)**: If a comparison
 165operator satisfies Identity, then the derived cost function takes value
 166zero at the multiplicative identity. -/
 167theorem identity_implies_normalized (C : ComparisonOperator)
 168    (hId : Identity C) :
 169    IsNormalized (derivedCost C) := by
 170  unfold IsNormalized derivedCost
 171  exact hId 1 one_pos
 172
 173/-- **Translation lemma 2 (Non-contradiction + Scale invariance ⇒ Reciprocity)**:
 174If a comparison operator is single-valued under argument reordering and
 175depends only on ratios, then the derived cost function is invariant under
 176inversion of its argument: F(x) = F(1/x).
 177
 178The chain of equalities:
 179  F(x) = C(x, 1)                       definition of derivedCost
 180       = C(1, x)                       non-contradiction
 181       = C(x⁻¹·1, x⁻¹·x)               scale invariance (multiply both args by x⁻¹)
 182       = C(x⁻¹, 1)                     simplify (x⁻¹·1 = x⁻¹, x⁻¹·x = 1)
 183       = F(x⁻¹)                        definition of derivedCost
 184-/
 185theorem non_contradiction_and_scale_imply_reciprocal
 186    (C : ComparisonOperator)
 187    (hNC : NonContradiction C)
 188    (hSI : ScaleInvariant C) :
 189    IsSymmetric (derivedCost C) := by
 190  intro x hx
 191  have hxinv : (0 : ℝ) < x⁻¹ := inv_pos.mpr hx
 192  have hx_ne : (x : ℝ) ≠ 0 := ne_of_gt hx
 193  -- Step 1: C(x, 1) = C(1, x) by non-contradiction.
 194  have h1 : C x 1 = C 1 x := hNC x 1 hx one_pos
 195  -- Step 2: scale invariance with x' = 1, y' = x, λ = x⁻¹ gives
 196  --   C(x⁻¹·1, x⁻¹·x) = C(1, x), so C(1, x) = C(x⁻¹·1, x⁻¹·x).
 197  have h2 : C 1 x = C (x⁻¹ * 1) (x⁻¹ * x) :=