Reference · Signed rationals

rainbow.math.rational.signed.matrix-lp-row-length-duality

Signed rationals src/rainbow/math/rational/signed/matrix_lp_row_length_duality.clj0 definitions, 1 theorems

Signed matrix LP weak duality from concrete dimension certificates. The core theorem accepts abstract `same-shape` and `matrix/compatible` evidence. External checkers naturally measure lengths instead. This corollary accepts exact length equality for the dual vector and one row-length equality per constraint row, derives the abstract premises, and delegates the actual optimization argument to the existing weak-duality theorem. This changes the certificate boundary, not the mathematical guarantee. It is Level-3, native, deterministic, and axiom-free on D63.

Depends onmath.rational.signed.matrix-lp-duality

optimization/signed-matrix-lp-weak-duality-from-length-certificates

TheoremFor all inputsNo axiomsSource, line 57

optimization/signed-matrix-lp-weak-duality-from-length-certificates :
  (rows : List (List ℚ)) (b c x y : List ℚ)
  (y-row-length : vector/length y = vector/length (matrix/column-shape rows))
  (rows-x-lengths : matrix/row-length-compatible rows x)
  (primal-feasible : vector/at-most (matrix/vector-multiply rows x) b)
  (dual-feasible : vector/at-most c (multiply))
  (x-nonnegative : vector/at-most (vector/zero-like x) x)
  (y-nonnegative : vector/at-most (vector/zero-like y) y)
  → vector/dot c x ≤ vector/dot b y
  where multiply := matrix/vector-multiply (matrix/transpose rows) y

= = equality/EqList = data/Listℚ = signed/SignedRational≤ = signed/at-most