Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-cross-vectors

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

The unified representation, brick 3 core: one elimination cross at the coefficient-vector level. Crossing a lower constraint b_L <= eval(L) against an upper constraint eval(U) <= b_U -- both coefficient vectors whose head pair is the variable x1 being eliminated -- yields the reduced constraint over the tail variables directly in coefficient-vector form: b_L*U_1 + eval(scale L_1 U_tail) <= b_U*L_1 + eval(scale U_1 L_tail). nnrat/farkas-cross-vectors proves it by composing three proved theorems: head-split each constraint on x1 (nnrat/linear-form-lower-split / -upper-split) to expose the current coefficient and the tail block, apply the affine cross crux (nnrat/farkas-affine-cross-necessary), then rewrite the product terms as scaled coefficient vectors (nnrat/farkas-reduced-vector). This is the round's arithmetic at the representation level: two coefficient-vector constraints in one fewer variable produce a both-sides coefficient-vector constraint. The fold over the variable count applies this per (lower, upper) pair, then head-splits and both-sides-reduces the next variable. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-affine-crossmath.rational.nnrat.farkas-reduced-vector

nnrat/farkas-cross-vectors :
  (x1 l-coeff u-coeff : ℚ≥0) (l-tail u-tail : List (data/Product ℚ≥0 ℚ≥0))
  (b-l b-u : ℚ≥0)
  (lower : b-l ≤ nnrat/linear-form (data/cons (data/Product ℚ≥0 ℚ≥0) (data/pair ℚ≥0 ℚ≥0 l-coeff x1) l-tail))
  (upper : nnrat/linear-form (data/cons (data/Product ℚ≥0 ℚ≥0) (data/pair ℚ≥0 ℚ≥0 u-coeff x1) u-tail) ≤ b-u)
  → b-l · u-coeff + nnrat/linear-form (nnrat/farkas-scale-right l-coeff u-tail) ≤ b-u · l-coeff + nnrat/linear-form (nnrat/farkas-scale-right u-coeff l-tail)