Reference · Matrices

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

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

Exact residual stopping certificates for finite affine value iteration. At any finite step, consecutive iterate equivalence is equivalent to the current linear residual equation `x - rows*x ~ offset`, under the explicit shape premises required by truncating vector subtraction. This connects an observable value-iteration stopping condition directly to the policy- evaluation equation. Theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-residual

matrix/affine-iterate-stable-implies-residual-equation :
  (rows : List (List ℚ)) (offset initial : List ℚ) (base : ℕ)
  (offset-image-shape : vector/same-shape offset (matrix/vector-multiply rows (matrix/affine-iterate rows offset base initial)))
  (stable : vector/equivalent (matrix/affine-iterate rows offset base initial) (iterate))
  → vector/equivalent (subtract) offset
  where iterate := matrix/affine-iterate rows offset (data/succ base) initial
  where subtract := vector/subtract (matrix/affine-iterate rows offset base initial) (matrix/vector-multiply rows (matrix/affine-iterate rows offset base initial))

matrix/affine-iterate-residual-equation-implies-stable :
  (rows : List (List ℚ)) (offset initial : List ℚ) (base : ℕ)
  (value-image-shape : vector/same-shape (matrix/affine-iterate rows offset base initial) (matrix/vector-multiply rows (matrix/affine-iterate rows offset base initial)))
  (residual-equation : vector/equivalent (subtract) offset)
  → vector/equivalent (matrix/affine-iterate rows offset base initial) (iterate)
  where iterate := matrix/affine-iterate rows offset (data/succ base) initial
  where subtract := vector/subtract (matrix/affine-iterate rows offset base initial) (matrix/vector-multiply rows (matrix/affine-iterate rows offset base initial))

matrix/affine-iterate-stable-iff-residual-equation :
  (rows : List (List ℚ)) (offset initial : List ℚ) (base : ℕ)
  (offset-image-shape : vector/same-shape offset (matrix/vector-multiply rows (matrix/affine-iterate rows offset base initial)))
  (value-image-shape : vector/same-shape (matrix/affine-iterate rows offset base initial) (matrix/vector-multiply rows (matrix/affine-iterate rows offset base initial)))
  → proposition/conjunction (equivalent₁ → equivalent) (equivalent → equivalent₁)
  where equivalent := vector/equivalent (vector/subtract (matrix/affine-iterate rows offset base initial) (matrix/vector-multiply rows (matrix/affine-iterate rows offset base initial))) offset
  where equivalent₁ := vector/equivalent (matrix/affine-iterate rows offset base initial) (matrix/affine-iterate rows offset (data/succ base) initial)