Reference · Matrices

rainbow.math.linear.matrix.affine-general-rate-tail-certificate

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

Sharp fixed-point-free tail certificates at arbitrary rational rates. For canonical `gamma=a/(a+g)`, exact residual decay supplies a computable envelope at each iteration horizon. Applying sharp two-candidate stability to horizons m and n gives d(x_m,x_n) <= ((a+g)/g) * (gamma^m*r_0 + gamma^n*r_0), where `r_0=d(x_0,x_1)`. This is a finite Cauchy certificate that requires neither an exact fixed point nor a completeness axiom. A threshold corollary exposes a direct stopping condition. Theorem-only, kernel-checked, and axiom-free on D63.

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

matrix/affine-general-rate-iterate-tail-bound :
  (rows : List (List ℚ)) (offset initial : List ℚ) (ap gp : ℕ)
  (step-shape : vector/same-shape initial (matrix/affine-action rows offset initial))
  (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 (make))
  (left-steps right-steps : ℕ)
  → vector/sup-distance (iterate₃) (iterate) ≤ signed/from-nnrat (nnrat/make (add) gp) · (signed/nnrat-power-scale (make) left-steps (distance) + signed/nnrat-power-scale (make) right-steps (distance))
  where add := algebra/nat-add (data/succ ap) (data/succ gp)
  where distance := vector/sup-distance initial (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
  where make := nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))

matrix/affine-general-rate-iterate-tail-stopping-certificate :
  (rows : List (List ℚ)) (offset initial : List ℚ) (ap gp : ℕ)
  (step-shape : vector/same-shape initial (matrix/affine-action rows offset initial))
  (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 (make))
  (left-steps right-steps : ℕ) (threshold : ℚ)
  (tail-envelope-at-most-threshold : signed/from-nnrat (nnrat/make (add) gp) · (signed/nnrat-power-scale (make) left-steps (distance) + signed/nnrat-power-scale (make) right-steps (distance)) ≤ threshold)
  → vector/sup-distance (iterate₃) (iterate) ≤ threshold
  where add := algebra/nat-add (data/succ ap) (data/succ gp)
  where distance := vector/sup-distance initial (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
  where make := nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))