Reference · Matrices

rainbow.math.linear.matrix.affine-residual-order

Matricessrc/rainbow/math/linear/matrix/affine_residual_order.clj0 definitions, 6 theorems

Residual order certificates for affine subsolutions and supersolutions. For `F(x) = offset + rows*x`, a Bellman subsolution `x <= F(x)` is equivalent to the residual upper bound `x - rows*x <= offset`; dually, a supersolution `F(x) <= x` is equivalent to `offset <= x - rows*x`. Directional theorems expose the minimal cancellation shape premise and iff theorems package both directions. Theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-residual-stopping

matrix/affine-subsolution-implies-residual-upper-bound :
  (rows : List (List ℚ)) (offset value : List ℚ)
  (offset-image-shape : vector/same-shape offset (matrix/vector-multiply rows value))
  (subsolution : vector/at-most value (matrix/affine-action rows offset value))
  → vector/at-most (subtract) offset
  where subtract := vector/subtract value (matrix/vector-multiply rows value)

matrix/affine-residual-upper-bound-implies-subsolution :
  (rows : List (List ℚ)) (offset value : List ℚ)
  (value-image-shape : vector/same-shape value (matrix/vector-multiply rows value))
  (residual-upper : vector/at-most (subtract) offset)
  → vector/at-most value (matrix/affine-action rows offset value)
  where subtract := vector/subtract value (matrix/vector-multiply rows value)

matrix/affine-subsolution-iff-residual-upper-bound :
  (rows : List (List ℚ)) (offset value : List ℚ)
  (offset-image-shape : vector/same-shape offset (matrix/vector-multiply rows value))
  (value-image-shape : vector/same-shape value (matrix/vector-multiply rows value))
  → proposition/conjunction (most₁ → most) (most → most₁)
  where most := vector/at-most (vector/subtract value (matrix/vector-multiply rows value)) offset
  where most₁ := vector/at-most value (matrix/affine-action rows offset value)

matrix/affine-supersolution-implies-residual-lower-bound :
  (rows : List (List ℚ)) (offset value : List ℚ)
  (offset-image-shape : vector/same-shape offset (matrix/vector-multiply rows value))
  (supersolution : vector/at-most (matrix/affine-action rows offset value) value)
  → vector/at-most offset (subtract)
  where subtract := vector/subtract value (matrix/vector-multiply rows value)

matrix/affine-residual-lower-bound-implies-supersolution :
  (rows : List (List ℚ)) (offset value : List ℚ)
  (value-image-shape : vector/same-shape value (matrix/vector-multiply rows value))
  (residual-lower : vector/at-most offset (subtract))
  → vector/at-most (matrix/affine-action rows offset value) value
  where subtract := vector/subtract value (matrix/vector-multiply rows value)

matrix/affine-supersolution-iff-residual-lower-bound :
  (rows : List (List ℚ)) (offset value : List ℚ)
  (offset-image-shape : vector/same-shape offset (matrix/vector-multiply rows value))
  (value-image-shape : vector/same-shape value (matrix/vector-multiply rows value))
  → proposition/conjunction (most₁ → most) (most → most₁)
  where most := vector/at-most offset (vector/subtract value (matrix/vector-multiply rows value))
  where most₁ := vector/at-most (matrix/affine-action rows offset value) value