Reference · Vectors

rainbow.math.linear.vector.pointwise-order-laws

Vectorssrc/rainbow/math/linear/vector/pointwise_order_laws.clj0 definitions, 5 theorems

Partial-order laws and order-reversing negation for signed vectors. `vector/at-most` is transitive, negation reverses it componentwise, and mutual componentwise order implies `vector/equivalent`. The latter is the correct antisymmetry conclusion for Grothendieck-pair signed rationals, whose mathematical equality is represented by signed/equivalent rather than raw pair equality. Dimension mismatch is handled constructively: vector/at-most reduces to proposition/falsity when exactly one list is empty, and those impossible witnesses eliminate the mismatch branches. Native and axiom-free on D63.

Depends onmath.finite.vectormath.linear.vector.pointwise-order

vector/negate-reverses-order :
  (left right : List ℚ) (ordered : vector/at-most left right)
  → vector/at-most (vector/negate right) (vector/negate left)

vector/at-most-transitive :
  (left middle right : List ℚ) (left-middle : vector/at-most left middle)
  (middle-right : vector/at-most middle right)
  → vector/at-most left right

vector/at-most-antisymmetric :
  (left right : List ℚ) (forward : vector/at-most left right)
  (backward : vector/at-most right left)
  → vector/equivalent left right

vector/equivalent-to-mutual-at-most :
  (left right : List ℚ) (same : vector/equivalent left right)
  → proposition/conjunction (vector/at-most left right) (vector/at-most right left)

vector/equivalent-to-at-most :
  (left right : List ℚ) (same : vector/equivalent left right)
  → vector/at-most left right