Reference · Matrices

rainbow.math.linear.matrix.affine-residual

Matricessrc/rainbow/math/linear/matrix/affine_residual.clj0 definitions, 3 theorems

Shape-safe residual characterization of affine fixed points. For `F(x) = offset + rows*x`, the Bellman fixed-point equation `F(x) ~ x` is equivalent to the linear residual equation `x - rows*x ~ offset` when the involved vectors have the shapes required by truncating vector arithmetic. The two directions expose their minimal shape premises; the iff theorem packages both. Theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-stabilization

matrix/affine-fixed-point-implies-residual-equation :
  (rows : List (List ℚ)) (offset value : List ℚ)
  (offset-image-shape : vector/same-shape offset (matrix/vector-multiply rows value))
  (fixed : vector/equivalent (matrix/affine-action rows offset value) value)
  → vector/equivalent (subtract) offset
  where subtract := vector/subtract value (matrix/vector-multiply rows value)

matrix/affine-residual-equation-implies-fixed-point :
  (rows : List (List ℚ)) (offset value : List ℚ)
  (value-image-shape : vector/same-shape value (matrix/vector-multiply rows value))
  (residual-equation : vector/equivalent (subtract) offset)
  → vector/equivalent (matrix/affine-action rows offset value) value
  where subtract := vector/subtract value (matrix/vector-multiply rows value)

matrix/affine-fixed-point-iff-residual-equation :
  (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 (equivalent₁ → equivalent) (equivalent → equivalent₁)
  where equivalent := vector/equivalent (vector/subtract value (matrix/vector-multiply rows value)) offset
  where equivalent₁ := vector/equivalent (matrix/affine-action rows offset value) value