Skip to content
Flexiana
Menu
Solutions
How we work
Research
Work
Products
Company
Bring us a hard problem
Rainbow docs menu

Reference · Signed rationals

rainbow.math.rational.signed.matrix-lp-dimension-decision-duality

Signed rationalssrc/rainbow/math/rational/signed/matrix_lp_dimension_decision_duality.clj0 definitions, 1 theorems

Signed matrix LP weak duality from executable dimension decisions. This is the proof-facing API an independent checker wants: provide evidence that the native Nat and matrix dimension deciders returned true, together with feasibility and nonnegativity evidence. The theorem converts those decisions into exact length certificates and delegates to the existing matrix weak-duality corollary. It verifies the submitted decision evidence, not a host parser, solver, or arbitrary executable. Native and axiom-free on D63.

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

optimization/signed-matrix-lp-weak-duality-from-dimension-decisions

TheoremFor all inputsNo axiomsSource, line 62

optimization/signed-matrix-lp-weak-duality-from-dimension-decisions :
  (rows : List (List ℚ)) (b c x y : List ℚ)
  (y-dimension-decision : nat/decide-equality (vector/length y) (vector/length (matrix/column-shape rows)) = data/true)
  (rows-x-dimension-decision : matrix/decide-row-length-compatible rows x = data/true)
  (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