Reference · Vectors

rainbow.math.linear.vector.add-cancellation

Vectorssrc/rainbow/math/linear/vector/add_cancellation.clj0 definitions, 4 theorems

Shape-safe cancellation of a common vector from equivalence and order. Because native vector/add truncates, both operands must have the offset's shape. Under those hypotheses a common right or left addend cancels from vector equivalence and from vector/at-most. Proofs compose existing checked arithmetic and order laws; there is no new recursion.

Depends onmath.linear.vector.shape-add

vector/equivalent-add-right-cancel :
  (left right offset : List ℚ) (left-shape : vector/same-shape left offset)
  (right-shape : vector/same-shape right offset)
  (same : vector/equivalent (vector/add left offset) (vector/add right offset))
  → vector/equivalent left right

vector/equivalent-add-left-cancel :
  (left right offset : List ℚ) (left-shape : vector/same-shape left offset)
  (right-shape : vector/same-shape right offset)
  (same : vector/equivalent (vector/add offset left) (vector/add offset right))
  → vector/equivalent left right

vector/at-most-add-right-cancel :
  (left right offset : List ℚ) (left-shape : vector/same-shape left offset)
  (right-shape : vector/same-shape right offset)
  (ordered : vector/at-most (vector/add left offset) (vector/add right offset))
  → vector/at-most left right

vector/at-most-add-left-cancel :
  (left right offset : List ℚ) (left-shape : vector/same-shape left offset)
  (right-shape : vector/same-shape right offset)
  (ordered : vector/at-most (vector/add offset left) (vector/add offset right))
  → vector/at-most left right