Reference · Matrices

rainbow.math.linear.matrix.affine-tail-diameter

Matricessrc/rainbow/math/linear/matrix/affine_tail_diameter.clj0 definitions, 4 theorems

Constructive tail diameter for contractive affine iteration. Shape preservation is factored into reusable lemmas: every iterate has the initial vector's shape, all horizons therefore share a shape, and each iterate has the shape of its affine image. Combining those facts with eventual residual certificates and approximate-solution stability proves k <= m, k <= n => d(x_m,x_n) <= 4 * from-nnrat(harmonic k). This is a computable Cauchy-style tail certificate that assumes no supplied exact fixed point or completeness principle. Native, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-approximate-fixed-point

matrix/affine-iterate-preserves-initial-shape :
  (rows : List (List ℚ)) (offset initial : List ℚ)
  (step-shape : vector/same-shape initial (action))
  (offset-shape : vector/same-shape offset (matrix/vector-multiply rows initial))
  (steps : ℕ)
  → vector/same-shape initial (iterate)
  where action := matrix/affine-action rows offset initial
  where iterate := matrix/affine-iterate rows offset steps initial

matrix/affine-iterates-same-shape :
  (rows : List (List ℚ)) (offset initial : List ℚ)
  (step-shape : vector/same-shape initial (action))
  (offset-shape : vector/same-shape offset (matrix/vector-multiply rows initial))
  (left-steps right-steps : ℕ)
  → vector/same-shape (iterate₁) (iterate)
  where action := matrix/affine-action rows offset initial
  where iterate := matrix/affine-iterate rows offset right-steps initial
  where iterate₁ := matrix/affine-iterate rows offset left-steps initial

matrix/affine-iterate-residual-shape :
  (rows : List (List ℚ)) (offset initial : List ℚ)
  (step-shape : vector/same-shape initial (action₁))
  (offset-shape : vector/same-shape offset (matrix/vector-multiply rows initial))
  (steps : ℕ)
  → vector/same-shape (matrix/affine-iterate rows offset steps initial) (action)
  where action := matrix/affine-action rows offset (matrix/affine-iterate rows offset steps initial)
  where action₁ := matrix/affine-action rows offset initial

matrix/affine-nnrat-iterate-tail-diameter :
  (rows : List (List ℚ)) (offset initial : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (step-shape : vector/same-shape initial (action))
  (offset-shape : vector/same-shape offset (matrix/vector-multiply rows initial))
  (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 gamma)
  (initial-residual-at-most-one : vector/sup-distance initial (action) ≤ 1)
  (index left-steps right-steps : ℕ)
  (left-large-enough : index ≤ left-steps)
  (right-large-enough : index ≤ right-steps)
  → vector/sup-distance (iterate₁) (iterate) ≤ signed/from-nnrat (nnrat/harmonic index) + signed/from-nnrat (nnrat/harmonic index) + (signed/from-nnrat (nnrat/harmonic index) + signed/from-nnrat (nnrat/harmonic index))
  where action := matrix/affine-action rows offset initial
  where iterate := matrix/affine-iterate rows offset right-steps initial
  where iterate₁ := matrix/affine-iterate rows offset left-steps initial