Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-eliminate-round

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

One full Fourier-Motzkin elimination round, composed : cross-product then reduction. Eliminating a variable v from a list of affine lower rows and a list of affine upper rows, brick 6's cross-product core (nnrat/farkas-cross-bilist-necessary) shows every pairwise cross condition holds, and the recursive reduction (nnrat/farkas-reduce-list-necessary) turns a both-sides cross-row list into a mixed affine-row system in one fewer variable. This composes them. The one seam between the two is STRUCTURAL, and this theorem makes it explicit rather than hiding it: the cross-product core emits cross conditions with OPAQUE survivor blocks, while the reduction consumes STRUCTURED both-sides rows A*v+P <= B*v+Q. Recognizing each cross condition's blocks as linear in the next variable is exactly the structured LP-system-as-data representation the n-variable capstone must supply. So the round takes that recognition as a hypothesis `link` (bilist cross conditions imply the both-sides row system holds); the capstone's representation discharges it. Given `link`, nnrat/farkas-eliminate-round proves the reduced affine system holds -- the whole elimination round in one theorem. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-cross-bilistmath.rational.nnrat.farkas-reduce-list

nnrat/farkas-eliminate-round :
  (lower-rows upper-rows : List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (v : ℚ≥0)
  (bs-rows : List (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))))
  (w : ℚ≥0)
  (link : nnrat/farkas-cross-bilist-conditions lower-rows upper-rows → nnrat/farkas-both-sides-rows-satisfied bs-rows w)
  (lowers : nnrat/farkas-lowers-satisfied lower-rows v)
  (uppers : nnrat/farkas-elim-affine-rows-satisfied upper-rows v)
  → nnrat/farkas-reduced-conditions bs-rows w