Reference · Signed rationals

rainbow.math.rational.signed.order

Signed rationalssrc/rainbow/math/rational/signed/order.clj1 definitions, 2 theorems

Order and structural laws for signed rationals. The signed order a <= b is the additive comparison pos(a) + neg(b) <= pos(b) + neg(a), reusing the nonnegative-rational order without any primitive subtraction. This is the foundation for signed minima and maxima (e.g. STL robustness) and for monotonicity results over descent and learning trajectories.

signed/at-most :
  (x₁ x₂ : ℚ)
  → Prop

signed/at-most-reflexive :
  (value : ℚ)
  → value ≤ value

signed/negate-involutive :
  (value : ℚ)
  → signed/negate (signed/negate value) = value