NonContradiction

formal source

  97equals the cost of comparing y to x. The mathematical counterpart of the
  98Aristotelian law ¬(A ∧ ¬A): if comparison were not single-valued under
  99reordering, the same comparison would simultaneously hold and not hold. -/
 100def NonContradiction (C : ComparisonOperator) : Prop :=
 101  ∀ x y : ℝ, 0 < x → 0 < y → C x y = C y x
 102
 103/-- **Excluded middle (totality and continuity)**: every comparison returns a
 104definite real value and small perturbations of inputs give small
 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.