Reference · Signed rationals

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

Signed rationalssrc/rainbow/math/rational/signed/vector_sup_translation.clj0 definitions, 2 theorems

Fixed-shape translation invariance of signed-list sup distance. Vector addition truncates to the shorter list, so common translation is a metric law only when the prefix has the shape of both translated vectors. A three-list structural proof lifts scalar distance translation through signed maximum. Vector-add commutativity and sup-distance congruence derive the right-translation orientation. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.signed.distance-translationmath.rational.signed.vector-sup-congruencemath.linear.vector.add-ordermath.linear.vector.shape-cancellation

vector/sup-distance-add-left-same-shape :
  (prefix left right : List ℚ) (prefix-left : vector/same-shape prefix left)
  (prefix-right : vector/same-shape prefix right)
  → vector/sup-distance (vector/add prefix left) (vector/add prefix right) = vector/sup-distance left right

vector/sup-distance-add-right-same-shape :
  (left right suffix : List ℚ) (suffix-left : vector/same-shape suffix left)
  (suffix-right : vector/same-shape suffix right)
  → vector/sup-distance (vector/add left suffix) (vector/add right suffix) = vector/sup-distance left right