Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-reduced-vector

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_reduced_vector.clj0 definitions, 1 theorems

The unified representation, brick 2 assembly : the cross condition expressed as a both-sides constraint over transformed coefficient vectors. Crossing a lower row (tail vector L_tail, head coefficient a_lo, bound w_lo) against an upper row (tail vector U_tail, head coefficient a_hi, bound b_hi) gives the cross condition w_lo*a_hi + eval(U_tail)*a_lo <= b_hi*a_lo + eval(L_tail)*a_hi. nnrat/farkas-reduced-vector rewrites its variable parts as coefficient vectors, using the scale lemma (nnrat/farkas-form-scale-right) on each side: eval(U_tail)*a_lo ~ eval(scale a_lo U_tail) and eval(L_tail)*a_hi ~ eval(scale a_hi L_tail). So the reduced constraint is w_lo*a_hi + eval(scale a_lo U_tail) <= b_hi*a_lo + eval(scale a_hi L_tail) -- a both-sides LINEAR constraint over the tail variables whose two coefficient vectors are scale(a_lo, U_tail) and scale(a_hi, L_tail). This is the columnwise cross transform assembled: the reduced constraint is back in the coefficient-vector representation over one fewer variable (head-splitting the next variable off these vectors, then the both-sides reduction, is the next round). Transported by at-most-respects. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-form-scale

nnrat/farkas-reduced-vector :
  (w-lo a-hi a-lo b-hi : ℚ≥0) (l-tail u-tail : List (data/Product ℚ≥0 ℚ≥0))
  (cross : w-lo · a-hi + nnrat/linear-form u-tail · a-lo ≤ b-hi · a-lo + nnrat/linear-form l-tail · a-hi)
  → w-lo · a-hi + nnrat/linear-form (nnrat/farkas-scale-right a-lo u-tail) ≤ b-hi · a-lo + nnrat/linear-form (nnrat/farkas-scale-right a-hi l-tail)