Reference · Vectors

rainbow.math.linear.vector.shape-map

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

Componentwise maps preserve native vector shape. The general theorem covers every signed-to-signed component mapping. Native vector negation, uniform scaling, and zero-like construction are reducible specializations. The proof is one List induction whose head obligation is signed zero reflexivity. Native and axiom-free on D63.

Depends onmath.linear.vector.shape-cancellation

vector/map-preserves-shape :
  (mapping : ℚ → ℚ) (values : List ℚ)
  → vector/same-shape (list/map ℚ ℚ mapping values) values

vector/negate-preserves-shape :
  (values : List ℚ)
  → vector/same-shape (vector/negate values) values

vector/scale-preserves-shape :
  (rate : ℚ≥0) (values : List ℚ)
  → vector/same-shape (vector/scale rate values) values

vector/zero-like-preserves-shape :
  (values : List ℚ)
  → vector/same-shape (vector/zero-like values) values