Reference · Matrices

rainbow.math.linear.matrix.affine-stabilization

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

Exact finite stabilization of signed affine value iteration. If two consecutive affine iterates are equivalent, the earlier iterate is a certified fixed point. Iteration composition then proves every later finite iterate equivalent to that value and, consequently, every pair of later iterates equivalent to each other. No positivity premise is needed. Theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-invariant-interval

matrix/affine-iterate-stable-implies-fixed-point :
  (rows : List (List ℚ)) (offset initial : List ℚ) (base : ℕ)
  (stable : vector/equivalent (matrix/affine-iterate rows offset base initial) (iterate))
  → vector/equivalent (action) (matrix/affine-iterate rows offset base initial)
  where action := matrix/affine-action rows offset (matrix/affine-iterate rows offset base initial)
  where iterate := matrix/affine-iterate rows offset (data/succ base) initial

matrix/affine-iterate-stabilizes :
  (rows : List (List ℚ)) (offset initial : List ℚ) (base : ℕ)
  (stable : vector/equivalent (iterate₂) (iterate₁)) (extra : ℕ)
  → vector/equivalent (iterate) (iterate₂)
  where iterate := matrix/affine-iterate rows offset (algebra/nat-add extra base) initial
  where iterate₁ := matrix/affine-iterate rows offset (data/succ base) initial
  where iterate₂ := matrix/affine-iterate rows offset base initial

matrix/affine-iterate-stable-tail-equivalent :
  (rows : List (List ℚ)) (offset initial : List ℚ) (base : ℕ)
  (stable : vector/equivalent (iterate₃) (iterate₂)) (left-extra right-extra : ℕ)
  → vector/equivalent (iterate₁) (iterate)
  where iterate := matrix/affine-iterate rows offset (algebra/nat-add right-extra base) initial
  where iterate₁ := matrix/affine-iterate rows offset (algebra/nat-add left-extra base) initial
  where iterate₂ := matrix/affine-iterate rows offset (data/succ base) initial
  where iterate₃ := matrix/affine-iterate rows offset base initial