Reference · Matrices

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

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

Uniqueness of enclosed affine residual solutions after bracket collapse. Linear solvers expose `x - rows*x ~ offset`, not an affine fixed-point proposition. Under the exact value/image shape needed to add the image back, an enclosed residual solution is identified with a collapsed monotone bracket; consequently any two enclosed residual solutions are equivalent. This is a solver-facing corollary of collapsed-bracket fixed-point uniqueness. Theorem-only, kernel-checked, and axiom-free on D63.

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

matrix/affine-iterate-collapsed-bracket-identifies-residual-solution :
  (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)
  (candidate-image-shape : vector/same-shape candidate (matrix/vector-multiply rows candidate))
  (residual-equation : vector/equivalent (subtract) offset) (base : ℕ)
  (collapsed : vector/equivalent (iterate₂) (iterate))
  → vector/equivalent candidate (iterate₂)
  where iterate := matrix/affine-iterate rows offset base upper
  where iterate₂ := matrix/affine-iterate rows offset base lower
  where subtract := vector/subtract candidate (matrix/vector-multiply rows candidate)

matrix/affine-iterate-collapsed-bracket-residual-solutions-equivalent :
  (rows : List (List ℚ)) (offset lower left-solution right-solution upper : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (lower-left : vector/at-most lower left-solution)
  (left-upper : vector/at-most left-solution upper)
  (lower-right : vector/at-most lower right-solution)
  (right-upper : vector/at-most right-solution upper)
  (left-image-shape : vector/same-shape left-solution (matrix/vector-multiply rows left-solution))
  (right-image-shape : vector/same-shape right-solution (matrix/vector-multiply rows right-solution))
  (left-residual : vector/equivalent (subtract₁) offset)
  (right-residual : vector/equivalent (subtract) offset) (base : ℕ)
  (collapsed : vector/equivalent (iterate₃) (iterate))
  → vector/equivalent left-solution right-solution
  where iterate := matrix/affine-iterate rows offset base upper
  where iterate₃ := matrix/affine-iterate rows offset base lower
  where subtract := vector/subtract right-solution (matrix/vector-multiply rows right-solution)
  where subtract₁ := vector/subtract left-solution (matrix/vector-multiply rows left-solution)