Reference · Matrices

rainbow.math.linear.matrix.affine-bracket-uniqueness

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

Affine fixed-point uniqueness inside a collapsed monotone bracket. A fixed point remains equivalent to every finite iterate of itself. If it lies between endpoints whose iterates agree at a finite base step, monotonicity identifies that iterate—and therefore the fixed point—with the collapsed endpoint. Applying this twice proves pairwise uniqueness of all fixed points in the certified enclosure, without a contraction assumption. Theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-bracket-collapse

matrix/affine-iterate-collapsed-bracket-identifies-fixed-point :
  (rows : List (List ℚ)) (offset lower candidate upper : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (lower-candidate : vector/at-most lower candidate)
  (candidate-upper : vector/at-most candidate upper)
  (fixed : vector/equivalent (action) candidate) (base : ℕ)
  (collapsed : vector/equivalent (iterate₁) (iterate))
  → vector/equivalent candidate (iterate₁)
  where action := matrix/affine-action rows offset candidate
  where iterate := matrix/affine-iterate rows offset base upper
  where iterate₁ := matrix/affine-iterate rows offset base lower

matrix/affine-iterate-collapsed-bracket-fixed-points-equivalent :
  (rows : List (List ℚ))
  (offset lower left-fixed-point right-fixed-point upper : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (lower-left : vector/at-most lower left-fixed-point)
  (left-upper : vector/at-most left-fixed-point upper)
  (lower-right : vector/at-most lower right-fixed-point)
  (right-upper : vector/at-most right-fixed-point upper)
  (left-fixed : vector/equivalent (action₁) left-fixed-point)
  (right-fixed : vector/equivalent (action) right-fixed-point) (base : ℕ)
  (collapsed : vector/equivalent (iterate₃) (iterate))
  → vector/equivalent left-fixed-point right-fixed-point
  where action := matrix/affine-action rows offset right-fixed-point
  where action₁ := matrix/affine-action rows offset left-fixed-point
  where iterate := matrix/affine-iterate rows offset base upper
  where iterate₃ := matrix/affine-iterate rows offset base lower