Reference · Matrices

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

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

Exact convergence certificates from collapsed affine brackets. If residual-certified lower and upper trajectories agree at a finite step, nested bracketing forces the lower trajectory to agree with its next step; exact stabilization then yields an affine fixed point. Independently, monotonicity shows that every trajectory started between the original endpoints agrees with the collapsed value at that step. Theorem-only, kernel-checked, and axiom-free on D63.

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

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

matrix/affine-iterate-residual-bracket-collapse-fixed-point :
  (rows : List (List ℚ)) (offset lower upper : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (lower-image-shape : vector/same-shape lower (matrix/vector-multiply rows lower))
  (upper-image-shape : vector/same-shape upper (matrix/vector-multiply rows upper))
  (lower-residual-upper : vector/at-most (subtract) offset)
  (upper-residual-lower : vector/at-most offset (subtract₂))
  (lower-upper : vector/at-most lower upper) (base : ℕ)
  (collapsed : vector/equivalent (matrix/affine-iterate rows offset base lower) (iterate))
  → vector/equivalent (action) (matrix/affine-iterate rows offset base lower)
  where action := matrix/affine-action rows offset (matrix/affine-iterate rows offset base lower)
  where iterate := matrix/affine-iterate rows offset base upper
  where subtract := vector/subtract lower (matrix/vector-multiply rows lower)
  where subtract₂ := vector/subtract upper (matrix/vector-multiply rows upper)

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