Reference
Vectors
44 modules in src/rainbow/math/linear/vector/. All folders
| Module | What it proves | Theorems |
|---|---|---|
| math.linear.vector.add-cancellation | Shape-safe cancellation of a common vector from equivalence and order. | 4 |
| math.linear.vector.add-order | Translation monotonicity for native signed vectors. | 6 |
| math.linear.vector.add-reorder | Four-term reordering and additive distribution for vector subtraction. | 2 |
| math.linear.vector.additive-units | Shape-preserving zero and additive-unit laws for native finite vectors. | 5 |
| math.linear.vector.convex-combination | Normalized two-point convex combinations preserve vector intervals. | 10 |
| math.linear.vector.dot-additive | Additivity of the native dot product in its first vector argument. | 1 |
| math.linear.vector.dot-bilinear | Right additivity of the native dot product, completing additive bilinearity. | 1 |
| math.linear.vector.dot-commutative | Commutativity of the native truncating signed-vector dot product. | 1 |
| math.linear.vector.dot-congruence | Quotient-safe congruence of the native vector dot product. | 3 |
| math.linear.vector.dot-distance-bound | Componentwise distance accounting for signed dot products. | 2 |
| math.linear.vector.dot-negate | Negation laws for signed multiplication and the native vector dot product. | 5 |
| math.linear.vector.dot-scale | Homogeneity of the native vector dot product in its first argument. | 5 |
| math.linear.vector.dot-subtract | Subtraction laws for signed values and the native vector dot product. | 3 |
| math.linear.vector.dot-zero-laws | Zero laws for the native dot product and exact squared norm. | 4 |
| math.linear.vector.equivalence | Componentwise equivalence of signed-rational vectors: two vectors are equivalent when every pair of components is signed-equivalent. | 5 |
| math.linear.vector.equivalence-laws | Structural laws for length-sensitive componentwise signed-vector equivalence. | 5 |
| math.linear.vector.equivalence-transitivity | Transitivity of length-sensitive componentwise vector equivalence. | 1 |
| math.linear.vector.negate-additive | Native vector negation distributes over native vector addition. | 1 |
| math.linear.vector.negate-reflection | Involutive vector negation reflects order and equivalence. | 2 |
| math.linear.vector.norm | The Euclidean vector norm over signed-rational vectors, built from the inner product and the perfect-square root witness: norm-squared v = <v, v> is-norm v n <=> n * n ~ <v, v> The squared norm is exact (a dot product); the norm itself is exact only on perfect-square instances (a witness n with n*n ~ norm-squared). | 3 |
| math.linear.vector.norm-congruence | Quotient-safe congruence laws for native squared norms and norm witnesses. | 2 |
| math.linear.vector.norm-expansion | Exact quadratic expansions for the native signed squared norm. | 2 |
| math.linear.vector.norm-laws | Algebraic laws for the exact signed squared norm. | 2 |
| math.linear.vector.norm-nonnegative | Constructive nonnegativity of signed squares and native squared norms. | 3 |
| math.linear.vector.norm-parallelogram | The exact parallelogram identity for native signed vectors. | 2 |
| math.linear.vector.norm-pythagorean | Pythagoras and order bounds for native signed-rational vectors. | 3 |
| math.linear.vector.norm-witness-laws | Transformation laws for exact native norm witnesses. | 3 |
| math.linear.vector.norm-zero-characterization | The proved forward zero-characterization for native exact norms. | 2 |
| math.linear.vector.norm-zero-reflection | Zero squared norm reflects componentwise zero for finite signed vectors. | 2 |
| math.linear.vector.pointwise-order | Length-sensitive componentwise order for signed-rational vectors. | 4 |
| math.linear.vector.pointwise-order-laws | Partial-order laws and order-reversing negation for signed vectors. | 5 |
| math.linear.vector.projected-gradient | Projected-gradient steps on finite signed-rational vectors. | 4 |
| math.linear.vector.row-sum-lipschitz | Nonnegative row-sum Lipschitz bounds for signed dot products. | 3 |
| math.linear.vector.scale-additive | Uniform nonnegative scaling distributes over native vector addition. | 1 |
| math.linear.vector.scale-composition | Composition of uniform nonnegative scaling on native signed vectors. | 1 |
| math.linear.vector.scale-order | Nonnegative-rational scaling preserves native positional vector order. | 2 |
| math.linear.vector.scale-subtract | Uniform nonnegative scaling commutes with negation and subtraction. | 2 |
| math.linear.vector.shape-add | Shape preservation for truncating vector addition and subtraction. | 4 |
| math.linear.vector.shape-cancellation | Shape equality and sound cancellation for truncating vector arithmetic. | 5 |
| math.linear.vector.shape-map | Componentwise maps preserve native vector shape. | 4 |
| math.linear.vector.subtract-cancellation | Shape-safe cancellation through native vector subtraction. | 4 |
| math.linear.vector.subtract-laws | Congruence and mixed-variance order laws for native vector subtraction. | 4 |
| math.linear.vector.subtract-negation | Interaction laws between native vector subtraction and negation. | 2 |
| math.linear.vector.uniform-clamp | Uniform box projection for finite signed-rational vectors. | 6 |