Reference · Matrices

rainbow.math.linear.matrix.affine-half-iterate-converges

Matricessrc/rainbow/math/linear/matrix/affine_half_iterate_converges.clj1 definitions, 6 theorems

Rate-null convergence for half-row signed affine iteration. The older `analysis/converges` quantifies over negative signed radii and is intentionally documented as uninhabitable even by constant sequences. This module instead defines `analysis/signed-rate-null` over the constructive reciprocal NNRAT ladder: after modulus M(k), a signed sequence is nonnegative and at most the embedded radius 1/(k+1). Domination and pointwise signed equivalence preserve this certificate. The signed geometric bridge proves the half-power unit envelope rate-null. Consequently unit-bounded paired affine iterates coalesce at that rate, and iteration from any unit-bounded initial distance converges to a certified fixed point. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.signed.geometric-bridge

analysis/signed-rate-null :
  (x₁ : ℕ → ℚ) (x₂ : ℕ → ℕ)
  → Prop

analysis/signed-half-power-one-rate-null :
  → analysis/signed-rate-null (fun n => signed/half-power-scale n 1) (fun k => k)

analysis/signed-rate-null-dominated :
  (source target : ℕ → ℚ) (modulus : ℕ → ℕ)
  (target-nonnegative : ∀ (n : ℕ), 0 ≤ target n)
  (dominated : ∀ (n : ℕ), target n ≤ source n)
  (source-null : analysis/signed-rate-null source modulus)
  → analysis/signed-rate-null target modulus

analysis/signed-rate-null-respects-equivalence :
  (source target : ℕ → ℚ) (modulus : ℕ → ℕ)
  (pointwise : ∀ (n : ℕ), source n = target n)
  (source-null : analysis/signed-rate-null source modulus)
  → analysis/signed-rate-null target modulus

analysis/signed-half-power-rate-null-of-at-most-one :
  (value : ℚ)
  (value-nonnegative : 0 ≤ value)
  (value-at-most-one : value ≤ 1)
  → analysis/signed-rate-null (fun n => signed/half-power-scale n value) (fun k => k)

matrix/affine-half-iterate-sup-distance-rate-null :
  (rows : List (List ℚ)) (offset left right : List ℚ)
  (initial-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 nnrat/half)
  (initial-distance-at-most-one : vector/sup-distance left right ≤ 1)
  → analysis/signed-rate-null (fun n => vector/sup-distance (matrix/affine-iterate rows offset n left) (matrix/affine-iterate rows offset n right)) (fun k => k)

matrix/affine-half-iterate-converges-to-fixed-point :
  (rows : List (List ℚ)) (offset left fixed-point : List ℚ)
  (initial-shape : vector/same-shape left fixed-point)
  (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 nnrat/half)
  (initial-distance-at-most-one : vector/sup-distance left fixed-point ≤ 1)
  (fixed : vector/equivalent (action) fixed-point)
  → analysis/signed-rate-null (fun n => vector/sup-distance (matrix/affine-iterate rows offset n left) fixed-point) (fun k => k)
  where action := matrix/affine-action rows offset fixed-point