Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-vector-both-sides

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_vector_both_sides.clj0 definitions, 2 theorems

The unified representation, second-variable step: convert a reduced both-sides COEFFICIENT-VECTOR row into a lower/upper affine row in the next variable x2, subtraction-free. One round (nnrat/farkas-cross-vectors / -all-reduced) eliminates x1 and leaves, per (lower,upper) pair, the reduced both-sides vector constraint b_L*u1 + eval(scale l1 u-tail) <= b_U*l1 + eval(scale u1 l-tail). When the tails are headed by the NEXT variable x2 -- u-tail = (a2u,x2)::ru, l-tail = (a2l,x2)::rl -- both scaled evals reduce definitionally (farkas-scale-right's cons case, then linear-form's cons case) to A*x2 + rest, so the whole constraint is affine in x2 on both sides: CL + (AL*x2 + EL) <= CR + (AR*x2 + ER) with AL = a2u*l1, AR = a2l*u1, CL = b_L*u1, CR = b_U*l1, EL = eval(scale l1 ru), ER = eval(scale u1 rl). Grouping the x2 term to the front (commute/reassociate, no subtraction) gives exactly the shape nnrat/farkas-both-sides-to-lower / -to-upper consume, so with the difference witness (AL+D~AR for a lower row, AR+D~AL for an upper row) this produces the reduced constraint for eliminating x2: to-lower: (CL + EL) <= D*x2 + (CR + ER) -- x2 lower-bounded to-upper: D*x2 + (CL + EL) <= (CR + ER) -- x2 upper-bounded These are the both-sides rows the next round crosses (packaging CL+EL / CR+ER as coefficient vectors with a unit column is the follow-on brick). This is the vector-level analogue of nnrat/farkas-both-sides, and the per-row core of the coefficient-vector partition that closes the over-variable recursion's step. Native proof data, axiom-free.

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

nnrat/farkas-vector-both-sides-to-lower :
  (l-coeff u-coeff b-l b-u a2l a2u : ℚ≥0) (rl ru : List (data/Product ℚ≥0 ℚ≥0))
  (x2 d : ℚ≥0)
  (diff : a2u · l-coeff + d = a2l · u-coeff)
  (h : b-l · u-coeff + nnrat/linear-form (nnrat/farkas-scale-right l-coeff (cons)) ≤ b-u · l-coeff + nnrat/linear-form (nnrat/farkas-scale-right u-coeff (cons₁)))
  → b-l · u-coeff + nnrat/linear-form (nnrat/farkas-scale-right l-coeff ru) ≤ d · x2 + (b-u · l-coeff + nnrat/linear-form (nnrat/farkas-scale-right u-coeff rl))
  where cons := data/cons (data/Product ℚ≥0 ℚ≥0) (data/pair ℚ≥0 ℚ≥0 a2u x2) ru
  where cons₁ := data/cons (data/Product ℚ≥0 ℚ≥0) (data/pair ℚ≥0 ℚ≥0 a2l x2) rl

nnrat/farkas-vector-both-sides-to-upper :
  (l-coeff u-coeff b-l b-u a2l a2u : ℚ≥0) (rl ru : List (data/Product ℚ≥0 ℚ≥0))
  (x2 d : ℚ≥0)
  (diff : a2l · u-coeff + d = a2u · l-coeff)
  (h : b-l · u-coeff + nnrat/linear-form (nnrat/farkas-scale-right l-coeff (cons)) ≤ b-u · l-coeff + nnrat/linear-form (nnrat/farkas-scale-right u-coeff (cons₁)))
  → d · x2 + (b-l · u-coeff + nnrat/linear-form (nnrat/farkas-scale-right l-coeff ru)) ≤ b-u · l-coeff + nnrat/linear-form (nnrat/farkas-scale-right u-coeff rl)
  where cons := data/cons (data/Product ℚ≥0 ℚ≥0) (data/pair ℚ≥0 ℚ≥0 a2u x2) ru
  where cons₁ := data/cons (data/Product ℚ≥0 ℚ≥0) (data/pair ℚ≥0 ℚ≥0 a2l x2) rl