Reference · Signed rationals

rainbow.math.rational.signed.distance-translation

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

Translation invariance of quotient-safe signed distance. A verified NNRat ring certificate first cancels a common signed prefix from subtraction. Absolute-value congruence lifts that identity to distance, and additive commutativity supplies the right-translation orientation. These are the scalar cancellation laws required to remove the offset from affine sup-distance bounds. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.nnrat.ringmath.rational.signed.distance

signed/subtract-add-left :
  (prefix left right : ℚ)
  → prefix + left - (prefix + right) = left - right

signed/distance-add-left :
  (prefix left right : ℚ)
  → signed/distance (prefix + left) (prefix + right) = signed/distance left right

signed/distance-add-right :
  (left right suffix : ℚ)
  → signed/distance (left + suffix) (right + suffix) = signed/distance left right