Reference · Matrices

rainbow.math.linear.matrix.affine-inverse-gap-stability

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

Sharp stability of two approximate affine solutions at arbitrary rates. For a reference affine map F with row-sum rate `q`, two candidates obey the quotient-safe inverse-gap bound d(x,y) <= inverse * (d(x,Fx) + d(Fy,y)), whenever `q + gap ~ 1` and `inverse * gap ~ 1`. A bridged form replaces `d(Fy,y)` by `d(Fy,Gy) + d(Gy,y)`, allowing comparison against an arbitrary second model without requiring that model to contract. Canonical wrappers instantiate `q=a/(a+g)` and `inverse=(a+g)/g` for every positive naturals `a=ap+1`, `g=gp+1`. Thus independently implemented solvers and perturbed models receive the sharp rational factor without a `q <= 1/2` premise. Theorem-only, kernel-checked, and axiom-free on D63.

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

matrix/affine-inverse-gap-approximate-stability :
  (rows : List (List ℚ)) (offset left right : List ℚ) (rate gap inverse : ℚ)
  (rate-nonnegative : 0 ≤ rate)
  (inverse-nonnegative : 0 ≤ inverse)
  (rate-plus-gap-one : rate + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  (shape : vector/same-shape left right)
  (left-residual-shape : vector/same-shape left (matrix/affine-action rows offset left))
  (right-residual-shape : vector/same-shape (matrix/affine-action rows offset right) 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 ≤ rate)
  → vector/sup-distance left right ≤ inverse · (vector/sup-distance left (matrix/affine-action rows offset left) + vector/sup-distance (matrix/affine-action rows offset right) right)

matrix/affine-inverse-gap-two-threshold-certificate :
  (rows : List (List ℚ)) (offset left right : List ℚ) (rate gap inverse : ℚ)
  (rate-nonnegative : 0 ≤ rate)
  (inverse-nonnegative : 0 ≤ inverse)
  (rate-plus-gap-one : rate + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  (shape : vector/same-shape left right)
  (left-residual-shape : vector/same-shape left (matrix/affine-action rows offset left))
  (right-residual-shape : vector/same-shape (matrix/affine-action rows offset right) 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 ≤ rate)
  (left-threshold right-threshold : ℚ)
  (left-residual-bound : vector/sup-distance left (matrix/affine-action rows offset left) ≤ left-threshold)
  (right-residual-bound : vector/sup-distance (matrix/affine-action rows offset right) right ≤ right-threshold)
  → vector/sup-distance left right ≤ inverse · (left-threshold + right-threshold)

matrix/affine-general-rate-approximate-stability :
  (rows : List (List ℚ)) (offset left right : List ℚ) (ap gp : ℕ)
  (shape : vector/same-shape left right)
  (left-residual-shape : vector/same-shape left (matrix/affine-action rows offset left))
  (right-residual-shape : vector/same-shape (matrix/affine-action rows offset right) 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/make (data/succ ap) (algebra/nat-add ap (data/succ gp))))
  → vector/sup-distance left right ≤ signed/from-nnrat (nnrat/make (add) gp) · (vector/sup-distance left (matrix/affine-action rows offset left) + vector/sup-distance (matrix/affine-action rows offset right) right)
  where add := algebra/nat-add (data/succ ap) (data/succ gp)

matrix/affine-general-rate-two-threshold-certificate :
  (rows : List (List ℚ)) (offset left right : List ℚ) (ap gp : ℕ)
  (shape : vector/same-shape left right)
  (left-residual-shape : vector/same-shape left (matrix/affine-action rows offset left))
  (right-residual-shape : vector/same-shape (matrix/affine-action rows offset right) 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/make (data/succ ap) (algebra/nat-add ap (data/succ gp))))
  (left-threshold right-threshold : ℚ)
  (left-residual-bound : vector/sup-distance left (matrix/affine-action rows offset left) ≤ left-threshold)
  (right-residual-bound : vector/sup-distance (matrix/affine-action rows offset right) right ≤ right-threshold)
  → vector/sup-distance left right ≤ signed/from-nnrat (nnrat/make (add) gp) · (left-threshold + right-threshold)
  where add := algebra/nat-add (data/succ ap) (data/succ gp)

matrix/affine-general-rate-bridged-threshold-certificate :
  (rows : List (List ℚ)) (offset left right comparison-image : List ℚ) (ap gp : ℕ)
  (shape : vector/same-shape left right)
  (left-residual-shape : vector/same-shape left (matrix/affine-action rows offset left))
  (bridge-shape : vector/same-shape (matrix/affine-action rows offset right) comparison-image)
  (comparison-residual-shape : vector/same-shape comparison-image 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/make (data/succ ap) (algebra/nat-add ap (data/succ gp))))
  (left-threshold bridge-threshold comparison-residual-threshold : ℚ)
  (left-residual-bound : vector/sup-distance left (matrix/affine-action rows offset left) ≤ left-threshold)
  (bridge-bound : vector/sup-distance (matrix/affine-action rows offset right) comparison-image ≤ bridge-threshold)
  (comparison-residual-bound : vector/sup-distance comparison-image right ≤ comparison-residual-threshold)
  → vector/sup-distance left right ≤ signed/from-nnrat (nnrat/make (add) gp) · (left-threshold + (bridge-threshold + comparison-residual-threshold))
  where add := algebra/nat-add (data/succ ap) (data/succ gp)

matrix/affine-general-rate-bridged-stability :
  (rows : List (List ℚ)) (offset left right comparison-image : List ℚ) (ap gp : ℕ)
  (shape : vector/same-shape left right)
  (left-residual-shape : vector/same-shape left (matrix/affine-action rows offset left))
  (bridge-shape : vector/same-shape (matrix/affine-action rows offset right) comparison-image)
  (comparison-residual-shape : vector/same-shape comparison-image 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/make (data/succ ap) (algebra/nat-add ap (data/succ gp))))
  → vector/sup-distance left right ≤ signed/from-nnrat (nnrat/make (add) gp) · (vector/sup-distance left (matrix/affine-action rows offset left) + (vector/sup-distance (matrix/affine-action rows offset right) comparison-image + vector/sup-distance comparison-image right))
  where add := algebra/nat-add (data/succ ap) (data/succ gp)