Reference · Non-negative rationals

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

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_cross_bilist.clj2 definitions, 1 theorems

Brick 6 (cross-product core) of the general LP strong-duality Fourier-Motzkin encoding: the cross-product over BOTH row lists -- a list of affine lower rows against a list of affine upper rows. The two-variable instance (5d-iii) eliminated a variable with ONE lower row (the objective) against a list of upper rows (5d-i). The general n-variable induction eliminates a variable that carries a LIST of lower rows AND a list of upper rows, and its reduced system is EVERY pairwise cross condition. This generalizes 5d-i by an outer List.rec over the lower rows: any v satisfying every lower row and every upper row yields, for each lower row, that lower's whole cross-condition list (5d-i applied per lower). Parameterized, no concrete arithmetic -- the reusable elimination step the n-variable induction folds over the variable count. nnrat/farkas-cross-bilist-necessary proves it; the reduced conditions are collected by nnrat/farkas-cross-bilist-conditions (a fold over the lower rows of 5d-i's per-lower fold). Reuses 5d-i (nnrat/farkas-cross-list-necessary) per lower row and brick 4's rows-satisfied for the uppers. Native proof data, axiom-free.

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

nnrat/farkas-lowers-satisfied :
  (x₁ : List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (x₂ : ℚ≥0)
  → Prop

nnrat/farkas-cross-bilist-conditions :
  (x₁ x₂ : List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))
  → Prop

nnrat/farkas-cross-bilist-necessary :
  (lower-rows upper-rows : List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (v : ℚ≥0)
  (lowers : nnrat/farkas-lowers-satisfied lower-rows v)
  (uppers : nnrat/farkas-elim-affine-rows-satisfied upper-rows v)
  → nnrat/farkas-cross-bilist-conditions lower-rows upper-rows