Reference · Non-negative rationals

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

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_cross_list.clj1 definitions, 1 theorems

Brick 5d-i of the general LP strong-duality Fourier-Motzkin encoding : the cross-product of one affine lower row against a LIST of affine upper rows. Eliminating a variable v that is bounded below by a single affine row (w_lo <= a_lo*v + s_lo -- the objective-boundary row in the two-variable case) and above by a list of affine upper rows (a_hi*v + s_hi <= b_hi -- the primal rows, brick 4's row type). Any v satisfying the lower row and every upper row yields, for EVERY upper row, that row's cross condition (brick 5c, nnrat/farkas-affine-cross-necessary): the reduced system in the surviving variables. This maps the single-pair cross crux across the upper-row list by List.rec, exactly as brick 4's projection mapped its per-row argument. The reduced conditions are collected by nnrat/farkas-cross-list-conditions (a fold of the per-row cross condition), and nnrat/farkas-cross-list-necessary proves feasibility implies they all hold. Reuses brick 4's rows-satisfied fold for the uppers and brick 5c for each pair. Native proof data, axiom-free. The n-lower generalization (a list of lowers too) is brick 6's induction; the two-variable payoff needs only this one-lower form.

Depends onmath.rational.nnrat.farkas-affine-crossmath.rational.nnrat.farkas-elim-affine-list

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

nnrat/farkas-cross-list-necessary :
  (a-lo s-lo w-lo : ℚ≥0) (upper-rows : List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))
  (v : ℚ≥0)
  (lower : w-lo ≤ a-lo · v + s-lo)
  (uppers : nnrat/farkas-elim-affine-rows-satisfied upper-rows v)
  → nnrat/farkas-cross-list-conditions upper-rows a-lo s-lo w-lo