Reference · Matrices

rainbow.math.linear.matrix.affine-nnrat-exact-rate

Matricessrc/rainbow/math/linear/matrix/affine_nnrat_exact_rate.clj1 definitions, 8 theorems

Exact NNRAT-rate contraction and residual certificates. `signed/nnrat-power-scale gamma n d` is the native signed recurrence `d, gamma*d, gamma*(gamma*d), ...`. Unlike the conservative half envelope, it records the actual certified row-sum factor. The matrix theorems prove exact gamma-power bounds for paired trajectories and successive residuals. When gamma <= 1/2, the a posteriori residual theorem then yields a fixed-point error certificate with the same exact envelope. Native, kernel-checked, and axiom-free on D63.

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

signed/nnrat-power-scale :
  (x₁ : ℚ≥0) (x₂ : ℕ) (x₃ : ℚ)
  → ℚ

signed/nnrat-power-scale-zero :
  (gamma : ℚ≥0) (value : ℚ)
  → signed/nnrat-power-scale gamma 0 value = value

signed/nnrat-power-scale-successor :
  (gamma : ℚ≥0) (steps : ℕ) (value : ℚ)
  → signed/nnrat-power-scale gamma (data/succ steps) value = signed/from-nnrat gamma · signed/nnrat-power-scale gamma steps value

signed/nnrat-power-scale-nonnegative :
  (gamma : ℚ≥0) (value : ℚ)
  (value-nonnegative : 0 ≤ value)
  (steps : ℕ)
  → 0 ≤ signed/nnrat-power-scale gamma steps value

signed/nnrat-power-scale-monotone :
  (gamma : ℚ≥0) (left right : ℚ)
  (ordered : left ≤ right)
  (steps : ℕ)
  → signed/nnrat-power-scale gamma steps left ≤ signed/nnrat-power-scale gamma steps right

matrix/affine-nnrat-row-sum-iterate-sup-distance-rate :
  (rows : List (List ℚ)) (offset left right : List ℚ) (gamma : ℚ≥0)
  (shape : vector/same-shape left right)
  (offset-shape : vector/same-shape offset (matrix/vector-multiply rows left))
  (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)
  (steps : ℕ)
  → vector/sup-distance (iterate₁) (iterate) ≤ signed/nnrat-power-scale gamma steps (vector/sup-distance left right)
  where iterate := matrix/affine-iterate rows offset steps right
  where iterate₁ := matrix/affine-iterate rows offset steps left

matrix/affine-nnrat-successive-residual-rate :
  (rows : List (List ℚ)) (offset initial : List ℚ) (gamma : ℚ≥0)
  (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 gamma)
  (steps : ℕ)
  → vector/sup-distance (iterate₂) (iterate) ≤ signed/nnrat-power-scale gamma steps (distance)
  where distance := vector/sup-distance initial (matrix/affine-action rows offset initial)
  where iterate := matrix/affine-iterate rows offset (data/succ steps) initial
  where iterate₂ := matrix/affine-iterate rows offset steps initial

matrix/affine-nnrat-strong-row-iterate-error-exact-rate :
  (rows : List (List ℚ)) (offset initial fixed-point : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (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 gamma)
  (fixed : vector/equivalent (action) fixed-point) (steps : ℕ)
  → vector/sup-distance (iterate) fixed-point ≤ scale + scale
  where action := matrix/affine-action rows offset fixed-point
  where iterate := matrix/affine-iterate rows offset steps initial
  where scale := signed/nnrat-power-scale gamma steps (vector/sup-distance initial (matrix/affine-action rows offset initial))

matrix/affine-nnrat-strong-row-stopping-certificate-exact-rate :
  (rows : List (List ℚ)) (offset initial fixed-point : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (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 gamma)
  (fixed : vector/equivalent (action) fixed-point) (steps : ℕ) (threshold : ℚ)
  (envelope-at-most-threshold : scale + scale ≤ threshold)
  → vector/sup-distance (iterate) fixed-point ≤ threshold
  where action := matrix/affine-action rows offset fixed-point
  where iterate := matrix/affine-iterate rows offset steps initial
  where scale := signed/nnrat-power-scale gamma steps (vector/sup-distance initial (matrix/affine-action rows offset initial))