Reference · Vectors

rainbow.math.linear.vector.pointwise-order

Vectors src/rainbow/math/linear/vector/pointwise_order.clj1 definitions, 4 theorems

Length-sensitive componentwise order for signed-rational vectors. vector/at-most [] [] = Truth vector/at-most [] (y :: ys) = Falsity vector/at-most (x :: xs) [] = Falsity vector/at-most (x :: xs) (y :: ys) = signed/at-most x y AND vector/at-most xs ys The definition turns scalar order certificates into a native finite-vector feasibility relation. Reflexivity and uniform-clamp monotonicity are proved structurally, without adding axioms or changing the kernel. This is deliberately distinct from signed/all-at-most: that theorem compares two functions on an explicit list of problem indices, while vector/at-most compares two native value lists by position and makes equal dimension part of the proposition.

Depends onmath.linear.vector.uniform-clamp

vector/at-most

DefinitionSource, line 63

vector/at-most :
  (x₁ x₂ : List ℚ)
  → Prop

List = data/Listℚ = signed/SignedRational

vector/at-most-empty

TheoremWorked exampleNo axiomsSource, line 105

vector/at-most-empty :
  → vector/at-most [] []

vector/at-most-cons

TheoremFor all inputsNo axiomsSource, line 110

vector/at-most-cons :
  (left-head right-head : ℚ) (left-tail right-tail : List ℚ)
  (head-ordered : left-head ≤ right-head)
  (tail-ordered : vector/at-most left-tail right-tail)
  → vector/at-most (data/cons ℚ left-head left-tail) (data/cons ℚ right-head right-tail)

List = data/Listℚ = signed/SignedRational≤ = signed/at-most

vector/at-most-reflexive

TheoremFor all inputsNo axiomsSource, line 131

vector/at-most-reflexive :
  (values : List ℚ)
  → vector/at-most values values

List = data/Listℚ = signed/SignedRational

vector/uniform-clamp-monotone

TheoremFor all inputsNo axiomsSource, line 155

vector/uniform-clamp-monotone :
  (lower upper : ℚ) (left right : List ℚ) (ordered : vector/at-most left right)
  → vector/at-most (vector/uniform-clamp lower upper left) (vector/uniform-clamp lower upper right)

List = data/Listℚ = signed/SignedRational