Reference · Matrices

rainbow.math.linear.matrix.row-sum-fixed-point-uniqueness

Matricessrc/rainbow/math/linear/matrix/row_sum_fixed_point_uniqueness.clj0 definitions, 2 theorems

Fixed-point uniqueness for row-sum-contractive signed affine systems. The row-sum Lipschitz theorem bounds the distance between affine images. If both inputs are fixed points, sup-distance congruence transports that bound to a self-bound `d <= rate*d`. A supplied scalar collapse certificate turns every nonnegative self-bounded distance into zero, and fixed-shape separation then identifies the two vectors. Keeping collapse explicit cleanly separates matrix geometry from the chosen strict-rate arithmetic. Native, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.row-sum-lipschitz

matrix/affine-row-sum-fixed-points-have-zero-sup-distance :
  (rows : List (List ℚ)) (offset left right : List ℚ) (rate : ℚ)
  (rate-nonnegative : 0 ≤ rate)
  (shape : vector/same-shape left right)
  (offset-shape : vector/same-shape offset (matrix/vector-multiply rows left))
  (positive-rows : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/at-most (vector/zero-like row) row)
  (bounded-sums : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/sum row ≤ rate)
  (left-fixed : vector/equivalent (matrix/affine-action rows offset left) left)
  (right-fixed : vector/equivalent (matrix/affine-action rows offset right) right)
  (collapse : ∀ (distance : ℚ), ∀ (distance-nonnegative : 0 ≤ distance), ∀ (self-bound : distance ≤ rate · distance), distance = 0)
  → vector/sup-distance left right = 0

matrix/affine-row-sum-fixed-points-unique :
  (rows : List (List ℚ)) (offset left right : List ℚ) (rate : ℚ)
  (rate-nonnegative : 0 ≤ rate)
  (shape : vector/same-shape left right)
  (offset-shape : vector/same-shape offset (matrix/vector-multiply rows left))
  (positive-rows : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/at-most (vector/zero-like row) row)
  (bounded-sums : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/sum row ≤ rate)
  (left-fixed : vector/equivalent (matrix/affine-action rows offset left) left)
  (right-fixed : vector/equivalent (matrix/affine-action rows offset right) right)
  (collapse : ∀ (distance : ℚ), ∀ (distance-nonnegative : 0 ≤ distance), ∀ (self-bound : distance ≤ rate · distance), distance = 0)
  → vector/equivalent left right