ExcludedMiddle

formal source

 105perturbations of cost. The mathematical counterpart of the Aristotelian
 106law A ∨ ¬A applied to continuous comparisons: there is no "neither" outcome
 107on the comparison's domain. -/
 108def ExcludedMiddle (C : ComparisonOperator) : Prop :=
 109  ContinuousOn (Function.uncurry C) (Set.Ioi (0 : ℝ) ×ˢ Set.Ioi (0 : ℝ))
 110
 111/-- **Scale invariance**: the cost of a comparison depends only on the
 112ratio of the two quantities. This is the structural bridge from a
 113two-argument comparison operator to a one-argument cost on positive ratios.
 114It is what allows the four laws of logic, which make no reference to absolute
 115scale, to be expressed as constraints on the multiplicative group ℝ₊. -/
 116def ScaleInvariant (C : ComparisonOperator) : Prop :=
 117  ∀ x y lam : ℝ, 0 < x → 0 < y → 0 < lam →
 118    C (lam * x) (lam * y) = C x y
 119
 120/-- **Route-independence (the d'Alembert form)**: the cost of any composite
 121comparison, taken in its symmetric forward-and-backward form on positive
 122ratios, is a polynomial function of the constituent ratio costs.
 123Concretely: assembling a comparison of ratio xy with a comparison of ratio
 124x/y (the symmetric forward+backward decomposition) gives a total cost that
 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