Reference · Matrices

rainbow.math.linear.matrix.half-row-sum-fixed-point-uniqueness

Matricessrc/rainbow/math/linear/matrix/half_row_sum_fixed_point_uniqueness.clj0 definitions, 6 theorems

Concrete half-contractive uniqueness for signed affine row-sum systems. The signed embedding of 1/2 adds to one, so two copies of `d <= (1/2)d` yield `d+d <= d`. Additive order cancellation gives `d <= 0`; combined with nonnegativity, antisymmetry gives `d ~ 0`. This discharges the abstract collapse certificate used by the generic row-sum fixed-point theorem and produces a premise-complete half-rate affine uniqueness result. Native, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.row-sum-fixed-point-uniqueness

signed/half-add-half :
  → signed/from-nnrat nnrat/half + signed/from-nnrat nnrat/half = 1

signed/half-scale-add-self :
  (value : ℚ)
  → signed/from-nnrat nnrat/half · value + signed/from-nnrat nnrat/half · value = value

signed/zero-at-most-half :
  → 0 ≤ signed/from-nnrat nnrat/half

signed/half-contraction-collapse :
  (distance : ℚ)
  (distance-nonnegative : 0 ≤ distance)
  (self-bound : distance ≤ signed/from-nnrat nnrat/half · distance)
  → distance = 0

matrix/affine-half-row-sum-fixed-points-have-zero-sup-distance :
  (rows : List (List ℚ)) (offset left right : List ℚ)
  (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)
  (left-fixed : vector/equivalent (matrix/affine-action rows offset left) left)
  (right-fixed : vector/equivalent (matrix/affine-action rows offset right) right)
  → vector/sup-distance left right = 0

matrix/affine-half-row-sum-fixed-points-unique :
  (rows : List (List ℚ)) (offset left right : List ℚ)
  (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)
  (left-fixed : vector/equivalent (matrix/affine-action rows offset left) left)
  (right-fixed : vector/equivalent (matrix/affine-action rows offset right) right)
  → vector/equivalent left right