Reference
Matrices
100 modules in src/rainbow/math/linear/matrix/. All folders
| Module | What it proves | Theorems |
|---|---|---|
| math.linear.matrix.action-associative | Finite matrix action is adjoint to native transpose. | 6 |
| math.linear.matrix.action-prepend | Action laws for inserting a leading column into a native finite matrix. | 5 |
| math.linear.matrix.action-scale | Arbitrary signed-scalar vector scaling for native matrix algebra. | 4 |
| math.linear.matrix.action-sup-bound | Lift rowwise dot-distance bounds to a matrix-action sup bound. | 1 |
| math.linear.matrix.add | Length-sensitive shape, addition, and left distributivity for matrices. | 3 |
| math.linear.matrix.add-algebra | Commutative, associative, quotient-safe native matrix addition. | 5 |
| math.linear.matrix.add-order | Pointwise order laws for native matrix addition and subtraction. | 6 |
| math.linear.matrix.add-right | Transpose additivity and right distributivity for native matrices. | 4 |
| math.linear.matrix.add-shape | Equivalence laws for matrix shape and shape preservation by addition. | 3 |
| math.linear.matrix.additive-group | Shaped zero, negation, subtraction, and inverse laws for matrices. | 8 |
| math.linear.matrix.affine-approximate-fixed-point | Constructive approximate fixed points from affine residual convergence. | 4 |
| math.linear.matrix.affine-approximate-offset-stability | Robust stability for approximate solutions under offset perturbation. | 2 |
| math.linear.matrix.affine-approximate-stability | A posteriori stability of approximate affine fixed points. | 3 |
| math.linear.matrix.affine-bracket-collapse | Exact convergence certificates from collapsed affine brackets. | 3 |
| math.linear.matrix.affine-bracket-uniqueness | Affine fixed-point uniqueness inside a collapsed monotone bracket. | 2 |
| math.linear.matrix.affine-equivalence | Congruence and fixed-point invariance for signed affine value iteration. | 7 |
| math.linear.matrix.affine-fixed-point-order | Order bounds for finite signed affine iteration around a fixed point. | 2 |
| math.linear.matrix.affine-general-rate-certificate | Sharp affine residual certificates for every canonical rational rate below one. | 7 |
| math.linear.matrix.affine-general-rate-iterate-certificate | Sharp finite-horizon iterate error at every canonical rational rate. | 2 |
| math.linear.matrix.affine-general-rate-sensitivity | Sharp robustness certificates for arbitrary-rate affine problem drift. | 4 |
| math.linear.matrix.affine-general-rate-tail-certificate | Sharp fixed-point-free tail certificates at arbitrary rational rates. | 2 |
| math.linear.matrix.affine-general-rate-uniqueness | Fixed-point uniqueness for every canonical rational row-sum contraction. | 3 |
| math.linear.matrix.affine-half-iterate-contraction | Shape preservation and one-step contraction for half-row affine iteration. | 3 |
| math.linear.matrix.affine-half-iterate-converges | Rate-null convergence for half-row signed affine iteration. | 6 |
| math.linear.matrix.affine-half-iterate-rate | Finite-horizon geometric rate for half-row signed affine iteration. | 5 |
| math.linear.matrix.affine-horizon-order | Composition and arbitrary-horizon order for finite affine iteration. | 3 |
| math.linear.matrix.affine-invariant-interval | Invariant intervals for finite signed affine value iteration. | 3 |
| math.linear.matrix.affine-inverse-gap-certificate | Sharp residual certificates for arbitrary strict contraction rates. | 3 |
| math.linear.matrix.affine-inverse-gap-stability | Sharp stability of two approximate affine solutions at arbitrary rates. | 6 |
| math.linear.matrix.affine-iterate | Finite signed value iteration for affine matrix maps. | 5 |
| math.linear.matrix.affine-nnrat-exact-rate | Exact NNRAT-rate contraction and residual certificates. | 8 |
| math.linear.matrix.affine-nnrat-exact-rate-null | Null-sequence bridges for exact NNRAT contraction envelopes. | 5 |
| math.linear.matrix.affine-offset-sensitivity | Sensitivity of contractive affine fixed points to offset perturbations. | 3 |
| math.linear.matrix.affine-operator-sensitivity | Approximate-solution stability across certified affine-map perturbations. | 3 |
| math.linear.matrix.affine-order | Order and interval laws for signed affine finite-matrix action. | 16 |
| math.linear.matrix.affine-problem-sensitivity | End-to-end robustness for approximate affine optimization problems. | 2 |
| math.linear.matrix.affine-residual | Shape-safe residual characterization of affine fixed points. | 3 |
| math.linear.matrix.affine-residual-bracket | Nested finite-horizon affine brackets from linear residual certificates. | 1 |
| math.linear.matrix.affine-residual-certificate | A posteriori error certificates for contractive signed affine systems. | 4 |
| math.linear.matrix.affine-residual-decay | Geometric decay and finite-horizon error bounds from computable residuals. | 4 |
| math.linear.matrix.affine-residual-iteration | Finite value-iteration guarantees from linear residual inequalities. | 3 |
| math.linear.matrix.affine-residual-order | Residual order certificates for affine subsolutions and supersolutions. | 6 |
| math.linear.matrix.affine-residual-stopping | Exact residual stopping certificates for finite affine value iteration. | 3 |
| math.linear.matrix.affine-residual-uniqueness | Uniqueness of enclosed affine residual solutions after bracket collapse. | 2 |
| math.linear.matrix.affine-sign | Cone preservation for vector addition and signed affine matrix action. | 6 |
| math.linear.matrix.affine-stabilization | Exact finite stabilization of signed affine value iteration. | 3 |
| math.linear.matrix.affine-strong-row-contraction | User-facing contraction results for any NNRAT row bound gamma <= 1/2. | 7 |
| math.linear.matrix.affine-sup-distance | Sup-distance cancellation and bound transfer for signed affine action. | 2 |
| math.linear.matrix.affine-tail-diameter | Constructive tail diameter for contractive affine iteration. | 4 |
| math.linear.matrix.affine-trajectory-order | Successive-order laws for finite signed affine value iteration. | 3 |
| math.linear.matrix.antitone | Antitonicity of native dot products, matrix action, and multiplication. | 8 |
| math.linear.matrix.associativity-counterexample | A checked counterexample to unrestricted native matrix associativity. | 5 |
| math.linear.matrix.composable | Dimension certificates for native finite matrix composition. | 6 |
| math.linear.matrix.composable-multiply | Closure of matrix composability under native multiplication bracketings. | 3 |
| math.linear.matrix.composable-transpose | Composable native matrix pairs reverse under transpose. | 1 |
| math.linear.matrix.equivalence | Length-sensitive, row-wise equivalence for native finite matrices. | 4 |
| math.linear.matrix.equivalence-shape | Shape transport for length-sensitive native matrix equivalence. | 4 |
| math.linear.matrix.gram-kernel | The zero kernel of the native Gram quadratic form. | 5 |
| math.linear.matrix.gram-positive | Positive-semidefinite Gram action for native signed matrices. | 3 |
| math.linear.matrix.half-row-sum-fixed-point-uniqueness | Concrete half-contractive uniqueness for signed affine row-sum systems. | 6 |
| math.linear.matrix.interval-order | Interval propagation for signed vectors and native finite matrices. | 10 |
| math.linear.matrix.least-squares-equality | Equality and nullspace directions in exact finite least squares. | 5 |
| math.linear.matrix.least-squares-normal | Normal-equation sufficiency for exact finite least squares. | 3 |
| math.linear.matrix.linear | Shape and scalar-linearity laws for native matrix-vector multiplication. | 3 |
| math.linear.matrix.mixed-sign-action | Mixed-sign laws for signed dot products and native matrix action. | 10 |
| math.linear.matrix.mixed-sign-multiply | Mixed-sign laws for native finite matrix multiplication. | 5 |
| math.linear.matrix.multiply | Native matrix multiplication for row-major finite signed matrices. | 5 |
| math.linear.matrix.multiply-associative | Associativity of composable native finite matrix multiplication. | 3 |
| math.linear.matrix.multiply-shape | Unconditional output-shape laws for native matrix multiplication. | 4 |
| math.linear.matrix.negate-linear | Negation commutes with native matrix action, transpose, and multiplication. | 5 |
| math.linear.matrix.pointwise-order-laws | Partial-order and quotient-transport laws for native finite matrices. | 6 |
| math.linear.matrix.positive-action | Positive dot products and monotone native matrix-vector action. | 7 |
| math.linear.matrix.positive-multiply | Nonnegativity and monotonicity of native finite matrix multiplication. | 4 |
| math.linear.matrix.prepend-add | Shape-safe additivity of total column insertion. | 3 |
| math.linear.matrix.row-gram | Symmetry and positive semidefiniteness of the native row Gram product. | 3 |
| math.linear.matrix.row-gram-kernel | Zero-kernel characterization for the native row Gram product AA^T. | 3 |
| math.linear.matrix.row-length-decider | Executable, sound dimension checking for finite signed matrices. | 8 |
| math.linear.matrix.row-length-shape | Bridges executable row-length evidence to abstract matrix shape certificates. | 6 |
| math.linear.matrix.row-sum-fixed-point-uniqueness | Fixed-point uniqueness for row-sum-contractive signed affine systems. | 2 |
| math.linear.matrix.row-sum-lipschitz | Sup-Lipschitz bounds for nonnegative row-sum-bounded affine matrices. | 2 |
| math.linear.matrix.shape | Explicit width and rectangularity certificates for nested-List matrices. | 7 |
| math.linear.matrix.signed-scale | Arbitrary signed-scalar homogeneity for native finite matrices. | 3 |
| math.linear.matrix.signed-scale-algebra | Additivity and composition of arbitrary signed matrix scaling. | 6 |
| math.linear.matrix.signed-scale-antitone | Nonpositive signed factors reverse scalar, vector, and matrix order. | 5 |
| math.linear.matrix.signed-scale-congruence | Quotient congruence for signed scalar, vector, and matrix scaling. | 9 |
| math.linear.matrix.signed-scale-order | Pointwise matrix order and monotonicity of signed module scaling. | 6 |
| math.linear.matrix.signed-scale-positive | Zero-value and nonnegativity laws for signed module scaling. | 6 |
| math.linear.matrix.signed-scale-right | The complementary half of arbitrary signed matrix bilinearity. | 4 |
| math.linear.matrix.signed-scale-sign | The remaining sign combinations for signed scalar, vector, and matrix scaling. | 9 |
| math.linear.matrix.signed-scale-subtract | Negation and subtraction laws for signed multiplication and module scaling. | 14 |
| math.linear.matrix.signed-scale-units | Scalar-factor additivity and zero/one laws for signed matrix scaling. | 9 |
| math.linear.matrix.subtract-linear | Subtraction commutes with native matrix action, transpose, and products. | 4 |
| math.linear.matrix.transpose | Total transpose primitives for row-major finite signed matrices. | 5 |
| math.linear.matrix.transpose-equivalence | Congruence laws for total native matrix transpose. | 4 |
| math.linear.matrix.transpose-involution | Algebraic foundations for nondegenerate transpose involution. | 2 |
| math.linear.matrix.transpose-involution-positive | Transpose involution for rectangular matrices of positive width. | 2 |
| math.linear.matrix.transpose-multiply | Transpose/product structure for nonempty native finite matrices. | 4 |
| math.linear.matrix.transpose-multiply-reverse | Transpose reverses native matrix multiplication at positive width. | 2 |
| math.linear.matrix.transpose-order | Pointwise order and nonnegativity for total native matrix transpose. | 4 |
| math.linear.matrix.transpose-shape | Rectangularity laws for total native matrix transpose. | 7 |