Reference · Signed rationals

rainbow.math.rational.signed.distance-triangle

Signed rationalssrc/rainbow/math/rational/signed/distance_triangle.clj0 definitions, 3 theorems

Triangle laws for quotient-safe signed absolute value and distance. The scalar proof is split into reusable algebra: subtraction through an intermediate point, subadditivity of absolute value, and then the distance triangle inequality. Signed equivalence, rather than structural equality, is used throughout. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.nnrat.ringmath.rational.signed.distancemath.rational.signed.order-monotone

signed/subtract-chain :
  (left middle right : ℚ)
  → left - right = left - middle + (middle - right)

signed/absolute-add-triangle :
  (left right : ℚ)
  → signed/absolute (left + right) ≤ signed/absolute left + signed/absolute right

signed/distance-triangle :
  (left middle right : ℚ)
  → signed/distance left right ≤ signed/distance left middle + signed/distance middle right