Reference · Signed rationals

rainbow.math.rational.signed.vector-sup-triangle

Signed rationalssrc/rainbow/math/rational/signed/vector_sup_triangle.clj0 definitions, 1 theorems

Triangle inequality for equal-shaped signed-rational list vectors. The list representation intentionally gives distance zero when either input is empty, so a global triangle law over arbitrary unequal lengths is false. Two adjacent `vector/same-shape` hypotheses rule out exactly those mismatch cases. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.signed.distance-trianglemath.rational.signed.vector-sup-distancemath.linear.vector.shape-cancellation

vector/sup-distance-triangle-same-shape :
  (left middle right : List ℚ) (left-middle : vector/same-shape left middle)
  (middle-right : vector/same-shape middle right)
  → vector/sup-distance left right ≤ vector/sup-distance left middle + vector/sup-distance middle right