RouteIndependence

formal source

 125is some fixed polynomial in the costs of the individual ratios x and y.
 126The polynomial restriction is the Level-1 regularity assumption; Level 2
 127will replace it with continuity. -/
 128def RouteIndependence (C : ComparisonOperator) : Prop :=
 129  ∃ P : ℝ → ℝ → ℝ,
 130    -- P is a polynomial in two variables of degree ≤ 2.
 131    (∃ a b c d e f : ℝ, ∀ u v, P u v = a + b*u + c*v + d*u*v + e*u^2 + f*v^2) ∧
 132    -- P is symmetric (consequence of non-contradiction at the combiner level).
 133    (∀ u v, P u v = P v u) ∧
 134    -- The d'Alembert composition law on the derived cost function.
 135    (∀ x y : ℝ, 0 < x → 0 < y →
 136       derivedCost C (x * y) + derivedCost C (x / y)
 137       = P (derivedCost C x) (derivedCost C y))
 138
 139/-- A comparison operator is **non-trivial** if there exists at least one
 140positive ratio with non-zero cost. (Without this assumption the constant zero
 141function vacuously satisfies all the constraints.) -/
 142def NonTrivial (C : ComparisonOperator) : Prop :=
 143  ∃ x : ℝ, 0 < x ∧ derivedCost C x ≠ 0
 144
 145/-- A comparison operator **satisfies the laws of logic** if all four
 146Aristotelian constraints hold, together with scale invariance (the bridge
 147from two-argument to one-argument form) and non-triviality (so that the
 148derived cost is not vacuously zero). -/
 149structure SatisfiesLawsOfLogic (C : ComparisonOperator) : Prop where
 150  identity            : Identity C
 151  non_contradiction   : NonContradiction C
 152  excluded_middle     : ExcludedMiddle C
 153  scale_invariant     : ScaleInvariant C
 154  route_independence  : RouteIndependence C
 155  non_trivial         : NonTrivial C
 156
 157/-! ## Translation Lemmas
 158