Reference · Non-negative rationals

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

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

Brick 5d-ii of the general LP strong-duality Fourier-Motzkin encoding : converting a both-sides row into a clean affine lower row, subtraction-free. Eliminating the SECOND variable, brick 5d-i's cross conditions carry the surviving variable v on BOTH sides: A*v + P <= B*v + Q. That is not a brick-4/5b affine row. But when A <= B, the difference witness D (with A + D ~ B, from nnrat/at-most-difference) makes it one: B*v ~ (A+D)*v ~ A*v + D*v, so A*v + P <= A*v + (D*v + Q), and cancelling the common A*v (subtraction-free, via commute + at-most-add-right-cancel) leaves P <= D*v + Q -- an affine LOWER row in v (brick 5b shape). nnrat/farkas-both-sides-to-lower takes the difference witness D (A+D~B) explicitly, so the caller supplies it from at-most-difference once A <= B is known. This unblocks the second elimination: cross rows with A_i <= B_i become affine lower rows in x2, eliminable by brick 5b (the A_i >= B_i case is the symmetric affine-upper mirror). Native proof data, axiom-free.

Depends onmath.rational.nnrat.add-monotonemath.rational.nnrat.additive-reassociationmath.rational.nnrat.distribute-rightmath.rational.nnrat.add-cancellation

nnrat/farkas-both-sides-to-lower :
  (a b d p q v : ℚ≥0)
  (diff : a + d = b)
  (both-sides : a · v + p ≤ b · v + q)
  → p ≤ d · v + q

nnrat/farkas-both-sides-to-upper :
  (a b d p q v : ℚ≥0)
  (diff : b + d = a)
  (both-sides : a · v + p ≤ b · v + q)
  → d · v + p ≤ q