Reference · Matrices

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

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

Sharp finite-horizon iterate error at every canonical rational rate. Exact NNRAT residual decay already proves d(x_n,x_(n+1)) <= gamma^n * d(x_0,x_1) for an arbitrary row-sum rate gamma. This module combines that computable envelope with the canonical inverse-gap certificate for `gamma=a/(a+g)`, `a=ap+1`, `g=gp+1`, yielding d(x_n,x*) <= ((a+g)/g) * gamma^n * d(x_0,x_1). Unlike the older exact-rate error theorem, no `gamma <= 1/2` premise is needed and the factor is sharp. An explicit stopping corollary accepts any threshold above the scaled envelope. Theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-nnrat-exact-rate

matrix/affine-general-rate-iterate-error-exact-envelope :
  (rows : List (List ℚ)) (offset initial fixed-point : List ℚ) (ap gp : ℕ)
  (shape : vector/same-shape initial fixed-point)
  (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))
  (fixed : vector/equivalent (action) fixed-point) (steps : ℕ)
  → vector/sup-distance (iterate) fixed-point ≤ signed/from-nnrat (nnrat/make (add) gp) · signed/nnrat-power-scale (make) steps (distance)
  where action := matrix/affine-action rows offset fixed-point
  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 steps initial
  where make := nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))

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