Reference · Matrices

rainbow.math.linear.matrix.affine-general-rate-uniqueness

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

Fixed-point uniqueness for every canonical rational row-sum contraction. The scalar theorem constructs the collapse certificate missing from the generic row-sum geometry. For `gamma=a/(a+g)`, a nonnegative distance with d <= gamma*d is treated as the zero-residual case of the inverse-gap theorem, yielding `d <= ((a+g)/g)*0 ~ 0`; antisymmetry then gives `d ~ 0`. Instantiating the existing affine row-sum uniqueness interface removes the practical `gamma <= 1/2` restriction from exact fixed-point uniqueness. Theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-general-rate-certificate

signed/general-rate-contraction-collapse :
  (ap gp : ℕ) (distance : ℚ)
  (distance-nonnegative : 0 ≤ distance)
  (self-bound : distance ≤ signed/from-nnrat (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) · distance)
  → distance = 0

matrix/affine-general-rate-fixed-points-have-zero-sup-distance :
  (rows : List (List ℚ)) (offset left right : List ℚ) (ap gp : ℕ)
  (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 ≤ signed/from-nnrat (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))))
  (left-fixed : vector/equivalent (matrix/affine-action rows offset left) left)
  (right-fixed : vector/equivalent (matrix/affine-action rows offset right) right)
  → vector/sup-distance left right = 0

matrix/affine-general-rate-fixed-points-unique :
  (rows : List (List ℚ)) (offset left right : List ℚ) (ap gp : ℕ)
  (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 ≤ signed/from-nnrat (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))))
  (left-fixed : vector/equivalent (matrix/affine-action rows offset left) left)
  (right-fixed : vector/equivalent (matrix/affine-action rows offset right) right)
  → vector/equivalent left right