Reference · Matrices

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

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

Composition and arbitrary-horizon order for finite affine iteration. Natural addition recurses on the extra-horizon argument, so affine iteration forms a finite semigroup action: running `base` steps and then `extra` steps agrees with running `extra + base` steps. Bellman subsolutions therefore stay below every later iterate, while supersolutions stay above every later iterate. Theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-trajectory-order

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

matrix/affine-iterate-subsolution-horizon :
  (rows : List (List ℚ)) (offset initial : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (subsolution : vector/at-most initial (action)) (base extra : ℕ)
  → vector/at-most (iterate₁) (iterate)
  where action := matrix/affine-action rows offset initial
  where iterate := matrix/affine-iterate rows offset (algebra/nat-add extra base) initial
  where iterate₁ := matrix/affine-iterate rows offset base initial

matrix/affine-iterate-supersolution-horizon :
  (rows : List (List ℚ)) (offset initial : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (supersolution : vector/at-most (action) initial) (base extra : ℕ)
  → vector/at-most (iterate) (iterate₁)
  where action := matrix/affine-action rows offset initial
  where iterate := matrix/affine-iterate rows offset (algebra/nat-add extra base) initial
  where iterate₁ := matrix/affine-iterate rows offset base initial